row-types-1.0.1.0: Open Records and Variants
Safe HaskellNone
LanguageHaskell2010

Data.Row.Dictionaries

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

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

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 #

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 #

a :=> (Read (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Read (Dict a) #

a :=> (Monoid (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Monoid (Dict a) #

a :=> (Enum (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Enum (Dict a) #

a :=> (Bounded (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Bounded (Dict a) #

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

a => Bounded (Dict a) 
Instance details

Defined in Data.Constraint

Methods

minBound :: Dict a #

maxBound :: Dict a #

a => Enum (Dict a) 
Instance details

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

Defined in Data.Constraint

Methods

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

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

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

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

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

Defined in Data.Constraint

Show (Dict a) 
Instance details

Defined in Data.Constraint

Methods

showsPrec :: Int -> Dict a -> ShowS #

show :: Dict a -> String #

showList :: [Dict a] -> ShowS #

Semigroup (Dict a) 
Instance details

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

Defined in Data.Constraint

Methods

mempty :: Dict a #

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

mconcat :: [Dict a] -> Dict a #

NFData (Dict c) 
Instance details

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

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 #

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

a => HasDict b (a :- b) 
Instance details

Defined in Data.Constraint

Methods

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

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

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

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

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

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.

Instance details

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

Defined in Data.Constraint

Methods

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

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

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

a => NFData (a :- b) 
Instance details

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

Instances details
HasDict a (Dict a) 
Instance details

Defined in Data.Constraint

Methods

evidence :: Dict a -> Dict a #

a => HasDict b (a :- b) 
Instance details

Defined in Data.Constraint

Methods

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

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

Defined in Data.Constraint

Methods

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

HasDict (a ~ b) (a :~: b) 
Instance details

Defined in Data.Constraint

Methods

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

HasDict (Coercible a b) (Coercion a b) 
Instance details

Defined in Data.Constraint

Methods

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

HasDict (a ~~ b) (a :~~: b) 
Instance details

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