vinyl-0.6.0: 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

RSubset k ([] k) ss ([] Nat) Source # 

Methods

rsubset :: Functor g => (Rec [k] f ss -> g (Rec [k] f ss)) -> Rec [k] f [Nat] -> g (Rec [k] f [Nat]) Source #

rcast :: Rec [k] f [Nat] -> Rec [k] f ss Source #

rreplace :: Rec [k] f ss -> Rec [k] f [Nat] -> Rec [k] f [Nat] Source #

(RElem k r ss i, RSubset k rs ss is) => RSubset k ((:) k r rs) ss ((:) Nat i is) Source # 

Methods

rsubset :: Functor g => (Rec ((k ': r) rs) f ss -> g (Rec ((k ': r) rs) f ss)) -> Rec ((k ': r) rs) f ((Nat ': i) is) -> g (Rec ((k ': r) rs) f ((Nat ': i) is)) Source #

rcast :: Rec ((k ': r) rs) f ((Nat ': i) is) -> Rec ((k ': r) rs) f ss Source #

rreplace :: Rec ((k ': r) rs) f ss -> Rec ((k ': r) rs) f ((Nat ': i) is) -> Rec ((k ': r) rs) f ((Nat ': i) is) Source #

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 ts :: 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) 

type family AllSatisfied cs t :: Constraint where ... Source #

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

Equations

AllSatisfied '[] t = () 
AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t) 

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)