Safe Haskell	None
Language	Haskell2010

Data.Vinyl.TypeLevel

Synopsis

data Nat
- = Z
- | S !Nat
class NatToInt (n :: Nat) where
- natToInt :: Int
class IndexWitnesses (is :: [Nat]) where
- indexWitnesses :: [Int]
type family Fst (a :: (k1, k2)) :: k1 where ...
type family Snd (a :: (k1, k2)) :: k2 where ...
type family RLength (xs :: [a]) :: Nat where ...
type family RIndex (r :: k) (rs :: [k]) :: Nat where ...
type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where ...
type family RDelete (r :: a) (rs :: [a]) :: [a] where ...
type family RecAll (f :: u -> Type) (rs :: [u]) (c :: Type -> Constraint) where ...
type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
type family AllConstrained (c :: u -> Constraint) (ts :: [u]) where ...
class AllSatisfied (cs :: k) (t :: k1)
type family AllAllSat (cs :: k) (ts :: [k1]) where ...
type family ApplyToField (t :: Type -> Type) (a :: k1) = (r :: k1) | r -> k1 t a where ...
type family MapTyCon (t :: Type -> Type) (xs :: [a]) = (r :: [a]) | r -> a xs where ...
class Coercible (f x) (g x) => Similar (f :: k1 -> k) (g :: k1 -> k) (x :: k1)

Documentation

data Nat Source #

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

Instances details

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat]) Source #
Instance details Defined in Data.Vinyl.Lens Methods rsubsetC :: forall g (f :: k -> Type). (Functor g, RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f) => (Rec f ('[] :: [k]) -> g (Rec f ('[] :: [k]))) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k -> Type). RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f => Rec f ss -> Rec f ('[] :: [k]) Source # rreplaceC :: forall (f :: k -> Type). RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f => Rec f ('[] :: [k]) -> Rec f ss -> Rec f ss Source #
(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is) Source #
Instance details Defined in Data.Vinyl.Lens Methods rsubsetC :: forall g (f :: k -> Type). (Functor g, RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k -> Type). RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f => Rec f ss -> Rec f (r ': rs) Source # rreplaceC :: forall (f :: k -> Type). RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) f => Rec f (r ': rs) -> Rec f ss -> Rec f ss Source #
IndexWitnesses ('[] :: [Nat]) Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods indexWitnesses :: [Int] Source #
(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods indexWitnesses :: [Int] Source #

class NatToInt (n :: Nat) where Source #

Produce a runtime Int value corresponding to a Nat type.

Methods

natToInt :: Int Source #

Instances

Instances details

NatToInt 'Z Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods natToInt :: Int Source #
NatToInt n => NatToInt ('S n) Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods natToInt :: Int Source #

class 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] Source #

Instances

Instances details

IndexWitnesses ('[] :: [Nat]) Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods indexWitnesses :: [Int] Source #
(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source #
Instance details Defined in Data.Vinyl.TypeLevel Methods indexWitnesses :: [Int] Source #

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

Project the first component of a type-level tuple.

Equations

Fst ('(x, y) :: (k1, k2)) = x

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

Project the second component of a type-level tuple.

Equations

Snd ('(x, y) :: (k1, k2)) = y

type family RLength (xs :: [a]) :: Nat where ... Source #

Equations

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

type 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 :: a) (r ': rs :: [a]) = 'Z
RIndex (r :: k) (s ': rs :: [k]) = 'S (RIndex r rs)

type 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 ('[] :: [k]) (ss :: [k]) = '[] :: [Nat]
RImage (r ': rs :: [k]) (ss :: [k]) = RIndex r ss ': RImage rs ss

type family RDelete (r :: a) (rs :: [a]) :: [a] where ... Source #

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

Equations

RDelete (r :: a) (r ': rs :: [a]) = rs
RDelete (r :: a) (s ': rs :: [a]) = s ': RDelete r rs

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

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

Equations

RecAll (f :: u -> Type) ('[] :: [u]) c = ()
RecAll (f :: u -> Type) (r ': rs :: [u]) c = (c (f r), RecAll f rs c)

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

Append for type-level lists.

Equations

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

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

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

Equations

AllConstrained (c :: u -> Constraint) ('[] :: [u]) = ()
AllConstrained (c :: u -> Constraint) (t ': ts :: [u]) = (c t, AllConstrained c ts)

class AllSatisfied (cs :: k) (t :: k1) Source #

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

Instances

Instances details

AllSatisfied ('[] :: [a]) (t :: k) Source #
Instance details Defined in Data.Vinyl.TypeLevel
(c t, AllSatisfied cs t) => AllSatisfied (c ': cs :: [k -> Constraint]) (t :: k) Source #
Instance details Defined in Data.Vinyl.TypeLevel

type family AllAllSat (cs :: k) (ts :: [k1]) 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 :: k1) ('[] :: [k2]) = ()
AllAllSat (cs :: k1) (t ': ts :: [k2]) = (AllSatisfied cs t, AllAllSat cs ts)

type family ApplyToField (t :: Type -> Type) (a :: k1) = (r :: k1) | r -> k1 t a 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) :: (k, Type)) = '(s, t x)
ApplyToField t (x :: Type) = t x

type family MapTyCon (t :: Type -> Type) (xs :: [a]) = (r :: [a]) | r -> a xs where ... Source #

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

Equations

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

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

Instances

Instances details

Coercible (f x) (g x) => Similar (f :: k2 -> k1) (g :: k2 -> k1) (x :: k2) Source #
Instance details Defined in Data.Vinyl.TypeLevel