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)

Instances

Show (MapC Name c)

(NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx)

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.

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

Map a binary function to all pairs of elements of two MapC vectors.

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.

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

Replace a single element of a MapC vector.

mapCToList :: MapC (Constant a) c -> [a]

Convert a MapC to a list