Data.Row.Dictionaries

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

Axioms

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

Map preserves uniqueness of labels.

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

Ap preserves uniqueness of labels.

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

ApSingle preserves uniqueness of labels.

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

Zip preserves uniqueness of labels.

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

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

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

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)

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

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

Proof that the Ap type family preserves labels and their ordering.

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

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

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

Map distributes over MinJoin

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

ApSingle distributes over MinJoin

type FreeForall r = Forall r Unconstrained1

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

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

Allow any Forall over a row-type, be usable for Unconstrained1.

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

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)

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)

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)

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

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

Subset is transitive

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

Map distributes over Difference

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

ApSingle distributes over Difference

Helper Types

class IsA c f a where

A class to capture the idea of As so that it can be partially applied in a context.

Methods

as :: As c f a

Instances

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

Defined in Data.Row.Dictionaries

Methods

as :: As c f (f a)

data As c f a where

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

A class to capture the idea of As' so that it can be partially applied in a context.

Methods

actsOn :: As' c t a

Instances

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

Defined in Data.Row.Dictionaries

Methods

actsOn :: As' c t (f t)

data As' c t a where

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

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

HasDict a (Dict a)

Defined in Data.Constraint

Methods

evidence :: Dict a -> Dict a

a :=> (Read (Dict a))

Defined in Data.Constraint

Methods

ins :: a :- Read (Dict a)

a :=> (Monoid (Dict a))

Defined in Data.Constraint

Methods

ins :: a :- Monoid (Dict a)

a :=> (Enum (Dict a))

Defined in Data.Constraint

Methods

ins :: a :- Enum (Dict a)

a :=> (Bounded (Dict a))

Defined in Data.Constraint

Methods

ins :: a :- Bounded (Dict a)

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

Defined in Data.Constraint

Methods

ins :: () :- Eq (Dict a)

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

Defined in Data.Constraint

Methods

ins :: () :- Ord (Dict a)

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

Defined in Data.Constraint

Methods

ins :: () :- Show (Dict a)

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

Defined in Data.Constraint

Methods

ins :: () :- Semigroup (Dict a)

a => Bounded (Dict a)

Defined in Data.Constraint

Methods

minBound :: Dict a

maxBound :: Dict a

a => Enum (Dict a)

Defined in Data.Constraint

Methods

succ :: Dict a -> Dict a

pred :: Dict a -> Dict a

toEnum :: Int -> Dict a

fromEnum :: Dict a -> Int

enumFrom :: Dict a -> [Dict a]

enumFromThen :: Dict a -> Dict a -> [Dict a]

enumFromTo :: Dict a -> Dict a -> [Dict a]

enumFromThenTo :: Dict a -> Dict a -> Dict a -> [Dict a]

Eq (Dict a)

Defined in Data.Constraint

Methods

(==) :: Dict a -> Dict a -> Bool

(/=) :: Dict a -> Dict a -> Bool

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

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)

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 :: forall r r'. (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)

Defined in Data.Constraint

Methods

compare :: Dict a -> Dict a -> Ordering

(<) :: Dict a -> Dict a -> Bool

(<=) :: Dict a -> Dict a -> Bool

(>) :: Dict a -> Dict a -> Bool

(>=) :: Dict a -> Dict a -> Bool

max :: Dict a -> Dict a -> Dict a

min :: Dict a -> Dict a -> Dict a

a => Read (Dict a)

Defined in Data.Constraint

Methods

readsPrec :: Int -> ReadS (Dict a)

readList :: ReadS [Dict a]

readPrec :: ReadPrec (Dict a)

readListPrec :: ReadPrec [Dict a]

Show (Dict a)

Defined in Data.Constraint

Methods

showsPrec :: Int -> Dict a -> ShowS

show :: Dict a -> String

showList :: [Dict a] -> ShowS

Semigroup (Dict a)

Defined in Data.Constraint

Methods

(<>) :: Dict a -> Dict a -> Dict a

sconcat :: NonEmpty (Dict a) -> Dict a

stimes :: Integral b => b -> Dict a -> Dict a

a => Monoid (Dict a)

Defined in Data.Constraint

Methods

mempty :: Dict a

mappend :: Dict a -> Dict a -> Dict a

mconcat :: [Dict a] -> Dict a

NFData (Dict c)

Defined in Data.Constraint

Methods

rnf :: Dict c -> ()

newtype a :- b infixr 9

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

Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

Defined in Data.Constraint

Methods

id :: forall (a :: k). a :- a

(.) :: forall (b :: k) (c :: k) (a :: k). (b :- c) -> (a :- b) -> a :- c

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

Defined in Data.Constraint

Methods

ins :: () :- Eq (a :- b)

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

Defined in Data.Constraint

Methods

ins :: () :- Ord (a :- b)

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

Defined in Data.Constraint

Methods

ins :: () :- Show (a :- b)

a => HasDict b (a :- b)

Defined in Data.Constraint

Methods

evidence :: (a :- b) -> Dict b

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Defined in Data.Constraint

Methods

(==) :: (a :- b) -> (a :- b) -> Bool

(/=) :: (a :- b) -> (a :- b) -> Bool

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

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)

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 :: forall r r'. (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 IncoherentInstances doesn't exist.

Defined in Data.Constraint

Methods

compare :: (a :- b) -> (a :- b) -> Ordering

(<) :: (a :- b) -> (a :- b) -> Bool

(<=) :: (a :- b) -> (a :- b) -> Bool

(>) :: (a :- b) -> (a :- b) -> Bool

(>=) :: (a :- b) -> (a :- b) -> Bool

max :: (a :- b) -> (a :- b) -> a :- b

min :: (a :- b) -> (a :- b) -> a :- b

Show (a :- b)

Defined in Data.Constraint

Methods

showsPrec :: Int -> (a :- b) -> ShowS

show :: (a :- b) -> String

showList :: [a :- b] -> ShowS

a => NFData (a :- b)

Defined in Data.Constraint

Methods

rnf :: (a :- b) -> ()

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.

Methods

evidence :: e -> Dict c

Instances

HasDict a (Dict a)

Defined in Data.Constraint

Methods

evidence :: Dict a -> Dict a

a => HasDict b (a :- b)

Defined in Data.Constraint

Methods

evidence :: (a :- b) -> Dict b

HasDict (Typeable k, Typeable a) (TypeRep a)

Defined in Data.Constraint

Methods

evidence :: TypeRep a -> Dict (Typeable k, Typeable a)

HasDict (a ~ b) (a :~: b)

Defined in Data.Constraint

Methods

evidence :: (a :~: b) -> Dict (a ~ b)

HasDict (Coercible a b) (Coercion a b)

Defined in Data.Constraint

Methods

evidence :: Coercion a b -> Dict (Coercible a b)

HasDict (a ~~ b) (a :~~: b)

Defined in Data.Constraint

Methods

evidence :: (a :~~: b) -> Dict (a ~~ b)

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

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

class Unconstrained

A null constraint

Instances

Unconstrained

Defined in Data.Row.Internal

class Unconstrained1 a

A null constraint of one argument

Instances

Unconstrained1 (a :: k)

Defined in Data.Row.Internal

class Unconstrained2 a b

A null constraint of two arguments

Instances

Unconstrained2 (a :: k1) (b :: k2)

Defined in Data.Row.Internal