什么是主要类型？

Question

OCaml编译器有一个"-principal"选项,邮件列表中有时会提到术语"主体类型".究竟是什么意思？维基百科中的定义是递归的,因为它假设读者已经熟悉这个概念.

Answer 1

类型推断的过程是在给定用户编写的程序的情况下猜测该程序的类型.通常,给定程序可能有几种正确的类型.例如,程序fun x -> x可以给出类型int -> int和bool -> bool.

给定一个程序,如果所有其他psosible类型都是此类型的特化(实例),则该程序的类型是主要的,如果它是可以赋予​​该程序的最通用类型.在我的fun x -> x例子中,多态'a -> 'a是一种主要类型.

在某些类型的系统中,主要类型并不总是存在.你有一个程序P有两个可能的类型T1和T2,没有人比另一个更普遍的.例如,在一些数字运算符被重载的系统中,程序fun x -> x + x可以被赋予类型int -> int和类型float -> float,并且没有包含两者的类型.这对于推理引擎来说是一个问题,因为它意味着它必须做出任意选择,选择一种可能的类型,而不知道它是否是用户想要的类型.如果您有主要类型,则推理过程不需要做出任何选择.

(为了解决这个例子你可以:(1)不重载算术运算符(2)做出任意选择(这就是F#做的iirc)(3)拒绝程序并要求类型注释去除歧义(4)有更多表达类型,如Haskell's Num a => a -> a.)

基于Hindley-Milner类型推断的OCaml语言的"简单"子集具有主要类型.这意味着推理引擎始终做正确的事情(给定可能类型的规范).类型系统的一些更高级的方面(例如,多态字段和方法)失去了这个属性:在某些情况下,类型系统找不到最通用的类​​型,或者找到最通用的类​​型将需要明智的更复杂的计算.类型推理引擎(通常试图快速).该-principal选项是一个旋钮,如果我没记错的话:

• 失败是某种情况下类型检查器否则会接受非主体解决方案(做出任意选择)
• 更加努力地寻找主要解决方案,代价是更长的类型检查时间和内存使用量

我对这个标志不太熟悉(我更喜欢避免使用太高级的类型系统功能,所以我的程序通常不用担心),所以你必须仔细检查一下,但这是个粗略的想法.这个标志在我看来相对不重要(你通常不需要关心),但主要类型的概念确实是ML语言理论的重要组成部分.

如果您想进一步了解,还有两个技术细节:

• "主要类型"的ML概念是在固定类型环境下是否存在最普遍类型的问题; 一些作者研究了它们是否存在最普遍(环境,类型)对的问题,即所谓的"主要打字"; 这是一个更难的问题(您必须推断出您对其他模块的期望,而在ML中,您将获得您所依赖的外部模块的签名;并且推断多态性非常困难),这在大多数ML启发的编程中都没有使用语言.

• 对于类型系统的设计者来说,主要类型的存在是一种微妙的平衡.如果从ML类型系统中删除功能(多态,类型等'a -> 'a),则会失去公主性,但如果增加功率(从ML到具有更具表现力的多态类型的System F),您也可能会失去公国性.您可以通过转移到更复杂的类型系统(如MLF)来重新获得丢失的公规,但这是一个难题.

在实践中,相当大一部分编程语言设计者最近放弃了公国性的概念.他们希望拥有更多雄心勃勃的类型系统(依赖类型等),因为它们太难以寻求公正性,所以他们用非主要推​​理来满足自己:如果推理引擎可以找到某种类型,那就已经很好了,让我们不要结果的一般性很难.Jacam Garrigue,OCaml类型系统的主要维护者,仍然非常关心它,我认为这是OCaml编程语言研究的一个有趣的方面.

Answer 2

为了对Gasche的解释稍作一点,这里是一个例子,从OCaml自己的测试套件中偷走,在那里出现公国或缺乏公国.免责声明:这使用对象.

class c = object method id : 'a. 'a -> 'a = fun x -> x end;;
type u = c option;;
let just = function None -> failwith "just" | Some x -> x;;
let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
let g x =
  let none = (fun y -> ignore [y;(None:u)]; y) None in
  let x = List.hd [Some x; none] in (just x)#id;;
let h x =
  let none = let y = None in ignore [y;(None:u)]; y in 
  let x = List.hd [Some x; none] in (just x)#id;;

在顶级会话中运行时,您将获得:

#     val f : c -> 'a -> 'a = <fun>
#     val g : c -> 'a -> 'a = <fun>
#     val h : < id : 'a; .. > -> 'a = <fun>

这些函数执行完全相同的操作但分配了不同的类型!

如果使用该-principal选项调用OCaml ,前两个示例将触发:

Warning 18: this use of a polymorphic method is not principal.

有趣的是,如果替换'a为hwith 的类型'a -> 'a,则得到与fand 完全相同的类型g,因为类型c只是类型缩写(即扩展为)< id: 'a -> 'a; .. >.

编译器想要告诉程序员的是,有两种合适的类型f和g,并且没有标准可以帮助OCaml决定哪一个是"最好的"(和"最好",我的意思是"主要",当然!).