Is it possible to derive a normalized source of a pure λ-function on Haskell?

Question

Let a pure λ-function be a term containing nothing but abstractions and applications. In JavaScript, you can output the source code of a pure function by applying all the abstractions to variational functions that collect a list of arguments. That is, it is possible:

lambdaSource(function(x){return x(x)}) == "λx.(xx)" 

See lambdaSource code for this value. This function has become especially useful for my interests, because it allows me to use existing JS engines to normalize unexplored expressions of lambda calculus much faster than any naive evaluator that I could write myself. Moreover, I know that the functions of λ-calculus can be expressed in Haskell using unsafeCoerce :

 (let (#) = unsafeCoerce in (\ fx -> (f # (f # (f # x))))) 

I do not know how to implement lambdaSource in Haskell due to the lack of variable functions. Is it possible to derive a normalized source of a pure λ-function on Haskell, so that:

 lambdaSource (\ fx -> f # (f # (f # x))) == "λ fx . f (f (fx))" 

?

Answer 1

Yes you can , but you need to provide a spine like your function, so it does not work for the ULC. See also lecture notes.

But since Daniel Wagner says you can just use HOAS.

There is another possibility: here is something that looks like HOAS, but is FOAS in fact, and all you need is a suitable normalization by evaluation ( in terms of quotation , in terms of reify and reflection ). pigworker also wrote a version of Jigger Haskell, but I cannot find it.

We can also do this safely in type theory: one way is to use valid conditions (which requires a postulate), or we can reify lambda terms into their PHOAS representation and then convert PHOAS to FOAS (which is very difficult).

EDIT

Here is the code related to HOAS:

 {-# LANGUAGE GADTs, FlexibleInstances #-} infixl 5 # data Term a = Pure a | Lam (Term a -> Term a) | App (Term a) (Term a) (#) :: Term a -> Term a -> Term a Lam f # x = fx f # x = App fx instance Show (Term String) where show = go names where names = map (:[]) ['a'..'z'] ++ map (++ ['\'']) names go :: [String] -> Term String -> String go ns (Pure n) = n go (n:ns) (Lam f) = concat ["\\", n, " -> ", go ns (f (Pure n))] go ns (App fx) = concat [go ns f, "(", go ns x, ")"] k :: Term a k = Lam $ \x -> Lam $ \y -> x s :: Term a s = Lam $ \f -> Lam $ \g -> Lam $ \x -> f # x # (g # x) omega :: Term a omega = (Lam $ \f -> f # f) # (Lam $ \f -> f # f) run t = t :: Term String main = do print $ run $ s -- \a -> \b -> \c -> a(c)(b(c)) print $ run $ s # k # k -- \a -> a -- print $ run $ omega -- bad idea 

In addition, instead of writing these Lam s, # and more, you can parse string representations of lambda terms in HOAS — it's no more complicated than typing HOAS terms.