Lambek Encoding

Categorical Semantics of Inductive Encodings

Article

Initial Object

data list (A: U) = nil | cons (a: A) (xs: list A)

Representing Functor F

FA = 1 + A * X

Construct corresponding F-Algebra

record listAlg (A: Type) : Type := (X: Type) (nil: Unit -> X) (cons: A -> X -> X)

Introduce List Morphisms

record listMor (A: Type) (x1,x2: ListAlg A) : Type := (map: x1.X -> x2.X) (mapNil: Path x2.X (map (x1.nil unit)) (x2.nil unit)) (mapCons: ∀ (a: A) -> ∀ (x: x1) -> Path x2.X (map (x1.cons a x)) (x2.cons a (map x)))

Introduce connected points of List type

record listPoint (A: Type) : Type := (point: ∀ (x: ListAlg A) -> x.X) (map: ∀ (x1,x2: listAlg A) -> (m: ListMor A x1 x2) -> Path x2.X (m.map (point x1)) (point x2))
$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$
$$U = ListAlg\\$$ $$U\ I = lim\ U\\$$ $\begin{array}{c}lim\ U\\\mapdown{\pi_i}\\X_i\end{array} \Longrightarrow \begin{array}{c}F\ lim\ U\\\mapdown{F\ \pi_i}\\F\ X_i\end{array} \Longrightarrow lim\ \begin{array}{c}F\ lim\ U\\\mapdown{F \pi_i}\\F\ X_i\end{array}$

Precise Encoding

Our encoding allows you to precise control the type of encoded parameter. There is only three cases and three equations: 1) for unit; 2) particular functorial type over a parameter type and 3) recursive embedding such as in Cons constructor.

q — is a limit in Dialg P category. The constructor body is calculated with q applied to forgetful functor U.

$$ q_{P,D,G} : End\ P\ (G'(-),G'(-)) \rightarrow P\ (Lim\ G',Lim\ G') \\ P : Set° \times Set \rightarrow Set \\ U : Dialg\ P \rightarrow Set \\ G : D \rightarrow Dialg\ P \\ G' = UG : D \rightarrow Set \\ U (Lim\ G) = Lim\ G' $$

Unit Parameters

Like for Bool or Nil constructors encoding.

$$ P_0(A,B) = B \\ q_0\ e : Lim\ G' \\ q_0\ e = e $$

Fixed Type Parameters

Like for Cons first parameter.

$$ P_1(A,B) = X \rightarrow P(A,B) \\ q_1\ e : X \rightarrow P ( Lim\ G', Lim\ G' ) \\ q_1\ e\ x\ A = e\ A\ x $$

Recursive Parameters

Like for Cons second parameter. This case is a key in encoding recursive data types such as Lists and recursive record types such as Streams.

$$ P_2(A,B) = A \rightarrow P(A,B) \\ q_2\ e : Lim\ G' \rightarrow P ( Lim\ G', Lim\ G' ) \\ q_2\ e\ I\ A = e\ A\ (I\ A) $$

Identity Functor Encoding

As known as predicative encoding

$$ \begin{array}{ccccccc} A & & \mapright{f} & & B & \mapright{f} & Set \\[3pt] & \mapdiagl{a} & \varphi & \mapdiagr{b} & & \searrow & \mapdown{\mathbf{1}} \\ & & Set & & & & Set \end{array} $$
$\varphi : a \rightarrow b$

Identity Functor Limit Encoding

As known as impredicative encoding

$$ \begin{array}{ccccccc} A & & \mapright{f} & & B & \mapright{f} & Set \\[3pt] & \mapdiagl{a} & \varphi & \mapdiagr{b} & & \searrow & \mapdown{\mathbf{1}} \\ & & Set & & & & Set \end{array} $$
$lim\ \varphi : lim\ a \rightarrow lim\ b$