Modulevinyl-0.14.3Haskell2010

Data.Vinyl.TypeLevel

Synopsis

data Nat
class NatToInt
class IndexWitnesses
family Fst
family Snd
family RLength
family RIndex
family RImage
family RDelete
family RecAll
family ++
family AllConstrained
class AllSatisfied
family AllAllSat
family ApplyToField
family MapTyCon
class Similar

Packagevinyl-0.14.3
Exports17
LanguageHaskell2010
LicenceMIT
SourceTypeLevel.hs

datadata 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

Instances4RecSubset, IndexWitnesses

RecSubset Rec '[] ss '[]Defined in vinyl-0.14.3 · Data.Vinyl.Lens
(RElem r ss i, RSubset rs ss is) => RecSubset Rec (r ': rs) ss (i ': is)Defined in vinyl-0.14.3 · Data.Vinyl.Lens
IndexWitnesses '[]Defined in vinyl-0.14.3 · Data.Vinyl.TypeLevel
(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is)Defined in vinyl-0.14.3 · Data.Vinyl.TypeLevel

classclass NatToInt (n :: Nat) where

Source#

Produce a runtime Int value corresponding to a Nat type.

Methods

natToInt :: Int

Instances2NatToInt

NatToInt 'ZDefined in vinyl-0.14.3 · Data.Vinyl.TypeLevel
NatToInt n => NatToInt ('S n)Defined in vinyl-0.14.3 · Data.Vinyl.TypeLevel

classclass IndexWitnesses (is :: [Nat]) where

Source#

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

Methods

indexWitnesses :: [Int]

Instances2IndexWitnesses

IndexWitnesses '[]Defined in vinyl-0.14.3 · Data.Vinyl.TypeLevel
(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is)Defined in vinyl-0.14.3 · Data.Vinyl.TypeLevel

familytype family Fst (a :: (k1, k2)) :: k1 where

Source#

Project the first component of a type-level tuple.

Equations

Fst '(x, y) = x

familytype family Snd (a :: (k1, k2)) :: k2 where

Source#

Project the second component of a type-level tuple.

Equations

Snd '(x, y) = y

familytype family RLength (xs :: [a]) :: Nat where

Equations

RLength '[] = 'Z
RLength (x ': xs) = 'S (RLength xs)

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

Source#

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)

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

Source#

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

familytype family RDelete (r :: a) (rs :: [a]) :: [a] where

Source#

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

Equations

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

familytype family RecAll (f :: u -> Type) (rs :: [u]) (c :: Type -> Constraint) :: Constraint where

Source#

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)

familytype family (++) (as :: [k]) (bs :: [k]) :: [k] where

Source#

Append for type-level lists.

Equations

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

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

Source#

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

Equations

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

classclass AllSatisfied (cs :: k) (t :: k1)

Source#

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

Instances2AllSatisfied

AllSatisfied '[] tDefined in vinyl-0.14.3 · Data.Vinyl.TypeLevel
(c t, AllSatisfied cs t) => AllSatisfied (c ': cs) tDefined in vinyl-0.14.3 · Data.Vinyl.TypeLevel

familytype family AllAllSat (cs :: k) (ts :: [k1]) :: Constraint where

Source#

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)

familytype family ApplyToField (t :: Type -> Type) (a :: k1) :: k1 where

Source#

Apply a type constructor to a record index. Record indexes are either Type or (Symbol, Type). In the latter case, the type constructor is applied to the second component of the tuple.

Equations

ApplyToField t '(s, x) = '(s, t x)
ApplyToField t x = t x

familytype family MapTyCon (t :: Type -> Type) (xs :: [a]) :: [a] where

Source#

Apply a type constructor to each element of a type level list using ApplyOn.

Equations

MapTyCon t '[] = '[]
MapTyCon t (x ': xs) = ApplyToField t x ': MapTyCon t xs

classclass Coercible (f x) (g x) => Similar (f :: k1 -> k) (g :: k1 -> k) (x :: k1)

Source#

This class is used for consMatchCoercion with older versions of GHC.

Instances1Similar

Coercible (f x) (g x) => Similar f g xDefined in vinyl-0.14.3 · Data.Vinyl.TypeLevel