Sml Church数字类型推断 [英] Sml Church numeral type inference

问题描述

我在SML中有此表达式，需要找到它的最通用类型.通过编译器运行时，我得到下面显示的内容.我将如何找到最通用的类​​型，不仅是此功能，还有其他功能，例如教堂数字功能二".

I have this expression in SML and need to find the most general type of it. When run through the compiler I get what it shows below. How would I go about finding what the most general type would be of not only this function but other functions like church numerals function "two".

val one = fn f => (fn x => f x)

为什么是这种类型:

('a -> 'b) -> 'a -> 'b

推荐答案

您要做的是，应用名为

What you do is, you apply a process called Hindley–Milner type inference.

一般原则包括三个步骤:

The general principle involves three steps:

1. 首先，我们为变量和表达式分配不确定类型(写为'Z，'Y，'X等).

• 如果表达式使用我们已经为其分配类型的变量，则可以使用它.例如，如果three已与类型int绑定，则在val nine = three * three中，我们知道three具有类型int.
• 如果表达式使用的变量我们已经将非平凡类型 scheme 分配给它(即，它是多态的)，则我们使用该方案，但将每个类型变量替换为不确定类型.例如，如果first已经与类型'a * 'b -> 'a绑定，则在val firstOfFirst = fn quartet => first (first quartet)中，我们将一个first分配为'Z * 'Y -> 'Z类型，将另一个分配给'X * 'W -> 'W类型.
• 如果表达式使用新绑定的变量(由fn或rec限定)，则该变量的所有出现都必须具有完全相同的类型—.这时不允许多态.例如，在fn f => (f 1, f "one")(最终会给出类型错误)中，我们最初将所有出现的f分配为单个类型'Z. (导致类型错误的原因是，我们后来需要将其精炼为int -> 'Y和string -> 'Y，这是矛盾的.这是因为Standard ML不支持

• If the expression uses a variable that we've already assigned a type to, then we use that. For example, if three has already been bound with type int, then in val nine = three * three, we know that the three has type int.
• If the expression uses a variable that we've already assigned a nontrivial type scheme to (i.e., it's polymorphic), then we use that scheme, but replace each type variable with an undetermined type. For example, if first has already been bound with type 'a * 'b -> 'a, then in val firstOfFirst = fn quartet => first (first quartet), we assign one first the type 'Z * 'Y -> 'Z and the other one the type 'X * 'W -> 'W.
• If the expression uses a newly-bound variable (scoped by fn or rec), then all occurrences of that variable have to have exact the same type — no polymorphism is allowed at this point. For example, in fn f => (f 1, f "one") (which ends up giving a type error), we initially assign all occurrences of f the single type 'Z. (The type error results because we later need to refine that to both int -> 'Y and string -> 'Y, and these are contradictory. This is because Standard ML doesn't support first-class polymorphism.)

在您的示例val one = fn f => (fn x => f x)中，我们可以将f的类型指定为'Z，将x的类型指定为'Y.

In your example, val one = fn f => (fn x => f x), we can assign f the type 'Z, and x the type 'Y.

接下来，我们执行类型统一，在此我们确定必须匹配的不同子表达式的类型的不同部分.例如，如果我们知道f的类型为'Z -> real，而i的类型为int，那么如果我们看到f i，则可以将'Z与int统一"并得出结论f具有类型int -> real.

Next, we perform type unification, where we identify different parts of the types of different sub-expressions that have to match. For example, if we know that f has type 'Z -> real and that i has type int, then if we see f i, we can "unify" the 'Z with the int and conclude that f has type int -> real.

• 类型统一有很多很多细节，但是我认为它们几乎都是您要假定的，因此我不再赘述.

在您的示例中，由于将f应用于x，因此我们可以将'Z与'Y -> ...统一，并最终为f指定类型'Y -> 'X.因此，整个表达式的类型为('Y -> 'X) -> 'Y -> 'X.

In your example, since f is applied to x, we can unify 'Z with 'Y -> ..., and end up assigning f the type 'Y -> 'X. So the expression as a whole has type ('Y -> 'X) -> 'Y -> 'X.

最后，我们执行类型概括.一旦我们执行了所有可以执行的统一操作—推论完所有关于类型的信息后-我们可以用绑定类型变量安全地替换未确定的类型.在您的情况下，我们可以为one指定类型∀αβ .((α →→ β) → 在α和β中，one具有类型(α>→<β) →<α →<β.在标准ML表示法中，我们不包括显式的∀β"部分；我们只写('a -> 'b) -> 'a -> 'b.

Lastly, we perform type generalization. Once we've performed all unifications that can be performed — once we've deduced everything we can about the types — we can safely replace the undetermined types with bound type variables. In your case, that lets us assign one the type-scheme ∀ αβ . (α → β) → α → β (meaning "for any and all types α and β, one has the type (α → β) → α → β"). In Standard ML notation, we don't include the explicit "∀ αβ" part; we just write ('a -> 'b) -> 'a -> 'b.

这篇关于Sml Church数字类型推断的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！