Suppose we implement the λ-calculus inside the λ-calculus itself with λ-encodings and Bruijn indices:
Lam = λ body . λ Lam . λ App . λ Var . Lam body App = λ fun . λ arg . λ Lam . λ App . λ Var . App fun arg Var = λ idx . λ Lam . λ App . λ Var . Var idx
Is it possible to implement a
quote() function that, given a native term, returns its own λ-encoded representation? For example:
quote(λ f . λ x . f (f x))
Lam (Lam (App (Var 1) (App (Var 1) (Var 0))))
If not, is it possible if given a type?
quote(Arr(Arr(T,T),Arr(T,T)), λ f . λ x . f (f x)))
Arr(Arr(T,T),Arr(T,T)) represents that the term we want to quote has the following STLC type:
(o -> o) -> o -> o.