编译器如何确定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(fa)'我们可以得出'a必须是一个接受类型'b的函数并输出一个布尔值,否则它将不起作用.

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

这样做'a是开始:

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

是我得到的最终答案.但是,当我在命令提示符下键入它时,我得到以下类型:

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

我错过了什么？'a和'b(来自我的最终类型评估)在什么时候专注于bool？

Answer 1

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

标准ML使用Damas-Hindley-Milner类型推断,但有几种算法可用于解析最常见的类型,特别是算法W.类型推理规则在例如

• 一种广义Let-Polymorphic类型推理算法 [PS],它实际上主要提供了一种更有效的替代算法G,但是引入非常容易阅读并给出了推断小表达式类型的完整示例.
• 所以你还是不明白Hindley-Milner？,它引入了足够的类型理论来解释StackOverflow问题"Milner-Hindley的哪个部分你不明白？" .

在什么时候'a和'b专门用于布尔？

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

当它说if (f a) then a else raise Break,然后

• a:t ₁
• f:t ₁ →布尔
• if ...:t ₁

同样地,当它说if not (f a) then a else b,我们还有那个

• b:t ₁

最后,f (raise Break) handle Break => if ... then a else ...给我们这个

• f (raise Break):布尔
• 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