Is it possible to infer the normalized source of a pure λ function on Haskell?

Question

Let a pure λ function be a term with nothing but abstractions and applications. On JavaScript, it is possible to infer the source code of a pure function by applying all abstractions to variadic functions that collect their argument list. That is, this is possible:

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

See the code for lambdaSource on this gist. That function became particularly useful for my interests since it allows me to use existing JS engines to normalize untyped lambda calculus expressions much faster than any naive evaluator I could code by myself. Moreover, I know λ-calculus functions can be expressed in Haskell with help of unsafeCoerce:

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

I do not know how to implement lambdaSource in Haskell because of the lack of variadic functions. Is it possible to infer the normalized source of a pure λ function on Haskell, such that:

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

?

Answer 1

Yes, you can, but you need to provide the spine of the type of your function, so it doesn't work for ULC. See also the whole lecture notes.

But as Daniel Wagner says you can just use HOAS.

There is also another opportunity: here is something that looks like HOAS, but is FOAS actually, and all you need is suitable normalization by evaluation (in terms of quote, in terms of reify & reflect). pigworker also wrote a Haskell version of the Jigger, but I can't find it.

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

EDIT

Here is some HOAS-related code:

{-# 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 = f x
f     # x = App f x

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 f x) = 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

Also, instead of writing this Lams, #s and stuff, you can parse string representations of lambda terms to HOAS — that's not harder than printing HOAS terms.