Safe Haskell | None |
---|---|

Language | Haskell2010 |

This module exports various dictionaries that help the type-checker when dealing with row-types.

For the various axioms, type variables are consistently in the following order:

- Any types that do not belong later.
- Labels
Row-types

- If applicable, the type in the row-type at the given label goes after each row-type

- Constraints

## Synopsis

- uniqueMap :: forall f r. Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
- uniqueAp :: forall fs r. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
- uniqueApSingle :: forall x r. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
- uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
- extendHas :: forall l t r. Dict ((Extend l t r .! l) ≈ t)
- mapHas :: forall f l t r. ((r .! l) ≈ t) :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
- apHas :: forall l f ϕ t ρ. ((ϕ .! l) ≈ f, (ρ .! l) ≈ t) :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
- apSingleHas :: forall x l f r. ((r .! l) ≈ f) :- ((ApSingle r x .! l) ≈ f x, (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
- mapExtendSwap :: forall f ℓ τ r. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
- apExtendSwap :: forall ℓ f fs τ r. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
- apSingleExtendSwap :: forall τ ℓ f r. Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
- zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
- type FreeForall r = Forall r Unconstrained1
- type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2
- freeForall :: forall r c. Forall r c :- Forall r Unconstrained1
- mapForall :: forall f ρ c. Forall ρ c :- Forall (Map f ρ) (IsA c f)
- apSingleForall :: forall a fs c. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
- class IsA c f a where
- data As c f a where
- class ActsOn c t a where
- data As' c t a where
- data Dict a where
- newtype a :- b = Sub (a -> Dict b)
- class HasDict c e | e -> c where
- (\\) :: HasDict c e => (c -> r) -> e -> r
- withDict :: HasDict c e => e -> (c -> r) -> r
- class Unconstrained
- class Unconstrained1 a
- class Unconstrained2 a b

# Axioms

uniqueMap :: forall f r. Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r) Source #

Map preserves uniqueness of labels.

uniqueAp :: forall fs r. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r) Source #

Ap preserves uniqueness of labels.

uniqueApSingle :: forall x r. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r) Source #

ApSingle preserves uniqueness of labels.

uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2)) Source #

Zip preserves uniqueness of labels.

extendHas :: forall l t r. Dict ((Extend l t r .! l) ≈ t) Source #

If we know that `r`

has been extended with `l .== t`

, then we know that this
extension at the label `l`

must be `t`

.

mapHas :: forall f l t r. ((r .! l) ≈ t) :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)) Source #

This allows us to derive `Map f r .! l ≈ f t`

from `r .! l ≈ t`

apHas :: forall l f ϕ t ρ. ((ϕ .! l) ≈ f, (ρ .! l) ≈ t) :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)) Source #

This allows us to derive `Ap ϕ ρ .! l ≈ f t`

from `ϕ .! l ≈ f`

and `ρ .! l ≈ t`

apSingleHas :: forall x l f r. ((r .! l) ≈ f) :- ((ApSingle r x .! l) ≈ f x, (ApSingle r x .- l) ≈ ApSingle (r .- l) x) Source #

This allows us to derive `ApSingle r x .! l ≈ f x`

from `r .! l ≈ f`

mapExtendSwap :: forall f ℓ τ r. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r)) Source #

Proof that the `Map`

type family preserves labels and their ordering.

apExtendSwap :: forall ℓ f fs τ r. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r)) Source #

Proof that the `Ap`

type family preserves labels and their ordering.

apSingleExtendSwap :: forall τ ℓ f r. Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ) Source #

Proof that the `ApSingle`

type family preserves labels and their ordering.

zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2)) Source #

Proof that the `Ap`

type family preserves labels and their ordering.

type FreeForall r = Forall r Unconstrained1 Source #

`FreeForall`

can be used when a `Forall`

constraint is necessary but there
is no particular constraint we care about.

type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2 Source #

`FreeForall`

can be used when a `BiForall`

constraint is necessary but
there is no particular constraint we care about.

freeForall :: forall r c. Forall r c :- Forall r Unconstrained1 Source #

Allow any `Forall`

over a row-type, be usable for `Unconstrained1`

.

mapForall :: forall f ρ c. Forall ρ c :- Forall (Map f ρ) (IsA c f) Source #

This allows us to derive a `Forall (Map f r) ..`

from a `Forall r ..`

.

apSingleForall :: forall a fs c. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a) Source #

This allows us to derive a `Forall (ApSingle f r) ..`

from a `Forall f ..`

.

## Helper Types

class IsA c f a where Source #

A class to capture the idea of `As`

so that it can be partially applied in
a context.

## Instances

c a => IsA (c :: k2 -> Constraint) (f :: k2 -> k1) (f a :: k1) Source # | |

Defined in Data.Row.Dictionaries |

This data type is used to for its ability to existentially bind a type
variable. Particularly, it says that for the type `a`

, there exists a `t`

such that `a ~ f t`

and `c t`

holds.

class ActsOn c t a where Source #

A class to capture the idea of `As'`

so that it can be partially applied in
a context.

## Instances

c f => ActsOn (c :: (k1 -> k2) -> Constraint) (t :: k1) (f t :: k2) Source # | |

Defined in Data.Row.Dictionaries |

Like `As`

, but here we know the underlying value is some `f`

applied to the
given type `a`

.

# Re-exports

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

HasDict a (Dict a) | |

Defined in Data.Constraint | |

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

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

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

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

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

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

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

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

a => Bounded (Dict a) | |

a => Enum (Dict a) | |

Defined in Data.Constraint | |

Eq (Dict a) | |

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

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) | |

a => Read (Dict a) | |

Show (Dict a) | |

Semigroup (Dict a) | |

a => Monoid (Dict a) | |

NFData (Dict c) | |

Defined in Data.Constraint |

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 (:-) | Possible since GHC 7.8, when |

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

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

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

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

Defined in Data.Constraint | |

Eq (a :- b) | Assumes |

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

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) | Assumes |

Defined in Data.Constraint | |

Show (a :- b) | |

a => NFData (a :- b) | |

Defined in Data.Constraint |

class HasDict c e | e -> c where #

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.

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

Operator version of `withDict`

, with the arguments flipped

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

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

class Unconstrained Source #

A null constraint

## Instances

Unconstrained Source # | |

Defined in Data.Row.Internal |

class Unconstrained1 a Source #

A null constraint of one argument

## Instances

Unconstrained1 (a :: k) Source # | |

Defined in Data.Row.Internal |

class Unconstrained2 a b Source #

A null constraint of two arguments

## Instances

Unconstrained2 (a :: k2) (b :: k1) Source # | |

Defined in Data.Row.Internal |