microgroove-0.2.1.0: Array-backed extensible records

Safe HaskellNone
LanguageHaskell2010

Data.Microgroove.Lib.TypeLevel

Contents

Synopsis

Constraints

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

All c xs holds if c x holds for all x in xs

Equations

All c '[] = () 
All c (x ': xs) = (c x, All c xs) 

type family AllF (c :: * -> Constraint) (f :: u -> *) (xs :: [u]) :: Constraint where ... Source #

AllF c f xs holds if c (f x) holds for all x in xs

Equations

AllF c f '[] = () 
AllF c f (x ': xs) = (c (f x), AllF c f xs) 

Naturals

class KnownNats ns where Source #

Minimal complete definition

intList

Methods

intList :: [Int] Source #

Instances

KnownNats [k] ([] k) Source # 

Methods

intList :: [Int] Source #

(KnownNat n, KnownNats [Nat] ns) => KnownNats [Nat] ((:) Nat n ns) Source # 

Methods

intList :: [Int] Source #

intVal :: forall n. KnownNat n => Int Source #

Type List operations

type family Length (xs :: [u]) :: Nat where ... Source #

Equations

Length '[] = 0 
Length (_ ': xs) = 1 + Length xs 

type family SubList# (ns :: [Nat]) (xs :: [u]) :: [u] where ... Source #

Take a sublist of xs given by the indicies in ns. ns@ must be in ascending order, but this is not checked

Equations

SubList# ns xs = SubList' ns xs 0 

type family Replicate (n :: Nat) (x :: u) :: [u] where ... Source #

Extend a type x into a type level list xs of length n

Equations

Replicate 0 x = '[] 
Replicate n x = x ': Replicate (n - 1) x 

type family SetAt n xs x where ... Source #

Equations

SetAt 0 (_ ': xs) x = x ': xs 
SetAt n (x ': xs) y = x ': SetAt (n - 1) xs y 

type family (xs :: [u]) !! (n :: Nat) where ... Source #

Index into a type level list

Equations

(x ': _) !! 0 = x 
(_ ': xs) !! n = xs !! (n - 1) 

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

Append type level lists

Equations

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