Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Assertions on precise generic data representation.
I like being real picky with my generic code, disallowing misuse at the type level. However, this makes it less flexible overall, and is a large chunk of the code I have to write over and over again.
I mainly care about sanity checks, along the lines of "if the generic representations looks like this, type error out". So they don't make any term-level changes.
So, instead of hiding these in generic type class instances, I put them in type family equations. Now we can turn these checks on and off -- and when they're on, you have to carry around that fact in your types. Fantastic!
Checks are formed as Constraint
s, where a failure triggers a TypeError
and a
success goes to the empty constraint ()
(
as well as
()
:: Constraint
Type
).
These checks were always done on the type-level, but they were "inline" with the rest of the type class. By pulling them out, we *should* be incurring some compile-time performance penalty (albeit hopefully minor due to the simple nature of the checks), but making no change to runtime.
Synopsis
- data GCAssert
- type family ApplyGCAssert x a where ...
- type family ApplyGCAsserts ls a where ...
- type family GCNoEmpty a where ...
- type family GCNoSum a where ...
- type family GCNeedSum a where ...
Documentation
Generic representation assertions, on the constructor level (bits that come
after D1
).
type family ApplyGCAssert x a where ... Source #
Convert a generic representation constructor-level assertion "label" to the assertion it represents, and make that assertion.
ApplyGCAssert 'NoEmpty a = GCNoEmpty a | |
ApplyGCAssert 'NoSum a = GCNoSum a | |
ApplyGCAssert 'NeedSum a = GCNeedSum a |
type family ApplyGCAsserts ls a where ... Source #
Apply a list of generic representation constructor-level assertions.
ApplyGCAsserts '[] a = () | |
ApplyGCAsserts (l ': ls) a = (ApplyGCAssert l a, ApplyGCAsserts ls a) |