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

Question

让纯粹的λ函数成为除了抽象和应用之外的任何术语.在JavaScript上,可以通过将所有抽象应用于收集其参数列表的可变参数函数来推断纯函数的源代码.也就是说,这是可能的:

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

请参阅此要点上的lambdaSource代码.这个函数对我的兴趣特别有用,因为它允许我使用现有的JS引擎来标准化无类型的lambda演算表达式,比我自己编写的任何天真评估器快得多.此外,我知道λ-calculus函数可以在Haskell中用以下方式表示unsafeCoerce:

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

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

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

？

Answer 1

是的,您可以,但是您需要提供功能类型的主干,因此它不适用于ULC.另请参阅整个讲义.

但正如Daniel Wagner所说,你可以使用HOAS.

还有另一个机会:这里的东西,看起来像的高阶像差,但实际上FOAS,所有你需要的是通过评估合适的正常化(在报价方面,在具体化和体现的方面).pigworker还写了一个Haskell版本的Jigger,但我找不到它.

我们也可以做到这一点类型安全的类型理论:一个方法是使用升降条款(这需要一个假设),或者我们可以具体化 lambda项到他们PHOAS表示,然后转换PHOAS到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术语的字符串表示而不是写入Lams,#s和stuff,而不是打印HOAS术语.