Data.Vinyl.TypeLevel

Documentation

data Nat

A mere approximation of the natural numbers. And their image as lifted by -XDataKinds corresponds to the actual natural numbers.

Constructors

Z

S !Nat

Instances

RecSubset (Rec :: (k -> *) -> [k] -> *) ([] :: [k]) (ss :: [k]) ([] :: [Nat])

Defined in Data.Vinyl.Lens

Associated Types

type RecSubsetFCtx Rec f :: Constraint

Methods

rsubsetC :: (Functor g, RecSubsetFCtx Rec f) => (Rec f [] -> g (Rec f [])) -> Rec f ss -> g (Rec f ss)

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f []

rreplaceC :: RecSubsetFCtx Rec f => Rec f [] -> Rec f ss -> Rec f ss

(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> *) -> [k] -> *) (r ': rs :: [k]) (ss :: [k]) (i ': is)

Defined in Data.Vinyl.Lens

Associated Types

type RecSubsetFCtx Rec f :: Constraint

Methods

rsubsetC :: (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss)

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs)

rreplaceC :: RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss

IndexWitnesses ([] :: [Nat])

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is)

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

class NatToInt (n :: Nat) where

Produce a runtime Int value corresponding to a Nat type.

Minimal complete definition

natToInt

Methods

natToInt :: Int

Instances

NatToInt Z

Defined in Data.Vinyl.TypeLevel

Methods

natToInt :: Int

NatToInt n => NatToInt (S n)

Defined in Data.Vinyl.TypeLevel

Methods

natToInt :: Int

class IndexWitnesses (is :: [Nat]) where

Reify a list of type-level natural number indices as runtime Ints relying on instances of NatToInt.

Minimal complete definition

indexWitnesses

Methods

indexWitnesses :: [Int]

Instances

IndexWitnesses ([] :: [Nat])

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is)

Defined in Data.Vinyl.TypeLevel

Methods

indexWitnesses :: [Int]

type family Fst (a :: (k1, k2)) where ...

Project the first component of a type-level tuple.

Equations

Fst '(x, y) = x

type family Snd (a :: (k1, k2)) where ...

Project the second component of a type-level tuple.

Equations

Snd '(x, y) = y

type family RLength xs where ...

Equations

RLength '[] = Z

RLength (x ': xs) = S (RLength xs)

type family RIndex (r :: k) (rs :: [k]) :: Nat where ...

A partial relation that gives the index of a value in a list.

Equations

RIndex r (r ': rs) = Z

RIndex r (s ': rs) = S (RIndex r rs)

type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where ...

A partial relation that gives the indices of a sublist in a larger list.

Equations

RImage '[] ss = '[]

RImage (r ': rs) ss = RIndex r ss ': RImage rs ss

type family RDelete r rs where ...

Remove the first occurence of a type from a type-level list.

Equations

RDelete r (r ': rs) = rs

RDelete r (s ': rs) = s ': RDelete r rs

type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where ...

A constraint-former which applies to every field in a record.

Equations

RecAll f '[] c = ()

RecAll f (r ': rs) c = (c (f r), RecAll f rs c)

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...

Append for type-level lists.

Equations

'[] ++ bs = bs

(a ': as) ++ bs = a ': (as ++ bs)

type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where ...

Constraint that all types in a type-level list satisfy a constraint.

Equations

AllConstrained c '[] = ()

AllConstrained c (t ': ts) = (c t, AllConstrained c ts)

class AllSatisfied cs t

Constraint that each Constraint in a type-level list is satisfied by a particular type.

Instances

AllSatisfied ([] :: [k1]) (t :: k2)

Defined in Data.Vinyl.TypeLevel

(c t, AllSatisfied cs t) => AllSatisfied (c ': cs :: [k -> Constraint]) (t :: k)

Defined in Data.Vinyl.TypeLevel

type family AllAllSat cs ts :: Constraint where ...

Constraint that all types in a type-level list satisfy each constraint from a list of constraints.

AllAllSat cs ts should be equivalent to AllConstrained (AllSatisfied cs) ts if partial application of type families were legal.

Equations

AllAllSat cs '[] = ()

AllAllSat cs (t ': ts) = (AllSatisfied cs t, AllAllSat cs ts)