Safe Haskell	None
Language	Haskell2010

Data.SOP.Dict

Description

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
- Dict :: c a => Dict c a
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 #

An explicit dictionary carrying evidence of a class constraint.

The constraint parameter is separated into a second argument so that Dict c is of the correct kind to be used directly as a parameter to e.g. NP.

Since: 0.2

Constructors

Dict :: c a => Dict c a

Instances

Instances details

Show (Dict c a) Source #
Instance details Defined in Data.SOP.Dict Methods showsPrec :: Int -> Dict c a -> ShowS # show :: Dict c a -> String # showList :: [Dict c a] -> ShowS #

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 All c holds for 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 All2 c holds for xss.

Since: 0.2

unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss Source #

Deprecated: 'All2 c' is now a synonym of 'All (All c)'

The constraint All2 c is convertible to All (All c).

Since: 0.2

all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss Source #

Deprecated: 'All2 c' is now a synonym of 'All (All c)'

The constraint All (All c) is convertible to All2 c.

Since: 0.2

withDict :: Dict c a -> (c a => r) -> r Source #

If we have an explicit dictionary, we can unwrap it and pass a function that makes use of it.

Since: 0.2

hdicts :: forall h c xs. (AllN h c xs, HPure h) => h (Dict c) xs Source #

A structure of dictionaries.

Since: 0.2.3.0