Safe Haskell	None
Language	Haskell2010

Data.Row.Dictionaries

Contents

Axioms
- Helper Types
Re-exports

Description

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))
mapMinJoin :: forall f r r'. Dict (( Map f r .\/ Map f r') ≈ Map f (r .\/ r'))
apSingleMinJoin :: forall r r' x. Dict (( ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x)
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)
subsetJoin :: forall r1 r2 s. Dict (( Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s)
subsetJoin' :: forall r1 r2 s. Dict (( Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s)
subsetRestrict :: forall r s l. Subset r s :- Subset (r .- l) s
subsetTrans :: forall r1 r2 r3. ( Subset r1 r2, Subset r2 r3) :- Subset r1 r3
mapDifference :: forall f r r'. Dict (( Map f r .\\ Map f r') ≈ Map f (r .\\ r'))
apSingleDifference :: forall r r' x. Dict (( ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x)
class IsA c f a where
- as :: As c f a
data As c f a where
- As :: forall c f a t. (a ~ f t, c t) => As c f a
class ActsOn c t a where
- actsOn :: As' c t a
data As' c t a where
- As' :: forall c f a t. (a ~ f t, c f) => As' c t a
data Dict a where
- Dict :: forall a. a => Dict a
newtype a :- b = Sub (a => Dict b)
class HasDict c e | e -> c where
- evidence :: e -> Dict c
(\\) :: 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.

mapMinJoin :: forall f r r'. Dict (( Map f r .\/ Map f r') ≈ Map f (r .\/ r')) Source #

Map distributes over MinJoin

apSingleMinJoin :: forall r r' x. Dict (( ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x) Source #

ApSingle distributes over MinJoin

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

subsetJoin :: forall r1 r2 s. Dict (( Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s) Source #

Two rows are subsets of a third if and only if their disjoint union is a subset of that third.

subsetJoin' :: forall r1 r2 s. Dict (( Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s) Source #

If two rows are each subsets of a third, their join is a subset of the third

subsetRestrict :: forall r s l. Subset r s :- Subset (r .- l) s Source #

If a row is a subset of another, then its restriction is also a subset of the other

subsetTrans :: forall r1 r2 r3. ( Subset r1 r2, Subset r2 r3) :- Subset r1 r3 Source #

Subset is transitive

mapDifference :: forall f r r'. Dict (( Map f r .\\ Map f r') ≈ Map f (r .\\ r')) Source #

Map distributes over Difference

apSingleDifference :: forall r r' x. Dict (( ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x) Source #

ApSingle distributes over Difference

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.

Methods

as :: As c f a Source #

Instances

Instances details

c a => IsA (c :: k1 -> Constraint ) (f :: k1 -> k2) (f a :: k2) Source #
Instance details Defined in Data.Row.Dictionaries Methods as :: As c f (f a) Source #

data As c f a where Source #

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.

Constructors

As :: forall c f a t. (a ~ f t, c t) => As c f a

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.

Methods

actsOn :: As' c t a Source #

Instances

Instances details

c f => ActsOn (c :: (k1 -> k2) -> Constraint ) (t :: k1) (f t :: k2) Source #
Instance details Defined in Data.Row.Dictionaries Methods actsOn :: As' c t (f t) Source #

data As' c t a where Source #

Like As , but here we know the underlying value is some f applied to the given type a .

Constructors

As' :: forall c f a t. (a ~ f t, c f) => As' c t a

Re-exports

data Dict a 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 :: forall a. a => Dict a

Instances

Instances details

HasDict a ( Dict a)
Instance details Defined in Data.Constraint Methods evidence :: Dict a -> Dict a Source #
a :=> ( Read ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Read ( Dict a) Source #
a :=> ( Monoid ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Monoid ( Dict a) Source #
a :=> ( Enum ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Enum ( Dict a) Source #
a :=> ( Bounded ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: a :- Bounded ( Dict a) Source #
() :=> ( Eq ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Eq ( Dict a) Source #
() :=> ( Ord ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Ord ( Dict a) Source #
() :=> ( Show ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Show ( Dict a) Source #
() :=> ( Semigroup ( Dict a))
Instance details Defined in Data.Constraint Methods ins :: () :- Semigroup ( Dict a) Source #
a => Bounded ( Dict a)
Instance details Defined in Data.Constraint Methods minBound :: Dict a Source # maxBound :: Dict a Source #
a => Enum ( Dict a)
Instance details 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)
Instance details Defined in Data.Constraint Methods (==) :: Dict a -> Dict a -> Bool Source # (/=) :: Dict a -> Dict a -> Bool Source #
( Typeable p, p) => Data ( Dict p)
Instance details 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)
Instance details Defined in Data.Constraint Methods compare :: Dict a -> Dict a -> Ordering Source # (<) :: Dict a -> Dict a -> Bool Source # (<=) :: Dict a -> Dict a -> Bool Source # (>) :: Dict a -> Dict a -> Bool Source # (>=) :: Dict a -> Dict a -> Bool Source # max :: Dict a -> Dict a -> Dict a Source # min :: Dict a -> Dict a -> Dict a Source #
a => Read ( Dict a)
Instance details Defined in Data.Constraint Methods readsPrec :: Int -> ReadS ( Dict a) Source # readList :: ReadS [ Dict a] Source # readPrec :: ReadPrec ( Dict a) Source # readListPrec :: ReadPrec [ Dict a] Source #
Show ( Dict a)
Instance details Defined in Data.Constraint Methods showsPrec :: Int -> Dict a -> ShowS Source # show :: Dict a -> String Source # showList :: [ Dict a] -> ShowS Source #
Semigroup ( Dict a)
Instance details Defined in Data.Constraint Methods (<>) :: Dict a -> Dict a -> Dict a Source # sconcat :: NonEmpty ( Dict a) -> Dict a Source # stimes :: Integral b => b -> Dict a -> Dict a Source #
a => Monoid ( Dict a)
Instance details Defined in Data.Constraint Methods mempty :: Dict a Source # mappend :: Dict a -> Dict a -> Dict a Source # mconcat :: [ Dict a] -> Dict a Source #
NFData ( Dict c)
Instance details Defined in Data.Constraint Methods rnf :: Dict c -> () Source #

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

Instances details

Category (:-)	Possible since GHC 7.8, when `Category` was made polykinded.
Instance details Defined in Data.Constraint Methods id :: forall (a :: k). a :- a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :- c) -> (a :- b) -> a :- c Source #
() :=> ( Eq (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Eq (a :- b) Source #
() :=> ( Ord (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Ord (a :- b) Source #
() :=> ( Show (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Show (a :- b) Source #
a => HasDict b (a :- b)
Instance details Defined in Data.Constraint Methods evidence :: (a :- b) -> Dict b Source #
Eq (a :- b)	Assumes `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods (==) :: (a :- b) -> (a :- b) -> Bool Source # (/=) :: (a :- b) -> (a :- b) -> Bool Source #
( Typeable p, Typeable q, p, q) => Data (p :- q)
Instance details 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)	Assumes `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods compare :: (a :- b) -> (a :- b) -> Ordering Source # (<) :: (a :- b) -> (a :- b) -> Bool Source # (<=) :: (a :- b) -> (a :- b) -> Bool Source # (>) :: (a :- b) -> (a :- b) -> Bool Source # (>=) :: (a :- b) -> (a :- b) -> Bool Source # max :: (a :- b) -> (a :- b) -> a :- b Source # min :: (a :- b) -> (a :- b) -> a :- b Source #
Show (a :- b)
Instance details Defined in Data.Constraint Methods showsPrec :: Int -> (a :- b) -> ShowS Source # show :: (a :- b) -> String Source # showList :: [a :- b] -> ShowS Source #
a => NFData (a :- b)
Instance details Defined in Data.Constraint Methods rnf :: (a :- b) -> () Source #

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.

Methods

evidence :: e -> Dict c Source #

Instances

Instances details

HasDict a ( Dict a)
Instance details Defined in Data.Constraint Methods evidence :: Dict a -> Dict a Source #
a => HasDict b (a :- b)
Instance details Defined in Data.Constraint Methods evidence :: (a :- b) -> Dict b Source #
HasDict ( Typeable k, Typeable a) ( TypeRep a)
Instance details Defined in Data.Constraint Methods evidence :: TypeRep a -> Dict ( Typeable k, Typeable a) Source #
HasDict (a ~ b) (a :~: b)
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #
HasDict ( Coercible a b) ( Coercion a b)
Instance details Defined in Data.Constraint Methods evidence :: Coercion a b -> Dict ( Coercible a b) Source #
HasDict (a ~~ b) (a :~~: b)
Instance details Defined in Data.Constraint Methods evidence :: (a :~~: b) -> Dict (a ~~ b) Source #

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

Operator version of withDict , with the arguments flipped

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 :- b , using a context a .

withDict :: Dict c -> (c => r) -> r
withDict :: a => (a :- c) -> (c => r) -> r

class Unconstrained Source #

A null constraint

Instances

Instances details

Unconstrained Source #
Instance details Defined in Data.Row.Internal

class Unconstrained1 a Source #

A null constraint of one argument

Instances

Instances details

Unconstrained1 (a :: k) Source #
Instance details Defined in Data.Row.Internal

class Unconstrained2 a b Source #

A null constraint of two arguments

Instances

Instances details

Unconstrained2 (a :: k1) (b :: k2) Source #
Instance details Defined in Data.Row.Internal