haskell - Milner 是否让多态性成为 2 级特征？

Question

let a = b in c可以被认为是 (\a -> c) b 的语法糖。 ，但在一般的打字设置中，情况并非如此。例如，在米尔纳微积分 let a = \x -> x in (a True, a 1)是可打字的，但看起来等价的 (\a -> (a True, a 1)) (\x -> x)不是。

然而，后者在系统 F 中是可键入的，第一个 lambda 具有等级 2 类型。

我的问题是:

让多态性成为 Milner 演算的其他 1 级世界中偷偷潜入的 2 级特征吗？

有单独的let的目的构造似乎指定了哪些类型应该由类型检查器概括，哪些不是。它还有其他用途吗？是否有任何理由扩展更强大的系统，例如系统 F 带有单独的 let哪个不是糖？是否有任何关于米尔纳微积分设计背后原理的论文对我来说似乎不再明显？

\a -> (a True, a 1) 有没有最通用的类​​型在系统 F 中？

是否存在在 beta 扩展下封闭的类型系统？ IE。如果 P 是可类型化的且 M N = P 那么 M 是可类型化的吗？

一些澄清:

等价是指等价模类型注释。 “System F a la Church”是正确的说法吗？

我知道通常主类型属性在 F 中不成立，但我的特定术语可能存在主类型。

作者 let我的意思是 let 的非递归风格.使用递归 let 扩展系统 F 显然很有用，因为它允许不终止。

Answer 1

W.r.t.对于提出的四个问题:

在这个问题上的一个关键见解是，不仅仅是输入一个
具有潜在多态参数类型的 lambda 抽象，我们
正在键入(1)只应用一次的(加糖的)抽象
而且，即 (2) 应用于静态已知参数。
也就是说，我们可以首先将“论据”(即
本地定义)类型重建以找到它的
(多态)类型；然后将找到的类型分配给“参数”
(被定罪)；然后，最后，在扩展中键入正文
类型上下文。

请注意，这比一般 rank-2 类型容易得多
推理。

请注意，严格来说，let .. = .. in .. 只是系统 F 中的语法糖，如果您要求定义项带有类型注释:let .. : .. = .. in .. 。

下面是系统 F 中 T in (\a::T -> (a True, a 1)) 的两个解:forall b。 (forall a.a -> b) -> (b, b) 和 forall c d。 (forall a b. a -> b) -> (c, d)。请注意，它们中的任何一个都不比另一个更通用。通常，系统 F 不接受主体类型。

我想这适用于简单类型的 lambda 演算？