是否可以推断 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)))))

由于缺少可变函数，我不知道如何在 Haskell 中实现 lambdaSource。是否有可能在 Haskell 上推断出纯 λ 函数的归一化源，这样：

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

?

Answer 1

是的，你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。

但是正如 Daniel Wagner 所说，您可以只使用 HOAS。

还有一个机会：这里是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也写了一个Haskell版本的Jigger，但是我没找到

我们也可以在类型论中安全地做到这一点：一种方法是使用liftable terms (which requires a postulate), or we can reify lambda terms into their PHOAS representation and then convert PHOAS to FOAS（这非常复杂）。

编辑

这是一些与 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 = 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

此外，您可以将 lambda 项的字符串表示解析为 HOAS，而不是编写此 Lam、# 之类的东西——这并不比打印 HOAS 项难。

是否可以推断 Haskell 上纯 λ 函数的归一化源？

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

algorithm

haskell

functional-programming

lambda-calculus