Typed λ Calculus Interpreter in Agda
In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.
In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.
By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the S
combinator is injective?”, tried to construct the inverse of S
and showed that S⁻¹ ○ S = id
in, guess what, Agda!
An indcutive type μF is simulated by forall x . (F x -> x) -> x
, while a coinductive type νF is simulatd by exists x . (x -> F x, x)
. When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.
We can even define primitive recursion, only that it does not have the desired type primrec :: (N -> b -> b) -> b -> N -> b
. Therefore, predecessor does not get the type pred :: N a -> N a
either.
Do you know that the S combinator is injective? I have a simple algebraic proof and Nakano actually constructed its inverse.