Add text to encoding examples (#407)

* Add explanation of Church encodings

* Add explanation of Scott encoding

* Add explanation for Parigot encoding

* Add explanation of Fu-Stump encoding

* Fix error

---------

Co-authored-by: Tim Süberkrüb <[email protected]>

examples/encoding_church.pol

@@ -1,6 +1,14 @@
-codata Fun(A B: Type) {
-    Fun(A, B).ap(A B: Type, x: A): B
-}
+use "../std/codata/fun.pol"
+-- Using the Church encoding we can represent a natural number using its
+-- iteration principle.
+--
+-- The iteration principle for the number "n" allows to construct, for any type "A",
+-- an inhabitant of "A" by applying a function "s : A -> A" n-times to the
+-- starting value "z : A".
+--
+-- By defunctionalizing and refunctionalizing the type "Nat" you can observe how
+-- the Church encoding corresponds to a program which defines an iteration principle
+-- on Peano natural numbers.
 
 codata Nat { .iter(A: Type, z: A, s: A -> A): A }
 

examples/encoding_fu_stump.pol

@@ -1,15 +1,26 @@
-codata Fun(A B: Type) {
-    Fun(A, B).ap(A B: Type, x: A): B
+use "../std/codata/fun.pol"
+-- Using an encoding proposed by Fu and Stump, we can represent a natural number using its
+-- induction principle.
+--
+-- The induction principle for the number "n" allows to construct, for any property "P : Nat -> Type",
+-- a proof of "P n" by applying the induction step n-times to the proof of the base case "P Z".
+--
+-- By defunctionalizing and refunctionalizing the type "Nat" you can observe how
+-- the Fu-Stump encoding corresponds to a program which defines an induction principle
+-- on Peano natural numbers.
+--
+-- - Peng Fu, Aaron Stump (2013): Self Types for Dependently Typed Lambda Encodings
+
+-- | The type of dependent functions.
+codata Π(A: Type, T: A -> Type) {
+    Π(A, T).dap(A: Type, T: A -> Type, x: A): T.ap(A, Type, x)
 }
 
+-- | An abbreviation of the induction step, i.e. a function from "P x" to "P (S x)".
 codef StepFun(P: Nat -> Type): Fun(Nat, Type) {
     .ap(_, _, x) => P.ap(Nat, Type, x) -> P.ap(Nat, Type, S(x))
 }
 
-codata Π(A: Type, T: A -> Type) {
-    Π(A, T).dap(A: Type, T: A -> Type, x: A): T.ap(A, Type, x)
-}
-
 codata Nat {
     (n: Nat).ind(P: Nat -> Type, base: P.ap(Nat, Type, Z), step: Π(Nat, StepFun(P)))
         : P.ap(Nat, Type, n)

examples/encoding_parigot.pol

@@ -1,6 +1,14 @@
-codata Fun(A B: Type) {
-    Fun(A, B).ap(A B: Type, x: A): B
-}
+use "../std/codata/fun.pol"
+-- The Parigot encoding combines the properties of the Church encoding and the Scott
+-- encoding.
+--
+-- The method "analyze" is the combination of the methods "iter" from the Church encoding
+-- and the method "case" from the Scott encoding. We have access to both the predecessor
+-- number itself and to the result of the recursive call.
+--
+-- By defunctionalizing and refunctionalizing the type "Nat" you can observe how
+-- the Parigot encoding can be understood as the refunctionalized version of Peano natural
+-- numbers which implement a "analyze" method.
 
 codata Nat { .analyze(A: Type, z: A, s: Nat -> A -> A): A }
 

examples/encoding_scott.pol

@@ -1,6 +1,14 @@
-codata Fun(A B: Type) {
-    Fun(A, B).ap(A B: Type, x: A): B
-}
+use "../std/codata/fun.pol"
+-- Using the Scott encoding we can represent a natural number using its
+-- pattern matching principle.
+--
+-- The pattern matching principle for the number "n" allows to distinguish the zero
+-- case from the successor case by either returning a value "z : A" if the number is zero,
+-- or by applying a function "f : Nat -> A" to the predecessor of the number if it isn't zero.
+--
+-- By defunctionalizing and refunctionalizing the type "Nat" you can observe how
+-- the Scott encoding corresponds to a program which defines a pattern matching principle
+-- on Peano natural numbers.
 
 codata Nat { .case(A: Type, z: A, s: Nat -> A): A }
 

lang/transformations/src/xfunc/matrix.rs

@@ -129,10 +129,8 @@ impl BuildMatrix for ast::Codata {
 impl BuildMatrix for ast::Def {
     fn build_matrix(&self, out: &mut Prg) -> Result<(), XfuncError> {
         let type_name = &self.self_param.typ.name;
-        let xdata = out.map.get_mut(&type_name.id).ok_or(XfuncError::Impossible {
-            message: format!("Could not resolve {type_name}"),
-            span: None,
-        })?;
+        // Only add to the matrix if the type is declared in this module
+        let Some(xdata) = out.map.get_mut(&type_name.id) else { return Ok(()) };
         xdata.dtors.insert(self.name.id.clone(), self.to_dtor());
 
         let cases = &self.cases;
@@ -149,10 +147,10 @@ impl BuildMatrix for ast::Def {
 impl BuildMatrix for ast::Codef {
     fn build_matrix(&self, out: &mut Prg) -> Result<(), XfuncError> {
         let type_name = &self.typ.name;
-        let xdata = out.map.get_mut(&type_name.id).ok_or(XfuncError::Impossible {
-            message: format!("Could not resolve {type_name}"),
-            span: None,
-        })?;
+        // Only add to the matrix if the type is declared in this module
+        let Some(xdata) = out.map.get_mut(&type_name.id) else {
+            return Ok(());
+        };
         xdata.ctors.insert(self.name.id.clone(), self.to_ctor());
 
         let cases = &self.cases;