Portability	non-portable
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>
Safe Haskell	Trustworthy

Data.Constraint

Contents

Constraints
Dictionary
Entailment
Reflection

Description

Synopsis

Constraints

data Constraint

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

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