Haskell 中高阶函数的 Lambda 表达式

Question

继this book之后，Haskell中的一切都是λ微积分：像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

首先，

everything in Haskell is λ-calculus

这是不正确的。 Haskell 有很多不符合无类型 λ 演算的特征。也许他们的意思是它可以编译为 λ-演算，但这很明显，“任何图灵完备的语言……”jadda jadda。

What is λ expression for a higher order function like map :: (a -> b) -> [a] -> [b]

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

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

或者

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

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

另一件事是 map 是一个定义在代数数据类型上的递归函数，将其转换为无类型的 λ-演算会使我们与 Haskell 相去甚远。将其转换为包含模式匹配 (case) 和 let-绑定的 λ-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 绑定几乎完全相同的工作，然后立即对其进行评估：

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)，据我所知。）

继续 by @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)

Haskell 中高阶函数的 Lambda 表达式

Lambda Expressions for Higher Order Function in Haskell

haskell

functional-programming

lambda-calculus

higher-order-functions