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.”)。即: ...

Functional Data Structure 2

Amortization Implementations with good amortized bounds are often simpler and faster than implementations with comparable worst-case bounds. Given a sequence of operations, we may wish to know the running time of the entire sequence, but not care about the running time of any individual operation. For instance, given a sequence of n operations, we may wish to bound the total running time of the sequence by O(n) without insisting than every individual operation run in O(1) time. We might be satisfied if a few operations run in O(log n) or even O(n) time, provided the total cost of the sequence is only O(n). This freedom opens up a wide design space of possible solutions, and often yields new solutions that are simpler and faster than worst-case solutions with equivalent bounds. ...

Functional Data Structure 1

Introduction To implement data structure in a functional way, there are two basic problems. First, from the point of view of designing and implementing efficient data structures, functional programming’s stricture against destructive updates(i.e. assignments) is a staggering handicap, tantamount to confiscating a master chef’s knives. Imperative data structures often rely on assignments in crucial ways, and so different solutions must be found for functional programs. The second difficulty is that functional data strcutures are expected to be more flexible than their imperative counterparts. In particular, when we update an imperative data structure we typically accept that the old version of the data strcuture will no longer be available, but when we update a functional data structure, we expect that both the old and the new version of the data structure will be available for further processing, this is called persistent, while the other is called ephemeral. And we are not surprised if the persistent version is more complicated and even less efficient that the ephemeral one. ...