55 lines
1.1 KiB
Plaintext
55 lines
1.1 KiB
Plaintext
-- Can we define the Y combinator in pi-forall?
|
|
-- Yes! See below.
|
|
-- Note: pi-forall allows recursive definitions,
|
|
-- so this is not necessary at all.
|
|
|
|
module Fix where
|
|
|
|
-- To type check the Y combinator, we need to have a type
|
|
-- D such that D ~~ D -> D
|
|
|
|
|
|
data D (A : Type) : Type where
|
|
F of (_ : D A -> D A)
|
|
V of (_ : A)
|
|
|
|
unV : [A:Type] -> D A -> A
|
|
unV = \[A] v.
|
|
case v of
|
|
V y -> y
|
|
F f -> TRUSTME
|
|
|
|
unF :[A:Type] -> D A -> D A -> D A
|
|
unF = \[A] v x .
|
|
case v of
|
|
F f -> f x
|
|
V y -> TRUSTME
|
|
|
|
-- Here's the Y-combinator. To make it type
|
|
-- check, we need to add the appropriate conversions
|
|
-- into and out of the D type.
|
|
|
|
fix : [A:Type] -> (A -> A) -> A
|
|
fix = \ [A] g.
|
|
let omega =
|
|
( \x. V (g (unV [A] (unF [A] x x)))
|
|
: D A -> D A) in
|
|
unV [A] (omega (F omega))
|
|
|
|
-- Example use case
|
|
|
|
|
|
data Nat : Type where
|
|
Zero
|
|
Succ of ( _ : Nat)
|
|
|
|
fix_add : Nat -> Nat -> Nat
|
|
fix_add = fix [Nat -> Nat -> Nat]
|
|
\radd. \x. \y.
|
|
case x of
|
|
Zero -> y
|
|
Succ n -> Succ (radd n y)
|
|
|
|
test : fix_add 5 2 = 7
|
|
test = Refl
|