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 remains somewhat experimental. It is therefore not exported via the main module and has to be imported explicitly.

## Synopsis

- data Dict (c :: k -> Constraint) (a :: k) 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
- hdicts :: forall h c xs. (AllN h c xs, HPure h) => h (Dict c) xs

# Documentation

data Dict (c :: k -> Constraint) (a :: k) where Source #

pureAll :: SListI xs => Dict (All Top) xs Source #

A proof that the trivial constraint holds over all type-level lists.

*Since: 0.2*

pureAll2 :: All SListI xss => Dict (All2 Top) xss Source #

A proof that the trivial constraint holds over all type-level lists of lists.

*Since: 0.2*

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.

*Since: 0.2*

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.

*Since: 0.2*

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.

*Since: 0.2*

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.

*Since: 0.2*

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`

.

*Since: 0.2*

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`

.

*Since: 0.2*

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

holds for `All`

c`xs`

.

*Since: 0.2*

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

holds for `All2`

c`xss`

.

*Since: 0.2*