Definition.idr

The Extension of Containers

The extension is crucial to understand containers as data descriptors. Given a container c, its extension Ex c : Type -> Type gives us the type constructor, in the host language, for the data structure that it represents. A typical example is the $List$ container that we will see in the next section.

Definition

Given a container $(A,\bar{A})$, its extension $[[\_]]$ is a functor $\mathcal{S}et\to \mathcal{S}et$ given by $[[(A,\bar{A})]]=\lambda x.\Sigma (a:A).\bar{A}(a)\to x$.

record Ex (cont : Container) (ty : Type) where
  autobind
  constructor MkEx
  ex1 : cont.req
  ex2 : cont.res ex1 -> ty

We reproduce this definition in Idris with a record. While we could use Σ-types as well, creating a new type for this ensure we never confuse the semantics of the extension with a regular Σ-type. The constructor is marked autobind such that one can create a value without using a lambda for the second argument.