From b49c66ab362dc5950e616950318832ba2b608181 Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 4 Dec 2024 16:24:08 +0100 Subject: [PATCH 1/5] Add explanation of Church encodings --- examples/encoding_church.pol | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/examples/encoding_church.pol b/examples/encoding_church.pol index fe37db82e..2af20a6d8 100644 --- a/examples/encoding_church.pol +++ b/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 } From a59e148a5d23465a9502d1d114d73dff33936860 Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 4 Dec 2024 16:28:33 +0100 Subject: [PATCH 2/5] Add explanation of Scott encoding --- examples/encoding_scott.pol | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/examples/encoding_scott.pol b/examples/encoding_scott.pol index dcd8727ab..571907ee5 100644 --- a/examples/encoding_scott.pol +++ b/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 } From 7b6fbca6a8f20615fe50cea0d6c2744321de4045 Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 4 Dec 2024 16:39:20 +0100 Subject: [PATCH 3/5] Add explanation for Parigot encoding --- examples/encoding_parigot.pol | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/examples/encoding_parigot.pol b/examples/encoding_parigot.pol index 23665478b..c4a6d6743 100644 --- a/examples/encoding_parigot.pol +++ b/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 } From 4fc341abd9f52edf4422ca8a25f70ed7d7300424 Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 4 Dec 2024 16:49:37 +0100 Subject: [PATCH 4/5] Add explanation of Fu-Stump encoding --- examples/encoding_fu_stump.pol | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/examples/encoding_fu_stump.pol b/examples/encoding_fu_stump.pol index e9a7bb662..eb5584e8d 100644 --- a/examples/encoding_fu_stump.pol +++ b/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) From b7008f5f8072d98b497f3769c80709ca96a8f1b9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Wed, 4 Dec 2024 17:35:02 +0100 Subject: [PATCH 5/5] Fix error --- lang/transformations/src/xfunc/matrix.rs | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/lang/transformations/src/xfunc/matrix.rs b/lang/transformations/src/xfunc/matrix.rs index 7eb7a92aa..9676bc8e2 100644 --- a/lang/transformations/src/xfunc/matrix.rs +++ b/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;