Data.Microgroove.Lib.TypeLevel

Constraints

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

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

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

Minimal complete definition

intList

Methods

intList :: [Int]

Instances

KnownNats [k] ([] k)

Methods

intList :: [Int]

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

Methods

intList :: [Int]

intVal :: forall n. KnownNat n => Int

Type List operations

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

Equations

Length '[] = 0

Length (_ ': xs) = 1 + Length xs

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

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

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

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

Index into a type level list

Equations

(x ': _) !! 0 = x

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

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

Append type level lists

Equations

'[] ++ bs = bs

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