Data.Type.List.Map

Vectors indexed by a type list

Documentation

data MapC f c where

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

Constructors

Nil :: MapC f Nil

:> :: MapC f c -> f a -> MapC f (c :> a)

empty :: MapC f Nil

Create an empty MapC vector.

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

Create a singleton MapC vector.

lookup :: Member c a -> MapC f c -> f a

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

mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g c

Map a function to all elements of a MapC vector.

append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)

Append two MapC vectors.

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

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

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

A version of mkAppend that takes in a Proxy argument.

split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)

Split a MapC vector into two pieces.

proxy :: MapC f c -> Proxy c

Create a Proxy object for the type list of a MapC vector.

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

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