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?
网友评论