hobbits-1.0: A library for canonically representing terms with binding




Vectors indexed by a type list



data MapC f c whereSource

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


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

empty :: MapC f NilSource

Create an empty MapC vector.

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

Create a singleton MapC vector.

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

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

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

Map a function to all elements of a MapC vector.

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

Append two MapC vectors.

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

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)Source

A version of mkAppend that takes in a Proxy argument.

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

Split a MapC vector into two pieces.

proxy :: MapC f c -> Proxy cSource

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

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

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