constraints-0.8: Constraint manipulation

Copyright(C) 2011-2015 Edward Kmett,
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Constraint

Contents

Description

ConstraintKinds made type classes into types of a new kind, Constraint.

Eq :: * -> Constraint
Ord :: * -> Constraint
Monad :: (* -> *) -> Constraint

The need for this extension was first publicized in the paper

Scrap your boilerplate with class: extensible generic functions

by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the things they needed into a custom Sat typeclass.

With ConstraintKinds we can put into code a lot of tools for manipulating these new types without such awkward workarounds.

Synopsis

The Kind of Constraints

data Constraint :: BOX

Instances

Category Constraint (:-)

Possible since GHC 7.8, when Category was made polykinded.

Dictionary

data Dict :: Constraint -> * where Source

Values of type Dict p capture a dictionary for a constraint of type 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.

Constructors

Dict :: a => Dict a 

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 
a => Bounded (Dict a) Source 
a => Enum (Dict a) Source 
Eq (Dict a) Source 
(Typeable Constraint p, p) => Data (Dict p) Source 
Ord (Dict a) Source 
a => Read (Dict a) Source 
Show (Dict a) Source 
a => Monoid (Dict a) Source 

Entailment

newtype a :- b infixr 9 Source

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only because 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 Ord a :- Eq [a], 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".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and them from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

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.

Constructors

Sub (a => Dict b) 

Instances

Category Constraint (:-) Source

Possible since GHC 7.8, when Category was made polykinded.

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

Assumes IncoherentInstances doesn't exist.

(Typeable Constraint p, Typeable Constraint q, p, q) => Data ((:-) p q) Source 
Ord ((:-) a b) Source

Assumes IncoherentInstances doesn't exist.

Show ((:-) a b) Source 

(\\) :: a => (b => r) -> (a :- b) -> r infixl 1 Source

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

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.

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

Transitivity of entailment

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

refl :: a :- a Source

Reflexivity of entailment

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

class Any => Bottom Source

Any inhabits every kind, including Constraint but is uninhabited, making it impossible to define an instance.

Minimal complete definition

no

top :: a :- () Source

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.

bottom :: Bottom :- a Source

This demonstrates the law of classical logic "ex falso quodlibet"

Dict is fully faithful

mapDict :: (a :- b) -> Dict a -> Dict b Source

Apply an entailment to a dictionary.

From a category theoretic perspective Dict is a functor that maps from the category of constraints (with arrows in :-) to the category Hask of Haskell data types.

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'

Methods

cls :: h :- b Source

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

Methods

ins :: b :- h Source

Instances

() :=> () Source 
a :=> (Monoid (Dict a)) Source 
a :=> (Read (Dict a)) Source 
a :=> (Bounded (Dict a)) Source 
a :=> (Enum (Dict a)) Source 
() :=> (Bounded Bool) Source 
() :=> (Bounded Char) Source 
() :=> (Bounded Int) Source 
() :=> (Bounded Ordering) Source 
() :=> (Bounded ()) Source 
() :=> (Enum Bool) Source 
() :=> (Enum Char) Source 
() :=> (Enum Double) Source 
() :=> (Enum Float) Source 
() :=> (Enum Int) Source 
() :=> (Enum Integer) Source 
() :=> (Enum Ordering) Source 
() :=> (Enum ()) Source 
() :=> (Eq Bool) Source 
() :=> (Eq Double) Source 
() :=> (Eq Float) Source 
() :=> (Eq Int) Source 
() :=> (Eq Integer) Source 
() :=> (Eq ()) Source 
() :=> (Eq ((:-) a b)) Source 
() :=> (Eq (Dict a)) Source 
() :=> (Floating Double) Source 
() :=> (Floating Float) Source 
() :=> (Fractional Double) Source 
() :=> (Fractional Float) Source 
() :=> (Integral Int) Source 
() :=> (Integral Integer) Source 
() :=> (Monad ((->) a)) Source 
() :=> (Monad []) Source 
() :=> (Monad IO) Source 
() :=> (Monad (Either a)) Source 
() :=> (Functor ((->) a)) Source 
() :=> (Functor []) Source 
() :=> (Functor IO) Source 
() :=> (Functor (Either a)) Source 
() :=> (Functor ((,) a)) Source 
() :=> (Functor Maybe) Source 
() :=> (Num Double) Source 
() :=> (Num Float) Source 
() :=> (Num Int) Source 
() :=> (Num Integer) Source 
() :=> (Ord Bool) Source 
() :=> (Ord Char) Source 
() :=> (Ord Double) Source 
() :=> (Ord Float) Source 
() :=> (Ord Int) Source 
() :=> (Ord Integer) Source 
() :=> (Ord ()) Source 
() :=> (Ord ((:-) a b)) Source 
() :=> (Ord (Dict a)) Source 
() :=> (Read Bool) Source 
() :=> (Read Char) Source 
() :=> (Read Ordering) Source 
() :=> (Read ()) Source 
() :=> (Real Double) Source 
() :=> (Real Float) Source 
() :=> (Real Int) Source 
() :=> (Real Integer) Source 
() :=> (RealFloat Double) Source 
() :=> (RealFloat Float) Source 
() :=> (RealFrac Double) Source 
() :=> (RealFrac Float) Source 
() :=> (Show Bool) Source 
() :=> (Show Char) Source 
() :=> (Show Ordering) Source 
() :=> (Show ()) Source 
() :=> (Show ((:-) a b)) Source 
() :=> (Show (Dict a)) Source 
() :=> (Applicative ((->) a)) Source 
() :=> (Applicative []) Source 
() :=> (Applicative IO) Source 
() :=> (Applicative (Either a)) Source 
() :=> (Applicative Maybe) Source 
() :=> (Monoid [a]) Source 
() :=> (Monoid Ordering) Source 
() :=> (Monoid ()) Source 
() :=> (Alternative []) Source 
() :=> (Alternative Maybe) Source 
() :=> (MonadPlus []) Source 
() :=> (MonadPlus Maybe) Source 
(:=>) b a => () :=> ((:=>) b a) Source 
Class b a => () :=> (Class b a) Source 
Class () ((:=>) b a) Source 
(Eq a) :=> (Eq (Ratio a)) Source 
(Eq a) :=> (Eq (Complex a)) Source 
(Eq a) :=> (Eq (Maybe a)) Source 
(Eq a) :=> (Eq [a]) Source 
(Integral a) :=> (RealFrac (Ratio a)) Source 
(Integral a) :=> (Fractional (Ratio a)) Source 
(Integral a) :=> (Real (Ratio a)) Source 
(Integral a) :=> (Num (Ratio a)) Source 
(Integral a) :=> (Enum (Ratio a)) Source 
(Integral a) :=> (Ord (Ratio a)) Source 
(Monad m) :=> (Applicative (WrappedMonad m)) Source 
(Monad m) :=> (Functor (WrappedMonad m)) Source 
(Ord a) :=> (Ord [a]) Source 
(Ord a) :=> (Ord (Maybe a)) Source 
(Read a) :=> (Read (Maybe a)) Source 
(Read a) :=> (Read [a]) Source 
(Read a) :=> (Read (Complex a)) Source 
(RealFloat a) :=> (Floating (Complex a)) Source 
(RealFloat a) :=> (Fractional (Complex a)) Source 
(RealFloat a) :=> (Num (Complex a)) Source 
(Show a) :=> (Show (Maybe a)) Source 
(Show a) :=> (Show [a]) Source 
(Show a) :=> (Show (Complex a)) Source 
(Monoid a) :=> (Applicative ((,) a)) Source 
(Monoid a) :=> (Monoid (Maybe a)) Source 
(MonadPlus m) :=> (Alternative (WrappedMonad m)) Source 
(Bounded a, Bounded b) :=> (Bounded (a, b)) Source 
(Eq a, Eq b) :=> (Eq (Either a b)) Source 
(Eq a, Eq b) :=> (Eq (a, b)) Source 
(Integral a, Read a) :=> (Read (Ratio a)) Source 
(Integral a, Show a) :=> (Show (Ratio a)) Source 
(Ord a, Ord b) :=> (Ord (Either a b)) Source 
(Ord a, Ord b) :=> (Ord (a, b)) Source 
(Read a, Read b) :=> (Read (Either a b)) Source 
(Read a, Read b) :=> (Read (a, b)) Source 
(Show a, Show b) :=> (Show (Either a b)) Source 
(Show a, Show b) :=> (Show (a, b)) Source 
(Monoid a, Monoid b) :=> (Monoid (a, b)) Source