最近掉进另外一个 PL 的坑里面，就是想读一下这本书，顺便继续熟悉一下 Ocaml。下面的记录是阅读过程中的一些摘录和理解。

1-2 章是数学预备部分，理论部分有些地方比较难懂，主要是一些数学符号看久了眼花。
解释器的实现大多只用看 syntax.ml 和 core.ml，就是语法和具体 eval，typeof 函数。

Untyped Systems

arith 是一个无类型的解释器，是后面所有章节的基础。printtm_Term 用了 Format 模块来格式化打印。

The Untyped Lambda-Calculus

浅显易懂的 Lambda-Calculus 解释，同时列举了一些 lambda calculus 扩展其他语言部分的例子。

An ML Implementation of the Lambda-Calculus

shifting 和 substitution 的实现挺难看懂的，本质上是把 context 里面的变量用 index 来替换，处理变量查找的一种实现而已。eval 部分是非常地简洁，我觉得 ML 系的语法看起来比 Scheme 都舒服紧凑。

Just because you’ve implemented something doesn’t mean you understand it.
​ —Brian Cantwell Smith

说起来全是泪，用这种函数式的编程语言来解释自己确实比较简单，但现实往往不是这样。语言能比较容易地实现自己至少可以表明语言的内核挺小，一个语言能实现 bootstrap 是成熟的一个表现。Rust 的实现最初是用 Ocaml 写的，然后编译出一个 Rust 的编译器，然后用上一版本的 Rust 再重新实现 Rust 编译器。

Typed Arithmetic Expressions

tyarith 是最简单的带类型的解释器，有 bool 和 Nat 类型。

Progress: A well-typed term is not stuck (either it is a value or it can take a step according to the evaluation rules).
Preservation: If a well-typed term takes a step of evaluation, then the resulting term is also well typed

These properties together tell us that a well-typed term can never reach a stuck state during evaluation.

Safety = Progress + Preservation

Simply Typed Lambda-Calculus

In general, languages in which type annotations in terms are used to help guide the typechecker are called explicitly typed. Languages in which we ask the typechecker to infer or reconstruct this information are called implicitly typed.

Well-typed programs cannot “go wrong.” —Robin Milner (1978)

An ML Implementation of Simple Types

simplebool 是一个只有 bool 类型的解释器，但是加上了函数。typeof 挺简单，主要是函数这里注意处理形参和实参：

| TmAbs(fi,x,tyT1,t2) ->
    let ctx' = addbinding ctx x (VarBind(tyT1)) in
    let tyT2 = typeof ctx' t2 in
    TyArr(tyT1, tyT2)
| TmApp(fi,t1,t2) ->
    let tyT1 = typeof ctx t1 in
    let tyT2 = typeof ctx t2 in
    (match tyT1 with
        TyArr(tyT11, tyT12) ->
          if (=) tyT2 tyT11 then tyT12
          else error fi "parameter type mismatch"
      | _ -> error fi "arrow type expected")

if 的判断部分必须为 bool，而且两个分支必须为同一类型：

| TmIf(fi,t1,t2,t3) ->
   if (=) (typeof ctx t1) TyBool then
     let tyT2 = typeof ctx t2 in
     if (=) tyT2 (typeof ctx t3) then tyT2
     else error fi "arms of conditional have different types"
     else error fi "guard of conditional not a boolean"

Simple Extensions

在上一章的基础上，加上各种 Drived Form。

• Sequencing:

  是多个表达式串，这在有副作用的语言里面很常见。另外也可以把 t1;t2 理解为 (λx:Unit.t2) t1。

• Wildcards:

  如何翻译好，意思就是无用形参可以不指定名字。

• Ascription

  是指类型缩写 (或者昵名)，C++ 里面的 typedef，和 Rust 里面的 usize as U 都是。这个的好处在于文档和接口更清晰，如果函数的参数可以是函数，类型加进以后语法看起来就比较繁琐了，用类型缩写更清晰。typechecker 的时候当然需要展开来进行。ascription 和 casting 也有一定关系。

  增加各种简单的基础类型，比如 String，还有 Pairs，Tuple，Record，Sum，Enum，List。支持一种类型除了一个新类型名字外，其 evaluation rules 和 type rules 也要明确。这里的 datatypes 是按照 Ocaml 的语法来说明的。

  因为加上了好多种类型，fullsimple 这个解释器复杂多了。

Type Dynamic

Even in statically typed languages, there is often the need to deal with data whose type cannot be determined at compile time. This occurs in particular when the lifetime of the data spans multiple machines or many runs of the compiler—when, for example, the data is stored in an external file system or database, or communicated across a network. To handle such situations safely, many languages offer facilities for inspecting the types of values at run time.

General Recursion

typed lambda-calculus 加上 fix combinator 就是一门极小的但是是 full abstraction 的语言。Ocaml 里面的 letrec 可以用来定义递归函数。fix point 的概念需要继续理解。