Data.Type.HList

A type list contains types as elements. We use GADT proofs terms to establish membership and append relations. A Data.Type.HList.HList f is a vector indexed by a type list, where f :: * -> * is applied to each type element.

Documentation

data Nil

Instances

TypeCtx Nil

NuMatchingList Nil

type r :++: Nil = r

data r :> a infixl 5

Instances

TypeCtx ctx => TypeCtx ((:>) ctx a)

(NuMatchingList args, NuMatching a) => NuMatchingList ((:>) args a)

type r1 :++: ((:>) r2 a) = (:>) ((:++:) r1 r2) a

type family r1 :++: r2 infixr 5

Instances

type r :++: Nil = r

type r1 :++: ((:>) r2 a) = (:>) ((:++:) r1 r2) a

proxyCons :: Proxy r -> f a -> Proxy (r :> a)

data Member ctx a where

A Member ctx a is a "proof" that the type a is in the type list ctx, meaning that ctx equals

 t0 ':>' a ':>' t1 ':>' ... ':>' tn

for some types t0,t1,...,tn.

Constructors

Member_Base :: Member (ctx :> a) a

Member_Step :: Member ctx a -> Member (ctx :> b) a

Instances

Show (Member r a)

NuMatching (Member c a)

Liftable (Member c a)

showsPrecMember :: Bool -> Member ctx a -> ShowS

weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a

membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)

data Append ctx1 ctx2 ctx where

An Append ctx1 ctx2 ctx is a "proof" that ctx = ctx1 :++: ctx2.

Constructors

Append_Base :: Append ctx Nil ctx

Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)

data HList f c where

A HList f c is a vector with exactly one element of type f a for each type a in the type list c.

Constructors

Nil :: HList f Nil

(:>) :: HList f c -> f a -> HList f (c :> a) infixl 5

Instances

Show (HList Name c)

(NuMatching1 f, NuMatchingList ctx) => NuMatching (HList f ctx)

empty :: HList f Nil

Create an empty HList vector.

singleton :: f a -> HList f (Nil :> a)

Create a singleton HList vector.

hlistLookup :: Member c a -> HList f c -> f a

Look up an element of a HList vector using a Member proof.

mapHList :: (forall x. f x -> g x) -> HList f c -> HList g c

Map a function on all elements of a HList vector.

mapHList2 :: (forall x. f x -> g x -> h x) -> HList f c -> HList g c -> HList h c

Map a binary function on all pairs of elements of two HList vectors.

appendHList :: HList f c1 -> HList f c2 -> HList f (c1 :++: c2)

Append two HList vectors.

mkAppend :: HList f c2 -> Append c1 c2 (c1 :++: c2)

Make an Append proof from any HList vector for the second argument of the append.

mkMonoAppend :: Proxy c1 -> HList f c2 -> Append c1 c2 (c1 :++: c2)

A version of mkAppend that takes in a Proxy argument.

proxiesFromAppend :: Append c1 c2 c -> HList Proxy c2

The inverse of mkAppend, that builds an HList from an Append

splitHList :: (c ~ (c1 :++: c2)) => Proxy c1 -> HList any c2 -> HList f c -> (HList f c1, HList f c2)

Split an HList vector into two pieces. The first argument is a phantom argument that gives the form of the first list piece.

members :: HList f c -> HList (Member c) c

Create a vector of proofs that each type in c is a Member of c.

hlistToList :: HList (Constant a) c -> [a]

Convert an HList to a list

class TypeCtx ctx where

A type-class which ensures that ctx is a valid context, i.e., has | the form (Nil :> t1 :> ... :> tn) for some types t1 through tn

Methods

typeCtxProxies :: HList Proxy ctx

Instances

TypeCtx Nil

TypeCtx ctx => TypeCtx ((:>) ctx a)