在函数调用中省略参数标签时类型推断失败可怕

Question

鉴于以下功能

let get_or ~default =
  function | Some a -> a
           | None -> default

如果使用标记的参数调用此函数,它将按预期工作:

let works = get_or ~default:4 (Some 2)

但如果省略标签,它就会失败:

let fails = get_or 4 (Some 2)

它变得更奇怪,但是,编译器在此处给出的错误消息是:

此表达式具有int类型,但表达式需要类型('a - >'b)选项

编译器不仅错误地推断它是一个选项,而且由于某种原因,它还从众所周知的魔术师的帽子中提取了一个函数类型!所以我很自然地想知道:它究竟来自哪里？对我的好奇心不那么重要,为什么不在这个特定情况下省略标签呢？

看到这个原因是一个互动示例的游乐场.

对于这个谜题的信用归结于@nachotoday的原因不和谐.

Answer 1

这是标记的参数,currying和一级函数之间的破坏性干扰的情况.该函数get_or具有类型

 val get_or: default:'a -> 'a option -> 'a 

带有标签参数的规则是当应用程序为total时可以省略标签.乍一看,这意味着如果一个适用get_or于两个参数,那么它就是一个完整的应用程序.但是返回类型get_or是多态(aka 'a)的事实会带来麻烦.考虑例如:

let id x = x
let x : _ -> _ = get_or (Some id) id ~default:id

这是有效的代码,其中get_or应用于三个参数,其中默认参数在第三个位置提供!

更进一步,令人惊讶的是,它仍然有效:

let y : default:_ -> _ -> - = get_or (Some id) id id

它产生了一个相当复杂的类型y.

这里的通用规则是,如果函数的返回类型是多态的,那么类型检查器永远不会知道函数应用程序是否是完全的; 因此永远不会遗漏标签.

回到你的例子,这意味着类型检查器读取

 get_or (4) (Some 2)

如

• 首先,get_or有类型default:'a -> 'a option -> 'a.尚未提供默认标签,因此结果将具有类型default:'r -> 'r
• 看着r在get_or 2 (Some 4),get_or有型 'a option -> 'a,从而get_or x:'a
• 然后get_or x:'a适用于y; 从而'a = 'b -> 'c
• 换句话说,我应该,x: ('b -> ' c) option 但我知道x:int.

这导致了类型检查器报告的矛盾,2预计是一个函数选项('a -> 'b) option,但显然是一个int.