vinyl-0.13.1: Extensible Records
Safe HaskellNone
LanguageHaskell2010

Data.Vinyl.TypeLevel

Synopsis

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

Associated Types

type RecSubsetFCtx Rec f Source #

Methods

rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss) Source #

rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[] Source #

rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> 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

Associated Types

type RecSubsetFCtx Rec f Source #

Methods

rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) Source #

rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs) Source #

rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss Source #

IndexWitnesses ('[] :: [Nat]) Source # 
Instance details

Defined in Data.Vinyl.TypeLevel

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source # 
Instance details

Defined in Data.Vinyl.TypeLevel

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.

Instances

Instances details
IndexWitnesses ('[] :: [Nat]) Source # 
Instance details

Defined in Data.Vinyl.TypeLevel

(IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) Source # 
Instance details

Defined in Data.Vinyl.TypeLevel

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

Project the first component of a type-level tuple.

Equations

Fst '(x, y) = x 

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

Project the second component of a type-level tuple.

Equations

Snd '(x, y) = y 

type family RLength xs where ... Source #

Equations

RLength '[] = 'Z 
RLength (x ': xs) = '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 (r ': rs) = 'Z 
RIndex r (s ': rs) = '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 '[] ss = '[] 
RImage (r ': rs) ss = RIndex r ss ': RImage rs ss 

type family RDelete r rs where ... Source #

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

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

Append for type-level lists.

Equations

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

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

class AllSatisfied cs t Source #

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

Instances

Instances details
AllSatisfied ('[] :: [k2]) (t :: k1) 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 ts :: 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) 

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

type family MapTyCon t xs = r | r -> xs 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 

class Coercible (f x) (g x) => Similar f g (x :: k) 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