Safe Haskell | None |
---|---|

Language | Haskell2010 |

Support for operating on Barbie-types with constrained functions.

Consider the following function:

showIt ::`Show`

a =>`Maybe`

a ->`Const`

`String`

a showIt =`Const`

.`show`

We would then like to be able to do:

`bmap`

`showIt`

::`FunctorB`

b => b`Maybe`

-> b (`Const`

`String`

)

This however doesn't work because of the `(`

constraint in the
the type of `Show`

a)`showIt`

.

This module adds support to overcome this problem.

- data DictOf c f a where
- PackedDict :: c (f a) => DictOf c f a

- packDict :: c (f a) => DictOf c f a
- requiringDict :: (c (f a) => r) -> DictOf c f a -> r
- class FunctorB b => ConstraintsB b where
- type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint

- class (ConstraintsB b, ProductB b) => ProofB b where

# Proof of instance

data DictOf c f a where Source #

is evidence that there exists an instance
of `DictOf`

c f a`c (f a)`

.

PackedDict :: c (f a) => DictOf c f a |

requiringDict :: (c (f a) => r) -> DictOf c f a -> r Source #

Turn a constrained-function into an unconstrained one that uses the packed instance dictionary instead.

# Retrieving proofs

class FunctorB b => ConstraintsB b Source #

Instances of this class provide means to talk about constraints,
both at compile-time, using `ConstraintsOf`

and at run-time,
in the form of class instance dictionaries, via `adjProof`

.

A manual definition would look like this:

data T f = A (f`Int`

) (f`String`

) | B (f`Bool`

) (f`Int`

) instance`ConstraintsB`

T where type`ConstraintsOf`

c f T = (c (f`Int`

), c (f`String`

), c (f`Bool`

)) adjProof t = case t of A x y -> A (`Pair`

(`packDict`

x) (`packDict`

y)) B z w -> B (`Pair`

(`packDict`

z) (`packDict`

w))

There is a default implementation of `ConstraintsOf`

for
`Generic`

types, so in practice one will simply do:

derive instance`Generic`

T instance`ConstraintsB`

T

type ConstraintsOf (c :: * -> Constraint) (f :: * -> *) b :: Constraint Source #

should contain a constraint `ConstraintsOf`

c f b`c (f x)`

for each `f x`

occurring in `b`

. E.g.:

`ConstraintsOf`

`Show`

f Barbie = (`Show`

(f`String`

),`Show`

(f`Int`

))

ConstraintsB b => ConstraintsB (Barbie b) Source # | |

class (ConstraintsB b, ProductB b) => ProofB b where Source #

Barbie-types with products have a canonical proof of instance.

There is a default `bproof`

implementation for `Generic`

types, so
instances can derived automatically.

bproof :: ConstraintsOf c f b => b (DictOf c f) Source #

bproof :: (CanDeriveGenericInstance b, ConstraintsOfMatchesGenericDeriv c f b, ConstraintsOf c f b) => b (DictOf c f) Source #