在Haskell上有可能推断出一个纯λ函数的归一化源吗？

Question

假设一个纯λ函数是一个除了抽象和应用之外什么都没有的术语。在JavaScript上，通过对收集参数列表的各种函数应用所有抽象，可以推断出纯函数的源代码。也就是说，这是可能的：

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

关于这个要点，请参见lambdaSource的代码。这个函数对我的兴趣特别有用，因为它允许我使用现有的JS引擎规范非类型化的lambda演算表达式，比我自己编写的任何简单的计算器都快得多。此外，我知道λ-微积分函数可以在unsafecoerce的帮助下用Haskell表示：

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

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

Answer 1

是的，你可以，但你需要提供脊柱的类型，你的功能，所以它不工作的ULC。另见整个课堂讲稿。

但正如Daniel Wagner所说，你可以使用Hoas。

还有另一个机会：这里的东西看起来像HOAS，但实际上是FOAS，您所需要的只是通过评估进行适当的规范化（就引用而言，就reify和reflect而言）。猪工人还写了一个哈斯克尔版本的跳汰机，但我找不到它。

{-# 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

另外，不需要编写lams、#之类的东西，您可以将lambda术语的字符串表示形式解析为HOAS-这并不比打印HOAS术语更难。