May 15, 2014

今年寒假看了一下Clean语言，给我留下的印象：难用，不过它也有一些有趣的特性，例如uniqueness typing和对泛型编程的支持（当然还有其他我不太感兴趣的），这篇主要记录一下uniqueness typing。

纯函数式编程语言里的IO

这里，“纯”当然是指Haskell推崇的纯，怎样在一个纯函数式语言里表达IO操作呢？Haskell的答案是IO Monad，而Clean的答案是uniqueness typing。

假设我们的语言里有一个函数getLine从stdin获取输入，getLine的每次调用会有副作用，可以返回不同的值，要怎样用纯函数来表达getLine呢？一个想法就是让getLine接受外部状态作为参数，返回一个新的状态和输入的字符串，getLine的类型就可以表示成World -> (String, World)，我们可以这样读入两行：

getTwoLine world0 =
    let (line1, world1) = getLine world0
        (line2, world2) = getLine world1
    in ((line1, line2), world2)

可以发现，其实我们是通过不断传递新的World参数来能表达语句间的数据依赖，从而让运行时按顺序执行语句。但是这里有一个问题，我们可能传递错了或重复传递：

badTwoLine world0 =
    let (line1, world1) = getLine world0
        (line2, world2) = getLine world0  -- use world0 the second time
    in ((line1, line2), world2)

为了解决这个问题，IO Monad会隐式传递World，而uniqueness typing会禁止一个World被重复使用（准确说法是不会被共享）。

Uniqueness typing

在Clean的类型系统里，一个值除了有类型外，还会有一个唯一性属性（uniqueness attribute）。如果一个值是唯一的（用*表示），它就不能被多次使用，一个函数使用完一个唯一值之后，返回值中也必须有一个新的唯一值，然后继续被传递。一些函数既能作用在唯一值，又能作用在非唯一值上，这时就能用匿名属性（.）或者属性变量（就像类型变量一样）来表示。

例如上面的badTwoLine函数，world0被使用了两次，Clean编译器能发现这个错误，说world0需要的唯一性不能被满足。

除此之外，还有不少细节问题，例如数据结构里元素的唯一性会向外传播，属性间有子类型关系，闭包的唯一性得等，整个属性系统变得很复杂，还好编译器能推导大部分的属性，化简了不少工作。

惰性求值

Clean程序会从Start :: *World -> *World函数开始执行，运行时系统会向Start传进一个唯一的World（实际上只是个数字），从这个唯一的World我们可以生成新的World或其他唯一值，通过这些唯一值就能执行IO和控制程序执行的顺序，甚至可以原地修改数据，对性能优化也有帮助。

Clean的执行是基于图规约的惰性求值，整个程序就是一个图，这个图就是维一值传递的网络，开始于*World结束于*World，只有对最后的*World的求值有意义的路径才会被执行，其他都被忽略。例如下面的程序

Start world0 = world1
  where
    (_, file0, world1) = fopen "file" FReadText world0
    (_, char,  file1)  = freadc file0
    (_, world2)        = fclose file1 world1

// fopen  :: !{#Char} !Int !*f -> (!Bool,!*File,!*f)
// freadc :: !*File -> (!Bool,!Char,!*File)
// fclose :: !*File !*f -> (!Bool,!*f)

where部分按顺序读下来，

fopen用world0打开文件，返回world1和file0 :: *File
freadc从file0里读一个字符，返回file1
fclose用world1关闭file1，返回world2

但是，实际是2和3是不被执行的，因为Start返回的是world1，而world1的求值在第1步就完成了。为了让freadc和fclose被执行，Start必须返回一个依赖于freadc和fclose的*World，在这里就是world2。

这也是Clean程序的模式，从一个*World生成更多唯一值，最后回到*World。

Clean语言: Uniqueness Typing

纯函数式编程语言里的IO

Uniqueness typing

惰性求值