Milner 是否让多态性成为 2 级特征? [英] Is Milner let polymorphism a rank 2 feature?

问题描述

let a = b in c 可以被认为是 (a -> c) b 的语法糖，但在一般的类型化设置中它不是案子.例如，在 Milner 演算中 let a = x ->;x in (a True, a 1) 是可键入的，但看似等效的 (a -> (a True, a 1)) (x -> x) 不是.

let a = b in c can be thought as a syntactic sugar for (a -> c) b, but in a typed setting in general it's not the case. For example, in the Milner calculus let a = x -> x in (a True, a 1) is typable, but seemingly equivalent (a -> (a True, a 1)) (x -> x) is not.

但是，后者在系统 F 中是可键入的，第一个 lambda 为 2 级类型.

However, the latter is typable in System F with a rank 2 type for the first lambda.

我的问题是:

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

• Is let polymorphism a rank 2 feature that sneaked secretly in the otherwise rank 1 world of Milner calculus?

拥有单独的 let 构造的目的似乎是指定哪些类型应该由类型检查器泛化，哪些不是.它还有其他用途吗?是否有任何理由扩展更强大的系统，例如系统 F 带有单独的 let 哪个不是糖?是否有任何关于米尔纳微积分设计原理的论文在我看来不再显而易见?

The purpose of having of separate let construct seems to specify which types should be generalized by type checker, and which are not. Does it serve any other purposes? Are there any reasons to extend more powerful systems e.g. System F with separate let which is not sugar? Are there any papers on the rationale behind the design of the Milner calculus which no longer seems obvious to me?

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

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

Are there type systems closed under beta expansion? I.e. if P is typable and M N = P then M is typable?

一些说明:

• 等价是指等价模类型注释.'System F a la Church' 是正确的说法吗?

• By equivalence I mean equivalence modulo type annotations. Is 'System F a la Church' the correct term for that?

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

I know that in general the principal typing property doesn't hold in F, but a principal type could exist for my particular term.

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

By let I mean the non-recursive flavour of let. Extension of system F with recursive let is obviously useful as it allows for non-termination.

推荐答案

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

W.r.t. to the four questions asked:

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

• A key insight in this matter is that rather than just typing a lambda-abstraction with a potentially polymorphic argument type, we are typing a (sugared) abstraction that is (1) applied exactly once and, moreover, that is (2) applied to a statically known argument. That is, we can first subject the "argument" (i.e. the definiens of the local definition) to type reconstruction to find its (polymorphic) type; then assign the found type to the "parameter" (the definiendum); and then, finally, type the body in the extended type context.

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

Note that that is considerably more easy than general rank-2 type inference.

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

Note that, strictly speaking, let .. = .. in .. is only syntactic sugar in System F if you demand that the definiendum carries a type annotation: 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 不接受主体类型.

Here are two solutions for T in (a :: T -> (a True, a 1)) in System F: forall b. (forall a. a -> b) -> (b, b) and forall c d. (forall a b. a -> b) -> (c, d). Note that neither one of them is more general than the other. In general, System F does not admit principal types.

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

I suppose this holds for the simply typed lambda-calculus?

这篇关于Milner 是否让多态性成为 2 级特征?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！