编译器如何确定sml中的类型

Question

我得到了以下代码，并被要求确定类型。

exception Break;
fn f => fn a => fn b =>
    (f(raise Break)
       handle Break => if (f a) then a else raise Break)
          handle Break => if not(f a) then a else b;

我知道这个函数在所有情况下都接受 f、a 和 b 并输出 a，所以它必须等价于：

fn f => fn a => fn b => a

类型：

'a -> 'b -> 'c -> 'b

因为 'if( f a)' 我们可以推导出 'a 必须是一个接受类型 'b 并输出布尔值的函数，否则它将无法工作。

('b->bool) -> 'b -> 'c -> 'b

re done so 'a is the beginning:

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

是我从中得到的最终答案。但是，当我在命令提示符中输入它时，我得到以下类型：

(bool->bool) -> bool -> bool -> bool

我错过了什么？ 'a 和 'b（来自我的最终类型评估）在什么时候专门用于 bool？

Answer 1

编译器如何判断sml中的类型

标准 ML 使用Damas-Hindley-Milner type inference，但有几种算法可以解决most general type，特别是算法 W。类型推断规则在例如

• A Generalized Let-Polymorphic Type Inference Algorithm[PS]，其实主要是提出了一种效率更高的替代算法G，但是介绍非常容易阅读，并且给出了一个推断小表达式类型的完整示例。
• So you still don't understand Hindley-Milner?，它引入了足够的类型理论来解释 StackOverflow 问题 "What part of Milner-Hindley do you not understand?"。

'a 和 'b 什么时候专门用于 bool？

'a 和 'b 专门用于 bool 的确切点取决于所使用的算法。我将跳过一些步骤，其中表达式被赋予类型并且这些类型是统一的。

当它说if (f a) then a else raise Break时，那么

• a : t₁
• f : t₁ → bool
• if ... : t₁

同样，当它说if not (f a) then a else b时，我们也有这个

• b : t₁

最后，f (raise Break) handle Break => if ... then a else ... 告诉我们

• f (raise Break) : bool
• t₁ = bool，因为f (raise Break) 和if ... then a else ... 必须具有相同的类型。

您缺少的部分可能是意识到x handle ... => y、x 和y 必须具有相同的类型。否则，您将拥有一个根据是否引发异常来更改类型的表达式。当在编译期间解析类型并且在运行时抛出异常时，这是不可能的。与此相关的一个实际示例是否定测试，其中handle ... 左侧的类型被强制为右侧的类型：

val factorial_robust_test = (factorial -1; false)
                            handle Domain => true
                                 | Overflow => false
                                 | _ => false