米尔纳让多态性成为2级特征吗? [英] Is Milner let polymorphism a rank 2 feature?

问题描述

let a = b in c 可以被认为是(\ a-> c)b 的语法糖，但是在类型设置中，通常不是案子.例如，在米尔纳演算中，让a = \ x->x in(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.

我的问题是:

• 是否让多态性成为在米尔纳演算的原本排名1的世界中偷偷溜走的2级特征?

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

具有单独的 let 构造的目的似乎是指定哪些类型应由类型检查器概括，而哪些则不能.它还有其他目的吗?是否有任何理由扩展功能更强大的系统，例如具有单独的 let 的系统F不是糖吗?是否有关于米尔纳演算设计原理的文章对我而言似乎不再显而易见?

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->中最通用的类​​型吗?(系统F中为True，则为1)?

是否在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?

一些说明:

• 通过等价，我是指等价模类型注释."F法拉教堂"是否是正确的说法?

• 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)应用于静态已知的参数.也就是说，我们可以首先对自变量"(即本地定义)以进行类型重建以找到其(多态的)类型；然后将找到的类型分配给参数"(definiendum);然后，最后在扩展名中键入主体输入上下文.

• 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.

请注意，这比普通的2级类型容易得多推断.

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

请注意，严格来说，如果您要求definiendum带有类型注释，则..中的.. = ..仅是系统F中的语法糖:let ..:.. = ....

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中(\ a :: T->(a True，a 1))中T的两种解决方案:forall b.(全部a.a-> b)->(b，b)和全部c d.(总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?

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