Copyright | (C) 2011-2015 Edward Kmett |
---|---|

License | BSD-style (see the file LICENSE) |

Stability | experimental |

Portability | non-portable |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

This module is taken from constraints:Data.Constraint A few things have been cut from the module to remove dependencies.

## Synopsis

- data Constraint
- data Dict :: Constraint -> * where
- class HasDict c e | e -> c where
- withDict :: HasDict c e => e -> (c => r) -> r
- (\\) :: HasDict c e => (c => r) -> e -> r
- newtype a :- b = Sub (a => Dict b)
- type (⊢) = (:-)
- weaken1 :: (a, b) :- a
- weaken2 :: (a, b) :- b
- contract :: a :- (a, a)
- strengthen1 :: Dict b -> (a :- c) -> a :- (b, c)
- strengthen2 :: Dict b -> (a :- c) -> a :- (c, b)
- (&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)
- (***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
- trans :: (b :- c) -> (a :- b) -> a :- c
- refl :: a :- a
- class Any => Bottom where
- no :: a

- top :: a :- ()
- bottom :: Bottom :- a
- mapDict :: (a :- b) -> Dict a -> Dict b
- unmapDict :: (Dict a -> Dict b) -> a :- b
- class Class b h | h -> b where
- class b :=> h | h -> b where

# The Kind of Constraints

data Constraint #

The kind of constraints, like `Show a`

# Dictionary

data Dict :: Constraint -> * where Source #

Values of type

capture a dictionary for a constraint of type `Dict`

p`p`

.

e.g.

`Dict`

::`Dict`

(`Eq`

`Int`

)

captures a dictionary that proves we have an:

`instance ``Eq`

'Int

Pattern matching on the `Dict`

constructor will bring this instance into scope.

## Instances

a :=> (Monoid (Dict a)) Source # | |

a :=> (Read (Dict a)) Source # | |

a :=> (Bounded (Dict a)) Source # | |

a :=> (Enum (Dict a)) Source # | |

() :=> (Eq (Dict a)) Source # | |

() :=> (Ord (Dict a)) Source # | |

() :=> (Show (Dict a)) Source # | |

() :=> (Semigroup (Dict a)) Source # | |

HasDict a (Dict a) Source # | |

a => Bounded (Dict a) Source # | |

a => Enum (Dict a) Source # | |

Defined in Data.Constraint | |

Eq (Dict a) Source # | |

(Typeable p, p) => Data (Dict p) Source # | |

Defined in Data.Constraint gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict p -> c (Dict p) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict p) # toConstr :: Dict p -> Constr # dataTypeOf :: Dict p -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dict p)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict p)) # gmapT :: (forall b. Data b => b -> b) -> Dict p -> Dict p # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r # gmapQ :: (forall d. Data d => d -> u) -> Dict p -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict p -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) # | |

Ord (Dict a) Source # | |

a => Read (Dict a) Source # | |

Show (Dict a) Source # | |

Semigroup (Dict a) Source # | |

a => Monoid (Dict a) Source # | |

class HasDict c e | e -> c where Source #

Witnesses that a value of type `e`

contains evidence of the constraint `c`

.

Mainly intended to allow (`\\`

) to be overloaded, since it's a useful operator.

withDict :: HasDict c e => e -> (c => r) -> r Source #

From a `Dict`

, takes a value in an environment where the instance
witnessed by the `Dict`

is in scope, and evaluates it.

Essentially a deconstruction of a `Dict`

into its continuation-style
form.

Can also be used to deconstruct an entailment, `a `

, using a context `:-`

b`a`

.

withDict ::`Dict`

c -> (c => r) -> r withDict :: a => (a`:-`

c) -> (c => r) -> r

(\\) :: HasDict c e => (c => r) -> e -> r infixl 1 Source #

Operator version of `withDict`

, with the arguments flipped

# Entailment

newtype a :- b infixr 9 Source #

This is the type of entailment.

`a `

is read as `:-`

b`a`

"entails" `b`

.

With this we can actually build a category for `Constraint`

resolution.

e.g.

Because

is a superclass of `Eq`

a

, we can show that `Ord`

a

entails `Ord`

a

.`Eq`

a

Because `instance `

exists, we can show that `Ord`

a => `Ord`

[a]

entails `Ord`

a

as well.`Ord`

[a]

This relationship is captured in the `:-`

entailment type here.

Since `p `

and entailment composes, `:-`

p`:-`

forms the arrows of a
`Category`

of constraints. However, `Category`

only became sufficiently
general to support this instance in GHC 7.8, so prior to 7.8 this instance
is unavailable.

But due to the coherence of instance resolution in Haskell, this `Category`

has some very interesting properties. Notably, in the absence of
`IncoherentInstances`

, this category is "thin", which is to say that
between any two objects (constraints) there is at most one distinguishable
arrow.

This means that for instance, even though there are two ways to derive

, the answers from these two paths _must_ by
construction be equal. This is a property that Haskell offers that is
pretty much unique in the space of languages with things they call "type
classes".`Ord`

a `:-`

`Eq`

[a]

What are the two ways?

Well, we can go from

via the
superclass relationship, and then from `Ord`

a `:-`

`Eq`

a

via the
instance, or we can go from `Eq`

a `:-`

`Eq`

[a]

via the instance
then from `Ord`

a `:-`

`Ord`

[a]

through the superclass relationship
and this diagram by definition must "commute".`Ord`

[a] `:-`

`Eq`

[a]

Diagrammatically,

Ord a ins / \ cls v v Ord [a] Eq a cls \ / ins v v Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

## Instances

Category (:-) Source # | Possible since GHC 7.8, when |

() :=> (Eq (a :- b)) Source # | |

() :=> (Ord (a :- b)) Source # | |

() :=> (Show (a :- b)) Source # | |

a => HasDict b (a :- b) Source # | |

Eq (a :- b) Source # | Assumes |

(Typeable p, Typeable q, p, q) => Data (p :- q) Source # | |

Defined in Data.Constraint gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) # toConstr :: (p :- q) -> Constr # dataTypeOf :: (p :- q) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) # gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # | |

Ord (a :- b) Source # | Assumes |

Defined in Data.Constraint | |

Show (a :- b) Source # | |

weaken1 :: (a, b) :- a Source #

Weakening a constraint product

The category of constraints is Cartesian. We can forget information.

weaken2 :: (a, b) :- b Source #

Weakening a constraint product

The category of constraints is Cartesian. We can forget information.

contract :: a :- (a, a) Source #

Contracting a constraint / diagonal morphism

The category of constraints is Cartesian. We can reuse information.

(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c) Source #

Constraint product

trans weaken1 (f &&& g) = f trans weaken2 (f &&& g) = g

(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d) Source #

due to the hack for the kind of `(,)`

in the current version of GHC we can't actually
make instances for `(,) :: Constraint -> Constraint -> Constraint`

, but `(,)`

is a
bifunctor on the category of constraints. This lets us map over both sides.

class Any => Bottom where Source #

`Any`

inhabits every kind, including `Constraint`

but is uninhabited, making it impossible to define an instance.

Every constraint implies truth

These are the terminal arrows of the category, and `()`

is the terminal object.

Given any constraint there is a unique entailment of the `()`

constraint from that constraint.

# Dict is fully faithful

unmapDict :: (Dict a -> Dict b) -> a :- b Source #

This functor is fully faithful, which is to say that given any function you can write
`Dict a -> Dict b`

there also exists an entailment `a :- b`

in the category of constraints
that you can build.

# Reflection

class Class b h | h -> b where Source #

Reify the relationship between a class and its superclass constraints as a class

Given a definition such as

class Foo a => Bar a

you can capture the relationship between 'Bar a' and its superclass 'Foo a' with

instance`Class`

(Foo a) (Bar a) where`cls`

=`Sub`

`Dict`

Now the user can use 'cls :: Bar a :- Foo a'

## Instances

class b :=> h | h -> b where infixr 9 Source #

Reify the relationship between an instance head and its body as a class

Given a definition such as

instance Foo a => Foo [a]

you can capture the relationship between the instance head and its body with

instance Foo a`:=>`

Foo [a] where`ins`

=`Sub`

`Dict`