Safe Haskell | None |
---|---|
Language | Haskell2010 |
Explicit dictionaries.
When working with compound constraints such as constructed
using All
or All2
, GHC cannot always prove automatically
what one would expect to hold.
This module provides a way of explicitly proving conversions between such constraints to GHC. Such conversions still have to be manually applied.
This module is new and experimental in generics-sop 0.2. It is therefore not yet exported via the main module and has to be imported explicitly. Its interface is to be considered even less stable than that of the rest of the library. Feedback is very welcome though.
- data Dict c a where
- pureAll :: SListI xs => Dict (All Top) xs
- pureAll2 :: All SListI xss => Dict (All2 Top) xss
- mapAll :: forall c d xs. (forall a. Dict c a -> Dict d a) -> Dict (All c) xs -> Dict (All d) xs
- mapAll2 :: forall c d xss. (forall a. Dict c a -> Dict d a) -> Dict (All2 c) xss -> Dict (All2 d) xss
- zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs
- zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss
- unAll_NP :: forall c xs. Dict (All c) xs -> NP (Dict c) xs
- unAll_POP :: forall c xss. Dict (All2 c) xss -> POP (Dict c) xss
- all_NP :: NP (Dict c) xs -> Dict (All c) xs
- all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss
- unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss
- all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss
- withDict :: Dict c a -> (c a => r) -> r
Documentation
pureAll :: SListI xs => Dict (All Top) xs Source
A proof that the trivial constraint holds over all type-level lists.
pureAll2 :: All SListI xss => Dict (All2 Top) xss Source
A proof that the trivial constraint holds over all type-level lists of lists.
mapAll :: forall c d xs. (forall a. Dict c a -> Dict d a) -> Dict (All c) xs -> Dict (All d) xs Source
Lifts a dictionary conversion over a type-level list.
mapAll2 :: forall c d xss. (forall a. Dict c a -> Dict d a) -> Dict (All2 c) xss -> Dict (All2 d) xss Source
Lifts a dictionary conversion over a type-level list of lists.
zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs Source
If two constraints c
and d
hold over a type-level
list xs
, then the combination of both constraints holds
over that list.
zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss Source
If two constraints c
and d
hold over a type-level
list of lists xss
, then the combination of both constraints
holds over that list of lists.
unAll_NP :: forall c xs. Dict (All c) xs -> NP (Dict c) xs Source
If we have a constraint c
that holds over a type-level
list xs
, we can create a product containing proofs that
each individual list element satisfies c
.
unAll_POP :: forall c xss. Dict (All2 c) xss -> POP (Dict c) xss Source
If we have a constraint c
that holds over a type-level
list of lists xss
, we can create a product of products
containing proofs that all the inner elements satisfy c
.
all_NP :: NP (Dict c) xs -> Dict (All c) xs Source
If we have a product containing proofs that each element
of xs
satisfies c
, then 'All c' holds for xs
.
all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss Source
If we have a product of products containing proofs that
each inner element of xss
satisfies c
, then 'All2 c'
holds for xss
.
unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss Source
The constraint 'All2 c' is convertible to 'All (All c)'.