constraints-0.4: Constraint manipulation

Portability non-portable experimental Edward Kmett Trustworthy

Data.Constraint

Contents

Description

Synopsis

# Dictionary

data Dict whereSource

Capture a dictionary for a given constraint

Constructors

 Dict :: a => Dict a

Instances

 a :=> (Monoid (Dict a)) a :=> (Read (Dict a)) a :=> (Bounded (Dict a)) a :=> (Enum (Dict a)) () :=> (Eq (Dict a)) () :=> (Ord (Dict a)) () :=> (Show (Dict a)) a => Bounded (Dict a) a => Enum (Dict a) Eq (Dict a) Ord (Dict a) a => Read (Dict a) Show (Dict a) a => Monoid (Dict a)

# Entailment

newtype a :- b Source

Constructors

 Sub (a => Dict b)

Instances

 () :=> (Eq (:- a b)) () :=> (Ord (:- a b)) () :=> (Show (:- a b)) Eq (:- a b) Ord (:- a b) Show (:- a b)

(\\) :: a => (b => r) -> (a :- b) -> rSource

Given that `a :- b`, derive something that needs a context `b`, using the context `a`

weaken1 :: (a, b) :- aSource

Weakening a constraint product

weaken2 :: (a, b) :- bSource

Weakening a constraint product

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

Contracting a constraint / diagonal morphism

(&&&) :: (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

trans :: (b :- c) -> (a :- b) -> a :- cSource

Transitivity of entailment

If we view '(:-)' as a Constraint-indexed category, then this is '(.)'

refl :: a :- aSource

Reflexivity of entailment

If we view '(:-)' as a Constraint-indexed category, then this is `id`

top :: a :- ()Source

Every constraint implies truth

These are the terminal arrows of the category, and () is the terminal object.

bottom :: (() ~ Bool) :- cSource

A bad type coercion lets you derive any type you want.

These are the initial arrows of the category and (() ~ Bool) is the initial object

This demonstrates the law of classical logical ex falso quodlibet

# Reflection

class Class b h | h -> b whereSource

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

Methods

cls :: h :- bSource

Instances

 Class () () Class () (Bounded a) Class () (Enum a) Class () (Eq a) Class () (Monad f) Class () (Functor f) Class () (Num a) Class () (Read a) Class () (Show a) Class () (Monoid a) Class () (:=> b a) Class () (Class b a) Class (Eq a) (Ord a) Class (Fractional a) (Floating a) Class (Monad f) (MonadPlus f) Class (Functor f) (Applicative f) Class (Num a) (Fractional a) Class (Applicative f) (Alternative f) Class (Num a, Ord a) (Real a) Class (Real a, Fractional a) (RealFrac a) Class (Real a, Enum a) (Integral a) Class (RealFrac a, Floating a) (RealFloat a)

class b :=> h | h -> b whereSource

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

Methods

ins :: b :- hSource

Instances