mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-12-23 09:19:50 +00:00
37 lines
No EOL
1.4 KiB
Text
37 lines
No EOL
1.4 KiB
Text
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
|
|
note foo_stump_encoding
|
|
|
|
/// The type of dependent functions.
|
|
codata Π(A: Type, T: A -> Type) {
|
|
Π(A, T).dap(A: Type, T: A -> Type, x: A): T.ap(a:=A, b:=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(a:=Nat, b:=Type, x) -> P.ap(a:=Nat, b:=Type, S(x))
|
|
}
|
|
|
|
codata Nat {
|
|
(n: Nat).ind(P: Nat -> Type, base: P.ap(a:=Nat, b:=Type, Z), step: Π(Nat, StepFun(P)))
|
|
: P.ap(a:=Nat, b:=Type, n),
|
|
}
|
|
|
|
codef Z: Nat { .ind(P, base, step) => base }
|
|
|
|
codef S(m: Nat): Nat {
|
|
.ind(P, base, step) =>
|
|
step.dap(Nat, StepFun(P), m)
|
|
.ap(a:=P.ap(a:=Nat, b:=Type, m), b:=P.ap(a:=Nat, b:=Type, S(m)), m.ind(P, base, step))
|
|
} |