mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-08-04 10:38:40 +00:00
62f8c46483
* Not working yet * Fix bugs * Update npm dependencies and language configuration * Fix some leftovers --------- Co-authored-by: Tim Süberkrüb <dev@timsueberkrueb.io>
17 lines
750 B
Text
17 lines
750 B
Text
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 }
|
|
|
|
codef S(p: Nat): Nat { .case(A, z, s) => s.ap(p) }
|
|
|
|
codef Z: Nat { .case(A, z, s) => z }
|