Haskell 中高阶函数的 Lambda 表达式

Question

在 this book 之后，Haskell 中的所有内容都是 λ-calculus：像 f(x)=x+1 这样的函数可以在 Haskell 中编写为 f = \x -> x+1 和 λ 表达式中的 λx.x+1。

• 对于像map::(a -> b) -> [a] -> [b] 这样的高阶函数，λ 表达式是什么？或λ 函数($) :: (a -> b) -> a -> b 的表达式？
• 函数列表（即f::[a->b]）呢？一个具体的例子可以是h = map (\f x -> f x 5) [(-),(+)]。那么λ 表示法类似于h = map (λfx.f(x(5)) [(λab.a-b),(λab.a+b)]?

我只熟悉 alpha 转换、beta 缩减等过程，但如果您以 λ 术语分解函数列表，将不胜感激，无需简化。

谢谢。

Answer 1

首先，

Haskell 中的一切都是 λ-演算

这并不正确。 Haskell 有许多与无类型 λ 演算中的东西不对应的特性。也许他们的意思是它可以编译为λ-演算，但这很明显，“任何图灵完备的语言......” jadda jadda。

像map :: (a -> b) -> [a] -> [b]这样的高阶函数的λ表达式是什么

这里有两个不相关的问题。对于直接 λ 平移，“高阶函数”部分完全没有问题，正如 cmets 已经说过的那样

($) = \f -> \x -> f x   -- λf.λx.fx

或者

($) = \f x -> f x
($) = \f -> f  -- by η-reduction

（在 Haskell 中我们会进一步缩短为 ($) = id）。

另一件事是map 是在代数数据类型上定义的递归函数，将其转换为无类型的 λ 演算将导致我们与 Haskell 相去甚远。将其转换为包含模式匹配 (case) 和 let-bindings 的 λ-flavor 更有指导意义，这实际上是 GHC 在编译程序时所做的。想出来很容易

map = \f l -> case l of
               [] -> []
               (x:xs) -> f x : map f xs

...或避免在顶级绑定上递归

map = \f -> let go l = case l of
                        [] -> []
                        (x:xs) -> f x : go xs
            in go

我们不能像那样摆脱let，因为λ-演算不直接支持递归。但是递归也可以用定点组合器来表示；与无类型 λ 演算不同，我们不能自己定义 Y 组合子，但我们可以假设 fix :: (a -> a) -> a 是一个原语。结果证明它完成了与递归 let-binding 几乎完全相同的工作，然后立即对其进行评估：

map = \f -> fix ( \go l -> case l of
                            [] -> []
                            (x:xs) -> f x : go xs )

为此构建一个 λ 风格的语法，

map = λf.fix(λg.λl.{l?[]⟼ []; (x:s)⟼fx:gs})

Answer 2

（警告：据我所知，以下代码包含一个错误，导致导致公式 map f (x:xs) == f x : map f (map f xs) 的定义。）

---

继续the answer @leftaroundabout，

MAP = λf.Y(λg.λl.l(NIL)(λxs.CONS(fx)(gs)))

Y 是一个定点组合器：

Y = λg.(λx.g(xx))(λx.g(xx))   -- Yg == g(Yg)

-- MAP(f) == (λl.l(NIL)(λxs.CONS(fx)(MAP(f)s)))

列表是接受两个参数以适当应用的 lambda 术语，第一个是如果列表为空，第二个如果不是：

-- constructs an empty list
NIL = λnc.n

-- constructs a non-empty list from its two constituent parts
CONS = λadnc.ca(dnc)

因此例如CONS(1)(CONS(2)NIL) 返回的术语将由 MAP(f) 转换为

MAP(f)(NIL)nc -> (NIL)nc -> n
MAP(f)(CONS(2)NIL)nc -> CONS(2)NIL(NIL)(λxs.CONS(fx)(MAP(f)s))nc
                     -> (λxs.CONS(fx)(MAP(f)s))(2)(NIL)nc
                     -> CONS(f(2))(MAP(f)(NIL))nc
                     -> c(f(2))(MAP(f)(NIL)nc)
                     -> c(f(2))((NIL)nc)
                     -> c(f(2))n
MAP(f)(CONS(1)(CONS(2)NIL))nc ->
                     -> CONS(1)(CONS(2)NIL)(NIL)(λxs.CONS(fx)(MAP(f)s))nc
                     -> (λxs.CONS(fx)(MAP(f)s))(1)(CONS(2)NIL)nc
                     -> CONS(f(1))(MAP(f)(CONS(2)NIL))nc
                     -> c(f(1))(MAP(f)(CONS(2)NIL)nc)
                     -> ....
                     -> c(f(1))(c(f(2))n)