| Copyright | (C) 2011-2015 Edward Kmett |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Data.Constraint
Description
ConstraintKinds
made type classes into types of a new kind,
Constraint
.
Eq:: * ->ConstraintOrd:: * ->ConstraintMonad:: (* -> *) ->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
- 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
- implied :: forall a b. (a => b) => a :- b
-
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 Source #
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(EqInt)
captures a dictionary that proves we have an:
instanceEqInt
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 Methods succ :: Dict a -> Dict a Source # pred :: Dict a -> Dict a Source # toEnum :: Int -> Dict a Source # fromEnum :: Dict a -> Int Source # enumFrom :: Dict a -> [ Dict a] Source # enumFromThen :: Dict a -> Dict a -> [ Dict a] Source # enumFromTo :: Dict a -> Dict a -> [ Dict a] Source # enumFromThenTo :: Dict a -> Dict a -> Dict a -> [ Dict a] Source # |
|
| Eq ( Dict a) Source # | |
| ( Typeable p, p) => Data ( Dict p) Source # | |
|
Defined in Data.Constraint Methods gfoldl :: ( forall d b. Data d => c (d -> b) -> d -> c b) -> ( forall g. g -> c g) -> Dict p -> c ( Dict p) Source # gunfold :: ( forall b r. Data b => c (b -> r) -> c r) -> ( forall r. r -> c r) -> Constr -> c ( Dict p) Source # toConstr :: Dict p -> Constr Source # dataTypeOf :: Dict p -> DataType Source # dataCast1 :: Typeable t => ( forall d. Data d => c (t d)) -> Maybe (c ( Dict p)) Source # dataCast2 :: Typeable t => ( forall d e. ( Data d, Data e) => c (t d e)) -> Maybe (c ( Dict p)) Source # gmapT :: ( forall b. Data b => b -> b) -> Dict p -> Dict p Source # gmapQl :: (r -> r' -> r) -> r -> ( forall d. Data d => d -> r') -> Dict p -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> ( forall d. Data d => d -> r') -> Dict p -> r Source # gmapQ :: ( forall d. Data d => d -> u) -> Dict p -> [u] Source # gmapQi :: Int -> ( forall d. Data d => d -> u) -> Dict p -> u Source # gmapM :: Monad m => ( forall d. Data d => d -> m d) -> Dict p -> m ( Dict p) Source # gmapMp :: MonadPlus m => ( forall d. Data d => d -> m d) -> Dict p -> m ( Dict p) Source # gmapMo :: MonadPlus m => ( forall d. Data d => d -> m d) -> Dict p -> m ( Dict p) Source # |
|
| Ord ( Dict a) Source # | |
| a => Read ( Dict a) Source # | |
| Show ( Dict a) Source # | |
| Semigroup ( Dict a) Source # | |
| a => Monoid ( Dict a) Source # | |
| NFData ( Dict c) Source # | |
|
Defined in Data.Constraint |
|
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 ::Dictc -> (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 Methods gfoldl :: ( forall d b. Data d => c (d -> b) -> d -> c b) -> ( forall g. g -> c g) -> (p :- q) -> c (p :- q) Source # gunfold :: ( forall b r. Data b => c (b -> r) -> c r) -> ( forall r. r -> c r) -> Constr -> c (p :- q) Source # toConstr :: (p :- q) -> Constr Source # dataTypeOf :: (p :- q) -> DataType Source # dataCast1 :: Typeable t => ( forall d. Data d => c (t d)) -> Maybe (c (p :- q)) Source # dataCast2 :: Typeable t => ( forall d e. ( Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) Source # gmapT :: ( forall b. Data b => b -> b) -> (p :- q) -> p :- q Source # gmapQl :: (r -> r' -> r) -> r -> ( forall d. Data d => d -> r') -> (p :- q) -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> ( forall d. Data d => d -> r') -> (p :- q) -> r Source # gmapQ :: ( forall d. Data d => d -> u) -> (p :- q) -> [u] Source # gmapQi :: Int -> ( forall d. Data d => d -> u) -> (p :- q) -> u Source # gmapM :: Monad m => ( forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) Source # gmapMp :: MonadPlus m => ( forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) Source # gmapMo :: MonadPlus m => ( forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) Source # |
|
| Ord (a :- b) Source # |
Assumes
|
|
Defined in Data.Constraint |
|
| Show (a :- b) Source # | |
| a => NFData (a :- b) Source # | |
|
Defined in Data.Constraint |
|
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.
implied :: forall a b. (a => b) => a :- b Source #
Convert a quantified constraint into an entailment.
Only available on GHC 8.6 or later.
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
instanceClass(Foo a) (Bar a) wherecls=SubDict
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] whereins=SubDict