TAPL

[at15]

Related https://github.com/at15/papers-i-read/issues/76

Read (I don't think I can write from scratch ...

• [x] 4 An ML Implementation of Arithmetic Expression 6292de6ce2447879884d48fa63bf54d1d3bbefbd
• [x] 7 An ML Implementation of the Lambda-Calculus 3e525257ffbc75163e777ed9d142309f73900356
  • [ ] tmmap, it is used in application and let binding, termSubstTop, mentioned in chap7, need to look at that in more detail
• [x] 10 An ML Implementation of Simple Types
• [ ] 17 An ML Implementation of Subtyping

OCamel

• https://realworldocaml.org/v1/en/html/index.html from TOC it is similar to TAPL

the mapping between code and chapters is in index ...

[at15]

https://www.cis.upenn.edu/~bcpierce/tapl/checkers/

[at15]

http://languagengine.co/blog/so-you-want-to-write-a-type-checker/ this is easier to understand, use javascript https://github.com/psygnisfive/so-you-want-to-write-a-type-checker

[at15]

about the interpreter in TAPL, someone said it is not very good 'Nameless Representation' https://www.zhihu.com/question/32473386/answer/55697951

类型系统（Type System）最好的入门书当属《Types and Programming Languages》了。这本书一开始从最简单的Untyped Lambda Calculus 开始先教你写解释器，但他的解释器用的是Nameless Representation，这种解释器实现方式初看简单，但你会发现当你要给语言加特性、扩展解释器的时候就必须要写一些很机械重复的代码而且还不好理解，所以我个人还是比较推荐上面一段中的实现方式。然后跟着这本书重点学习并实现Simple Typed Lambda Calculus 及其扩展类型系统。在学完Subtyping 之后如果你觉得Recursive Types 难理解的话跳过它也无妨。然后就是重头戏了：Polymorphism 和Type Inference

上面的那个解释器是王垠的，原文链接挂了 ... http://www.yinwang.org/blog-cn/2012/08/01/interpreter

nameless 在 TAPL 的第 6 章，给了 5 种，选了第三种

we chose the third, which in our experience, scales better when we come to some of the more complex implementations later in the book

王垠的文章里对函数的解释

对变量最基本的操作，是对它的“绑定”（binding）和“取值”（evaluate）。什么是绑定呢？拿上面的函数 f(x) 作为例子。当我们调用 f(1) 时，函数体里面的 x 等于 1，所以 x 2 的值是 2，而当我们调用 f(2) 时，函数体里面的 x 等于 2，所以 x 2 的值是 4。这里，两次对 f 的调用，分别对 x 进行了两次绑定。第一次 x 被绑定到了 1，第二次被绑定到了 2

处理 typing context 的方法，每次产生一个新的环境，把新的环境传进去，之前的环境还在

;; 对环境 env 进行扩展，把 x 映射到 v
(define ext-env
  (lambda (x v env)
    (cons `(,x . ,v) env)))