Programming Languages, UW, Part A - ML Basic & FP

Posted on 繁/简： set

毫无疑问的神课，不愧于 Coursera 上接近满分的评价。Dan Grossman 教授显然对 PL 领域十分 passionate 并且有很深的造诣，在上课的过程中都能感受到他的热情和对课程倾注的心血。

这门课介绍了 PL 中的很多基本概念，尤其强调函数式编程的设计哲学；对我来说确实是一个全新的范畴。

另外，课程提供的总结性质的 material 质量很高，这篇笔记远远无法覆盖其所有的精华内容。当遇到难以理解的概念时，记得一定要去查阅原材料。

Part A is a precisely specified introduction to functional programming built up piece-by-piece, using Standard ML as an example.


  This article is a self-administered course note.

  It will NOT cover any exam or assignment related content.


ML Basics

An ML program is a sequence of bindings.

绑定 (binding) 与我们熟悉的赋值语句 (assignment statement) 尽管形式相似，却有着本质的不同：最主要的区别在于 bindings 是 immutable 的，而 assignment statement 支持以赋值的形式 mutate 变量的值。

  • Each binding gets type-checked and (assume it type-checks) then evaluated.
  • What type of a binding has depends on a static environment or context, which is roughly the types of the preceding bindings.
  • How a binding is evaluated depends on a dynamic environment or just environment, which is roughly the values of the preceding bindings.

这也就是说，if x maps to some value v in some environment, it will forever map to v in that environment. There is NO assignment statement that changes x to map to a different value. 尽管你可以在之后引入新的 binding 来 shadows x，但这并不会改变之前的环境中 x 与 v 对应的事实。

接下来，我们看看 ML 如何处理 variable bindings 与 function bindings。

Variable Bindings

variable binding 的语法 (syntax) 如下：

1
var x = e;

e 是一个表达式 (expression)；注意表达式与值 (value) 之间的区别：A value is an expression that "has no more computation to do". Therefore, all values are expressions, but not all expressions are values.

  • We use current static environment to type-check e, and (if it type-checks) add x : t back to the static environment where t is the type of e.
  • We use current dynamic environment to evaluate e, and (if it type-checks) add x = v back to the dynamic environment where v is the value of e.

Function Bindings

function binding 的语法如下：

1
fun x0 (x1:t1, ..., xn:tn) = e

Binding x0 takes arguments x1, ..., xn of types t1, ..., tn and has an expression e for its body.

Type-checking:

  • Type-check the body e in a static environment that (in addition to all the earlier binding) maps x1 to t1, ... xn to tn and x0 to t1 * ... * tn -> t. Since x0 is in the environment, we can make recursive function calls, i.e., a function definition can use itself.
  • For the function binding to type-check, body e must have the type t, i.e., the result type of x0.
  • If the function binding type-checks, x0 : t1 * ... * tn -> t is added to the static environment. Note that the arguments are not added to the top-level static environment.

Note that t is never wrote down: it is up to the type-checker to figure out what t should be such that using it for the result type of x0 makes everything work out. This is called type inference.

Evaluation:

function bindings 的 evaluation 就比较 trivial 了，这是因为在 ML 中，A function is a value.

我们仅仅需要将 x0 加入 current dynamic environment 即可。As expected for recursion, x0 is in the dynamic environment in the function body and for subsequent bindings.

Function Call

function binding 的存在是为了支持 function calls。它的语法如下：

1
e0 (e1,...,en)

Typing rules:

若 e0 的类型为 t1 * ... * tn -> t 且 ei 的类型为 ti，则整个函数调用的类型为 t.

Evaluation rules:

我们使用调用处的环境 (environment at the point of the call) 来 evaluate e0 to v0, e1 to v1, ..., en to vn. 若 v0 是函数，则函数调用是 type-checked 的。

接下来，我们使用定义处的环境 (environment where the function is defined) extends 函数参数形成的 bindings x1 = v1, ..., xn = vn 来 evaluate 函数体。


First-Class Function

By first-class we mean that functions can be computed, passed, stored, etc. wherever other values can be computed passed stored, etc.

在函数式编程体系中，函数也是第一等公民：这是因为 All functions are values。函数就像所有其他类型的值一样，可以作为 higher-order 函数的参数，返回值，甚至可以被存储。

函数的 first-class 性质使得 function closure 的概念被提出，并进一步催生了匿名函数 (anonymous function)，高阶函数 (higher-order function)，函数的 combination，callback 与 currying 等机制。

一些典型的函数比如 map, filter, fold 等在函数式编程体系中可以很方便的实现。

The term higher-order function refers to the function that takes or returns other functions.

到底什么是函数式编程 (functional programming)？实际上，对此并没有一个准确的定义。但一般来说，函数式编程语言有以下特点：

  • 函数是第一等公民：using functions as values.
  • NOT using mutable data in most or all cases.
  • 函数式编程鼓励使用递归 (recursive) 与递归数据结构。(支持尾递归优化)
  • 函数式编程中的 function 最贴近数学中对函数的原始定义。
  • 使用 laziness 的特性。


Anonymous Function

匿名函数是没有名字的函数，因此其可以方便的作为其他函数的参数或者返回值。但这也使得它无法进行递归。原因在于：evaluate function bindings 时需要将函数的名字 x0 加入环境以实现后续的递归。

1
(fn x => e)

我们可以把关键字 fun 视为 syntactic sugar：下面这两个表达其实是一致的。

1
2
fun x = e
val x = fn x => e

在使用匿名函数时，要注意避免 unnecessary function wrapping：

1
2
fun nth_tail_poor (n, x) = n_times((fn y => tl y), n, x)
fun nth_tail_neat (n, x) = n_times(tl, n, x)


Currying

在 ML 中，每一个函数只有一个参数；多参数函数的形参本质上是一个包含多个变量的 tuple。

然而除此之外，有另一种方式可以实现所谓的多参数，那就是函数的 currying。即，通过匿名函数的嵌套实现类多参数函数结构，再通过语法糖进行等价转换。

注意第三条语句是第二条语句的 syntactic sugar，三个函数的作用完全相同。

1
2
3
fun p(x, y, z) = e
fun curry_p = fn x => fn y => fn z => e
fun curry_p2 x y z = e

通过 currying，我们还能实现函数的部分化应用 (partial application)，从而消除 redundant arguments。

1
2
fun curry_p x y z = ... z
fun partial_curry_p x y = ...

基于 tuple 实现的多参数函数可以与 currying 多参数函数相互转换。

1
2
fun uncurry f x y = f(x, y)
fun curry f (x, y) = f x y


Lexical Scope

在 ML 中，函数的 evaluation 遵循这样一条铁律 (之前在 function binding 部分中也介绍过)：

The body of a function is evaluated in the environment where the function is defined, not the environment where the function is called.

也就是说，函数体的 evaluation 依赖的是函数各个函数 bindings 与被定义时的环境。我们通过一个 silly example 来认识这一点。

1
2
3
4
5
val x = 1
fun f y = x + y
val x = 2
val y = 3
val z = f (x+y)

变量 z 的值是 6，而不是 5。在调用函数 f 的环境中，x 的值为 2，y 的值为 3，因此函数的参数 evaluates to 5。而在 evaluate 函数体时，我们参照的是函数 f 定义时的环境：在那里 x 还未被 shadow，其值为 1。而参数 y 又与 5 绑定，最后计算出来的值为 1 + 5 = 6。

这样的 semantics，就是词法作用域 lexical scope。比较来说，函数体与参数均在调用处的环境被 evaluate 的机制更加符合直觉，这种与 lexical scope 对立的 semantics 称为动态作用域 dynamic scope。

早期的编程语言大多是遵循 dynamic scope 的，但是很快程序员就发现了其致命问题：变量的 shadowing 常常会与这一机制产生冲突。一个最典型的例子如下：

1
2
3
4
var x = 3
fun f = x + 1 
var x = "hello"
var y = f

这一程序是 type-checked 的：x : int, f : null -> int, x (shadow) : string, y : int；但在 dynamic scope 中，y = 3 + "hello"，这破坏了类型一致性。而在 lexical scope 中这一程序则不会出现问题。

dynamic scope 还会导致许多其他的问题 (见 section3sum)，因此现在的绝大多数语言默认都采用 lexical scope 来作为函数 evaluation 的准则。但 dynamic scope 并没有完全消失：

  • 少数语言 (如 Racket) 仍然提供对 dynamic scope 的支持。
  • 一些特殊的编程 feature (如 exception) 遵循的是 dynamic scope。

When an exception is raised, evaluation has to look up which handle expression should be evaluated. This "look up" is done using the dynamic call stack, with no regard for the lexical sturcture of the program.


Environments and Closures

我们一直强调在函数式编程中，All functions are values。那么这个“值”具体是什么呢？

  • the code for the function.
  • the environment that was current when we created the function.

也就是说，function value 包括 code 与定义时的 environment 两部分；这个 pair 被称为函数闭包 function closure 或者闭包 closure。闭包的定义也是符合词法作用域 lexical scope 的。

我们不能单独访问 pair 中的任意一部分，对于 function value，我们能够执行的操作只有调用 call。这其实也是一种 encapsulation。我们能够发现，the closure overall is closed —— it has everything it needs to produce a function result given a function argument.

1
2
var x = 3
fun f = x + 1

在上例中，the binding fun f y = x + y bound f to a closure.

  • the code part is the function fn y => x + y.
  • the environment part maps x to 1.

在函数 f 闭包创建以后，无论在哪调用 f 最终返回的值都是 4。闭包保证了 evaluate 该函数的环境与调用它时的环境完全隔绝：这是对闭包的另一种理解。

注意，lexical scope 词法作用域是目前大多数编程语言遵循的 semantics；然而 closure 并不是所有语言都具有的；closure 是 function 的 value，因此其在函数式编程语言中是最常见的。


Type Inference

type inference 是 ML 一个十分优雅的特性。在我接触过的所有 (极其有限的) 语言中从未见过这个 feature。

Statically typed languages. Every binding has a type that is determined at compile-time; The type-checker is a compile-time procedure that either accepts or rejects a program.

Java, C, ML 都是 statically typed languages。与之相对的是 dynamically typed language，例如 Racket, Ruby, Python。动态类型语言在运行时才会确定 bindings 的类型；因此在这些语言中类型错误是一种 run-time error 而非 compile-time error。

与 Java 和 C 又不同，ML 的类型是隐式 (implicitly typed) 的，即我们几乎不需要声明 binding 的类型。这个 feature 真的非常的厉害，它使得：

  • binding 声明的流程大大简化；我们可以完全把类型的问题抛在一边。
  • 优雅的支持参数多态 (parametric polymorphism)。

这样做的代价就是，ML 的 type-checker 远比其他显式类型语言的复杂。在程序员不具体声明 binding 类型的前提下，type-checker 需要根据代码与 bindings 之间的关系推断 (infer) 出所有可能的 type annotations。如果不存在任何一种解，type-checker 将会拒绝 (reject) 该程序。

Parametric polymorphism, or more commonly generic types, lets functions take argument of any type. In ML, when the inferencer determines a function's argument or result "could be anything", the resulting type uses type variable 'a, 'b, etc.

注意，虽然 type inference 与多态联系紧密，但它们终究是两个独立的概念：举例来说，Java 支持泛型 (generics types)，但它是一种显式类型语言，不支持类型推断。

Undecidability

When we say type inference may be impossible, we mean this is the technical sense of undecidability, like the famous halting problem.

对于某些 type system，不存在一个有效的 type inference 能够同时满足以下三个条件：

  • the inference process always terminates.
  • the inference process always succeeds if inference is possible.
  • the inference process always fails if inference is not possible.

关于这一部分的详细内容将会在 P2 中介绍；由于 type inference 系统是 static checker 的一部分，这牵涉到 static checker 的正确性 (correctness) 问题。

幸运的是，ML 的 type inference 算法设计得非常简洁与优美；虽然存在 non-trivial 的程序能够使得 inference 效率变得非常低，但在现实应用背景下这种情况几乎不可能发生。

Overview of ML Type Inference

ML 的 type inference 大致遵循以下规则：

  • It determines the types of bindings in order, using the types of earlier binding to infer the types of later ones. This is why you cannot use later bindings in a file. (When you need to, use mutual recursion and type inference determines the types of all mutually recursive bindings together)
  • For each val and fun binding, it analyzes the binding to determine necessary facts about its type. We gather facts for function calls, pattern-matches, etc.
  • Afterward, use type variable (e.g., 'a) for any unconstrained types in function arguments or results.
  • Enforce the value restriction such that only variables and values can have polymorphic types.

ML type inference 的这种 "going in order" 的优美设计使得其不会 reject 任何一个能够 type-check 的程序，同时也不会 accept 一个不能 type-check 的程序。因此，explicit type annotations really are optional.

1
2
3
4
fun length xs =
    case xs of
        [] => 0
      | x::xs' => 1 + (length xs')

我们来看这个例子：type inferencer 开始按照顺序进行类型推断。

  • length has type T1->T2.
  • xs has type T1. (参数)
  • T1=T3 list. (根据 case...of 的 pattern matching 得出)
  • T2=int. (函数返回值可以为 0)
  • x has type T3 and xs' has type T3 list.

至此，我们已经获得了所有变量的类型。最后 type inferencer 对于所有的 unconstrained types 统一的分配 type variables：T3='a, T1=T3 list='a list. 对于函数 length 的类型推断完成：length: 'a list->int.

type variable 'a indicates itself as a polymorphic datatype (or generic type). 因此，函数 length 体现了 parametric polymorphism：它的参数类型是一个多态类型。

更多的例子，以及关于 value restriction 的相关介绍见课程提供的 section3sum.pdf。在之后，它还介绍了在 ML 中使用 signature 实现抽象的方式。但是这一部分内容并不是 functional programming 的核心 feature，在此按下不表。


Reference

  This article is a self-administered course note.

  References in the article are from corresponding course materials if not specified.

Course info:

Programming Languages, Part A, University of Washington, Lecturer: Professor Dan Grossman.


-----------------------------------そして、次の曲が始まるのです。-----------------------------------