Type Checking 做题非常容易错

拿到一个Expression的时候第一步先把整个expression写出来，然后决定按什么顺序Type-Check。

上述let x: Str<-"a" 是第一个要被type check的 Also 每一次assign的时候都要check一下assign value是不是subtype of declare type .所以在接下来type check inner expression的时候， 假设let x: Str<-"a" 已经check好了。因此Environment里会有一个binding。O[str/x].

接下来要check什么？很明显是那个超级长的一串。这里需要化简一下，original expression可以看做

let x: str<-"a" in e: Int     整个东西的返回值是Int

所以很明显 我们要check e, e 就是那个很长的一串。

e = e1 + e2 所以 接下来我们要type check e1, 和 e2.

e1 是 let x: int <- 1 in e   e2是let y: Str<-"a" in e

这里有一点Tricky，我们之前x不是binding过了吗？由于closest enclosing principle，内层scope里的x会被替换成新的值。我们必须同时记住外层和内存的bindings，所以写作:O[string/x][Int/x]

还有一个比较tricky的是if, while 那些condition的表示。

比如if x = y  我们type check 写： x = y: bool

最后一个就是Type checking的最上层：

O2(x) = Int 就是apply environment function O2 on x, O2因为是O[str/x][int/x] 所以取内层得Int。

所以可见整个Type Check就是不断check sub expression.

在这题里我们只用了O environment，因为里面没有调用dispatch method. 如果涉及function，我们需要用M as well.

Type-derivation第二题：

从这题稍微看出来一点，Top level: O[type/x][x]=type 表示这个scope里的x的值。

还有一个Tricky的地方： O[str/x], M |- x: str  Str<=Ob 这里是declared Type为object的x被assign了一个Str的值。分析一下static type和dynamic type. static=obj, dynamic = string. 我比较不理解为什么最右边是O[str/x][ob/x]呢？因为目前看起来x不是一个String吗？ 但是如果这样还怎么用dispatch? ：好像是因为这里是一个继承关系所以method继承来了。 但是真的要格外小心。。。最内存在调用type_name()的时候似乎被认为是一个object Type? O[str/x][Ob/x] = ob

原因是因为Type-check只check static Type, dynamic type是run time check的。所以最里面那层根据declare type来处理。

第三题Tricky:

我们要知道什么时候需要O[T/x]什么时候不需要。这个例子里第一个O[T/x]之所以不能出现在那里是因为

evaluate e1的时候也许需要用到outside let scope 里x 的值， e1是先计算好再assign给x的！

Summary:

Type check之前要先把e 给完整写出来，然后再type check

let x<-e  , assign的时候 下一步先eval(e), 然后O[type/x]

Dispatch typecheck

这里比较Tricky的几个点：

1. new A: A  A<= A 这一步很容易忘记做，即便这个Type =自己，还是要check。 

2. dispatch check的办法：

1. 看看M里存不存在该function   M(class, method) = (formal arg Type, ..., formal arg type, return type) 

到这里function就算check好了

2. check一下参数： O, M |- 10: Int Int<=Int

最后还是要O[A/a](a) = A 似乎意思就是正式assign a = class A?