Value restriction,从OCaml到F#
Value Restriction是什么? Value restriction是用于控制类型推断能否对值声明进行多态泛化的规则(MLton原文:“The value restriction is a rule that governs when type inference is allowed to polymorphically generalize a value declaration.”)。常出现在ML系的语言中,如SML,OCaml,F#中,其实value restriction产生的本质原因是为了保证类型系统在结合参数多态与命令式特性(imperative feature,如ref)时候的可靠性(soundness)。一个典型的例子就是: 1 2 3 4 5 6 // 如果没有value restriction let x = ref None // 'a option ref let y: int option ref = x // type checked let z: string option ref = x // type checked let () = y := Some 2 // type checked let v: string = !z // 破坏了类型安全 限制了什么? 简单来讲,value restriction限制了类型泛化只能发生在表达式的右边是句法意义上的值。那么什么是句法意义上的值呢,SML的语言规范上明确给出了什么样的表达式是句法意义上的值(准确来说是non-expansive): 常量,如13,"string" 变量,如x,y 函数,如fn x => e 除了ref以外的构造函数在值上的调用,如Foo v 类型上受约束的值,如v: t 每一个元素都是值的tuple, 如(v1, v2, v3) 每一个字段都是值的record, 如{l1 = v1, l2 = v2} 每一个元素都是值的list, 如[v1, v2, v3] 确切的来讲,只要是协变(covariant)的类型并且不和可变的特性相结合,那么它总是可以类型安全的泛化(OCaml manual原文:“As a corollary, covariant variables will never denote mutable locations and can be safely generalized.”)。即: ...