在 Haskell 中去掉 let

Question

我可能应该首先提到我对 Haskell 很陌生。在 Haskell 中保留 let 表达式有什么特别的原因吗？

我知道 Haskell 去掉了 rec 关键字，该关键字对应于 let 语句的 Y-combinator 部分，表明它是递归的。为什么他们没有完全摆脱let 声明？

如果他们这样做了，那么语句在某种程度上似乎会更具迭代性。例如，类似：

let y = 1+2
    z = 4+6
    in y+z

应该是：

y = 1+2
z = 4+6
y+z

对于刚接触函数式编程的人来说，这更易读、更容易理解。我能想到保留它的唯一原因是这样的：

aaa = let y = 1+2
          z = 4+6
          in  y+z

如果没有let，这看起来会是这样，我认为这最终会成为模棱两可的语法：

aaa = 
  y = 1+2
  z = 4+6
  y+z

但如果 Haskell 不忽略空格，并且代码块/范围的工作方式与 Python 类似，它是否能够删除 let？

是否有更充分的理由保留let？

对不起，如果这个问题看起来很愚蠢，我只是想更多地了解它为什么在那里。

Answer 1

从句法上讲，您可以轻松想象没有let 的语言。如果需要，我们可以立即在 Haskell 中生成它，只需依赖 where。除此之外还有许多可能的语法。

---

从语义上讲，你可能认为 let 可以翻译成这样的东西

let x = e in g      ==>    (\x -> g) e

事实上，在运行时这两个表达式是相同的（模递归绑定，但可以使用fix 来实现）。然而，传统上，let 具有特殊的类型语义（连同where 和顶级名称定义......所有这些实际上都是let 的语法糖）。

---

特别是，在构成 Haskell 基础的 Hindley-Milner 类型系统中，有一个 let-generalization 的概念。直观地说，它考虑了我们将函数升级为最多态形式的情况。特别是，如果我们有一个函数出现在某个地方的表达式中，其类型类似于

a -> b -> c

a、b 和 c 这些变量在该表达式中可能已经或可能没有意义。特别是，它们被假定为固定但未知的类型。将其与类型进行比较

forall a b c. a -> b -> c

其中包含 多态性 的概念，即立即声明，即使环境中恰好有类型变量 a、b 和 c 可用，这些引用是新鲜的。

这是 HM 推理算法中非常重要的一步，因为它是生成多态性的方式，从而允许 HM 达到其更一般的类型。不幸的是，我们无法随时执行此步骤 - 必须在受控点执行。

这就是let-generalization 所做的：它说当类型被let-绑定到特定名称时，它们应该被泛化为多态类型。当它们仅作为参数传递给函数时，就不会发生这种概括。

---

因此，最终，您需要一种“let”形式来运行 HM 推理算法。此外，尽管它们具有相同的运行时特性，但它不能只是函数应用程序的语法糖。

在语法上，这个“let”概念可能被称为let 或where，或者按照顶级名称绑定的约定（这三个都在 Haskell 中可用）。只要它存在并且是在人们期望多态性的地方生成绑定名称的主要方法，那么它就会有正确的行为。

Answer 2

Haskell 和其他函数式语言使用let 有重要原因。我将尝试逐步描述它们：

类型变量的量化

Haskell 和其他函数式语言中使用的Damas-Hindley-Milner type system 允许多态类型，但类型量词只允许在给定类型表达式的前面。例如，如果我们写

const :: a -> b -> a
const x y = x

那么const的类型是多态的，它被隐式地普遍量化为

∀a.∀b. a -> b -> a

和const 可以专门化为我们通过用两个类型表达式替换a 和b 获得的任何类型。

但是，类型系统不允许在类型表达式中使用量词，例如

(∀a. a -> a) -> (∀b. b -> b)

这种类型在System F 中是允许的，但是类型检查和类型推断是不可判定的，这意味着编译器将无法为我们推断类型，我们必须用类型显式注释表达式。

(很长一段时间以来，系统 F 中类型检查的可判定性问题一直是开放的，有时它被称为“一个令人尴尬的开放性问题”，因为除此之外的许多其他系统都证明了不可判定性，直到 1994 年被乔·威尔斯证明。）

（GHC 允许您使用 RankNTypes 扩展启用此类显式内部量词，但如前所述，无法自动推断类型。）

lambda 抽象的类型

考虑表达式λx.M，或者用Haskell表示法\x -> M， 其中M 是包含x 的某个术语。如果x的类型是a，M的类型是b，那么整个表达式的类型就是λx.M : a → b。由于上述限制，a 不能包含 ∀，因此 x 的类型不能包含类型量词，它不能是多态的（或者换句话说它必须是 单态）。

为什么 lambda 抽象还不够

考虑这个简单的 Haskell 程序：

i :: a -> a
i x = x

foo :: a -> a
foo = i i

让我们暂时忽略foo 不是很有用。重点是foo定义中的id是用两种不同的类型实例化的。第一个

i :: (a -> a) -> (a -> a)

第二个

i :: a -> a

现在，如果我们尝试将此程序转换为没有let 的纯 lambda 演算语法，我们最终会得到

(λi.i i)(λx.x)

其中第一部分是foo 的定义，第二部分是i 的定义。但是这个词不会进行类型检查。问题是i 必须具有单态类型（如上所述），但我们需要它是多态的，以便我们可以将i 实例化为两种不同的类型。

确实，如果您尝试在 Haskell 中键入 i -> i i，它将失败。没有可以分配给i 的单态类型，以便i i 进行类型检查。

let 解决问题

如果我们写let i x = x in i i，情况就不同了。与上一段不同，这里没有 lambda，没有像 λi.i i 这样的自包含表达式，我们需要抽象变量 i 的多态类型。因此let 可以允许i 具有多态类型，在这种情况下∀a.a → a 和i i 类型检查。

如果没有let，如果我们编译一个 Haskell 程序并将其转换为单个 lambda 项，则必须为每个函数分配一个单态类型！这将毫无用处。

所以let 是一种基本结构，它允许基于 Damas-Hindley-Milner 类型系统的语言中的多态。

Answer 3

Haskell 的let 看起来确实如此的部分原因也是它管理缩进敏感性的一致方式。每个缩进敏感结构都以相同的方式工作：首先有一个引入关键字（let、where、do、of）；然后下一个标记的位置决定了这个块的缩进级别；以及从同一级别开始的后续行被认为是块中的新元素。这就是为什么你可以拥有

let a = 1
    b = 2
in a + b

或

let
  a = 1
  b = 2
in a + b

但不是

let a = 1
  b = 2
in a + b

我认为实际上可能有基于无关键字缩进的绑定而不会使语法在技术上模棱两可。但我认为当前的一致性是有价值的，至少对于最小意外的原则是这样。一旦你看到一个缩进敏感结构是如何工作的，它们的工作原理都是一样的。作为奖励，它们都具有相同的缩进不敏感等价物。这个

keyword <element 1>
        <element 2>
        <element 3>

总是等价于

keyword { <element 1>; <element 2>; <element 3> }

事实上，作为一个以 F# 为主的开发者，这是我羡慕 Haskell 的一点：F# 的缩进规则更复杂，而且并不总是一致的。

Answer 4

History of Haskell 说明了 Haskell 早已接受复杂的表面语法这一事实。

我们花了一些时间来确定风格选择，就像我们在这里所做的那样，但一旦我们这样做了，我们就开始激烈争论哪种风格“更好”。一个潜在的假设是，如果可能的话，应该“只有一种方法来做某事”，例如，同时拥有 let 和 where 将是多余和混乱的。

最后，我们放弃了基本假设，并为两种样式提供了完整的句法支持。这似乎是一个经典的委员会决定，但目前的作者认为这是一个不错的选择，我们现在认为这是该语言的优势。不同的结构有不同的细微差别，真正的程序员在实践中确实会同时使用 let 和 where、守卫和条件、模式匹配定义和 case 表达式——不仅在同一个程序中，有时在同一个函数定义中。确实，额外的句法糖使语言看起来更精致，但它是一种表面上的复杂性，很容易通过纯句法转换来解释。

Answer 5

这不是一个愚蠢的问题。这是完全合理的。

首先，let/in 绑定在语法上是明确的，并且可以以简单的机械方式重写为 lambda。

其次，正因为如此，let ... in ... 是一个表达式：也就是说，它可以写在任何允许表达式的地方。相比之下，您建议的语法更类似于 where，它绑定到周围的语法结构，例如函数定义的模式匹配行。

人们也可能会争辩说您建议的语法在风格上过于强制性，但这肯定是主观的。

您可能更喜欢使用where 而不是let。许多 Haskell 开发人员都这样做。这是一个合理的选择。

Answer 6

let 的存在是有充分理由的：

• let 可以在 do 表示法中使用。
• 它可以在列表理解中使用。
• 可以在here提到的函数定义中方便地使用。

您提供以下示例作为let 的替代方案：

y = 1+2
z = 4+6
y+z

上面的例子不会进行类型检查，y 和z 也会导致全局命名空间的污染，使用let 可以避免。