Data.Microgroove.TypeLevel

Documentation

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

Index into a type level list

Equations

(x ': _) !! 0 = x

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

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

Equations

Length '[] = 0

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

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

AllF c f xs ensures that constraint 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)

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

Append type level lists

Equations

'[] ++ bs = bs

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

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

data Some f where

Inductive Natural Numbers

An injective form of Replicate using inductive Nat' rather than builtins

The Existential Type Some f is some f x where x is known at runtime

Constructors

Some :: f x -> Some f

data MaybeSome f

Avoids one indirection compared with Maybe (Some f)

Constructors

JustSome (f x)

None

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