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

Portability GHC experimental emw4@rice.edu Safe-Infered

Data.Type.List.Map

Description

Vectors indexed by a type list

Synopsis

# Documentation

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`.

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)

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.

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

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

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`.

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

Replace a single element of a `MapC` vector.