From f8b76ae112e98dac5945a4c949fc925963579df2 Mon Sep 17 00:00:00 2001 From: niltok Date: Fri, 25 Dec 2020 23:11:45 +0800 Subject: [PATCH] fix(Lambda) Env --- doc/CoC.md | 50 +++++++++--------------- doc/STLC.md | 97 +++++++++++++++++++---------------------------- doc/SysFO.md | 43 +++++++-------------- doc/SystemF.md | 37 +++++++----------- html/CoC.html | 50 +++++++++--------------- html/STLC.html | 94 +++++++++++++++++---------------------------- html/SysFO.html | 43 +++++++-------------- html/SystemF.html | 37 +++++++----------- 8 files changed, 161 insertions(+), 290 deletions(-) diff --git a/doc/CoC.md b/doc/CoC.md index f1b01fa..ece6f56 100644 --- a/doc/CoC.md +++ b/doc/CoC.md @@ -36,21 +36,24 @@ interface Expr { Expr fullReduce(); Expr apply(Val v, Expr e); - Expr checkType() throws BadTypeException; - boolean checkApply(Val v); + Expr checkType(Env env) throws BadTypeException; } + class Sort implements Expr { int x; // 1 为 * ， 2 为 □ } + class Val implements Expr { String x; UUID id; Expr t; // 类型 } + class Fun implements Expr { Val x; Expr e; } + class App implements Expr { Expr f, x; } @@ -65,68 +68,51 @@ class Pi implements Expr { ```java class Sort implements Expr { - public Expr checkType() { + public Expr checkType(Env env) { return new Sort(x + 1); } - public boolean checkApply(Val v) { - return true; - } } class Val implements Expr { - public Expr checkType() { + public Expr checkType(Env env) throws BadTypeException { + if (t == null) return env.lookup(id); return t.fullReduce(); } - public boolean checkApply(Val v) { - if (equals(v)) - return checkType().equals(v.checkType()); - return t.checkApply(v); - } } class Fun implements Expr { - public Expr checkType() throws BadTypeException { - Expr pi = new Pi(x, e.checkType()); - if (pi.checkType() instanceof Sort) + public Expr checkType(Env env) throws BadTypeException { + Expr pi = new Pi(x, e.checkType(new ConsEnv(x, env))); + if (pi.checkType(env) instanceof Sort) return pi; throw new BadTypeException(); } - public boolean checkApply(Val v) { - return x.checkApply(v) && - e.checkApply(v); - } } class App implements Expr { - public Expr checkType() throws BadTypeException { - Expr tf = f.checkType(); + public Expr checkType(Env env) throws BadTypeException { + Expr tf = f.checkType(env); if (tf instanceof Pi) { Pi pi = (Pi) tf; - if (x.checkType().equals(pi.x.checkType())) + if (x.checkType(env).equals(pi.x.checkType(env))) return pi.e.apply(pi.x, x); } throw new BadTypeException(); } - public boolean checkApply(Val v) { - return f.checkApply(v) && x.checkApply(v); - } } class Pi implements Expr { - public Expr checkType() throws BadTypeException { - Expr ta = x.checkType().checkType(); // x.t 的类型 - Expr tb = e.checkType(); + public Expr checkType(Env env) throws BadTypeException { + Expr ta = x.checkType(env).checkType(env); // x.t 的类型 + Expr tb = e.checkType(new ConsEnv(x, env)); if (ta instanceof Sort && tb instanceof Sort) { return tb; } throw new BadTypeException(); } - public boolean checkApply(Val v) { - return x.checkApply(v) && e.checkApply(v); - } } ``` -所以实际上 `Pi` 就是一个类型检查期的标识，并不参与最终值的演算。 +所以实际上 `Pi` 就是一个类型检查期的标识，并不参与最终值的演算。因为不区分值和类型，其中 `Env` 保存的内容改为 `Val` ，并且 `lookup` 改为用 `UUID` 检索。 这样就构造出了一个相当强大的类型系统，它的表现力已经超越了几乎所有常见语言的类型系统。之后将会介绍如何利用这个强大的类型系统表达复杂的类型，做一些常见类型系统做不到的事情。 \ No newline at end of file diff --git a/doc/STLC.md b/doc/STLC.md index 55e29a6..25a9dbf 100644 --- a/doc/STLC.md +++ b/doc/STLC.md @@ -28,9 +28,6 @@ class TVal implements Type { public String toString() { return name; } - public boolean equals(Object o) { - // ... - } } // FunctionType class TArr implements Type { @@ -38,9 +35,6 @@ class TArr implements Type { public String toString() { return "(" + src + " → " + tar + ")"; } - public boolean equals(Object o) { - // ... - } } ``` @@ -63,9 +57,28 @@ class App implements Expr { } ``` -注意只有变量和函数定义的变量需要标记类型，表达式的类型是可以被简单推导出的。 +注意只有函数定义的变量需要标记类型，表达式的类型是可以被简单推导出的。同时还需要一个环境来保存定义变量的类型（其实是一个不可变链表）： -而对于这样简单的模型，类型检查只需要判断 `F X` 中的 `F` 需要是函数类型，并且 `λ x. E` 中 `E` 里所有的 `x` 类型匹配，并且 `(λ x. F) E` 中 `x` 的类型和 `E` 的类型一致。 +```java +interface Env { + Type lookup(String s) throws BadTypeException; +} +class NilEnv implements Env { + public Type lookup(String s) throws BadTypeException { + throw new BadTypeException(); + } +} +class ConsEnv implements Env { + Val v; + Env next; + public Type lookup(String s) throws BadTypeException { + if (s.equals(v.x)) return v.type; + return next.lookup(s); + } +} +``` + +而对于这样简单的模型，类型检查只需要判断 `F X` 中的 `F` 需要是函数类型，并且 `(λ x. F) E` 中 `x` 的类型和 `E` 的类型一致。 而类型推导也很简单：变量的类型就是它被标记的类型；函数定义的类型就是以它变量的标记类型为源，它函数体的类型为目标的函数类型；而函数应用的类型就是函数的目标类型，在能通过类型检查的情况下。 @@ -74,79 +87,45 @@ class App implements Expr { ```java // 构造函数， toString 已省去 interface Expr { - Type checkType() - throws BadTypeException; - - boolean checkApply(Val val); + Type checkType(Env env) throws BadTypeException; } - class Val implements Expr { - public Type checkType() { - return type; - } - - public boolean checkApply(Val val) { - if (x.equals(val.x)) - return type.equals(val.type); - else return true; + public Type checkType(Env env) throws BadTypeException { + if (type != null) return type; + return env.lookup(x); } } - class Fun implements Expr { - public Type checkType() - throws BadTypeException { - if (e.checkApply(x)) - return new TArr(x.type, - e.checkType()); - else throw new BadTypeException(); - } - - public boolean checkApply(Val val) { - if (x.x.equals(val.x)) return true; - return e.checkApply(val); + public Type checkType(Env env) throws BadTypeException { + return new TArr(x.type, e.checkType(new ConsEnv(x, env))); } } - class App implements Expr { - public Type checkType() - throws BadTypeException { - Type tf = f.checkType(); - + public Type checkType(Env env) throws BadTypeException { + Type tf = f.checkType(env); if (tf instanceof TArr && - ((TArr) tf).src - .equals(x.checkType())) + ((TArr) tf).src.equals(x.checkType(env))) return ((TArr) tf).tar; else throw new BadTypeException(); } - - public boolean checkApply(Val val) { - return f.checkApply(val) - && x.checkApply(val); - } } ``` 下面的测试代码对 ```` -(λ (x: int). (y: bool → int)) (1: int) +(λ (x: int). (λ (y: int → bool). (y x))) ```` -进行了类型检查，会打印输出 `(bool → int)` ： +进行了类型检查，会打印输出 `(int → ((int → bool) → bool))` ： ```java public interface STLambda { - static void main(String[] args) - throws BadTypeException { - System.out.println(new App( - new Fun( - new Val("x", - new TVal("int")), - new Val("y", new TArr( - new TVal("bool"), - new TVal("int")))), - new Val("1", new TVal("int")) - ).checkType()); + static void main(String[] args) throws BadTypeException { + System.out.println( + new Fun(new Val("x", new TVal("int")), + new Fun(new Val("y", new TArr(new TVal("int"), new TVal("bool"))), + new App(new Val("y"), new Val("x")))).checkType(new NilEnv())); } } ``` @@ -154,7 +133,7 @@ public interface STLambda { 而如果对 ``` -(λ (x: int). (x: bool → int)) (1: int) +(λ (x: bool). (λ (y: int → bool). (y x))) ``` 进行类型检查就会抛出 `BadTypeException` 。 \ No newline at end of file diff --git a/doc/SysFO.md b/doc/SysFO.md index b1c6bb1..3b854ca 100644 --- a/doc/SysFO.md +++ b/doc/SysFO.md @@ -22,7 +22,6 @@ interface Type { Type fullReduce(); Type apply(TVal v, Type t); Type genUUID(); - Type applyUUID(TVal v); } class TVal implements Type { String x; @@ -42,16 +41,13 @@ class TForall implements Type { class TArr implements Type { Type a, b; public Type reduce() { - return new TArr(a.reduce(), - b.reduce()); + return new TArr(a.reduce(), b.reduce()); } public Type fullReduce() { - return new TArr(a.fullReduce(), - b.fullReduce()); + return new TArr(a.fullReduce(), b.fullReduce()); } public Type apply(TVal v, Type t) { - return new TArr(a.apply(v, t), - b.apply(v, t)); + return new TArr(a.apply(v, t), b.apply(v, t)); } } ``` @@ -62,33 +58,23 @@ class TArr implements Type { ```java interface Expr { - Type checkType() throws BadTypeException; - boolean checkApply(Val v); + Type checkType(Env env) throws BadTypeException; Expr genUUID(); Expr applyUUID(TVal v); } class Val implements Expr { String x; Type t; - public Type checkType() { + public Type checkType(Env env) { + if (t == null) return env.lookup(x); return t.fullReduce(); } - public boolean checkApply(Val v) { - if (x.equals(v.x)) - return t.fullReduce() - .equals(v.t.fullReduce()); - return true; - } } class Fun implements Expr { Val x; Expr e; - public Type checkType() - throws BadTypeException { - if (e.checkApply(x)) - return new TArr(x.checkType(), - e.checkType()); - throw new BadTypeException(); + public Type checkType(Env env) throws BadTypeException { + return new TArr(x.checkType(env), e.checkType(env)); } } class App implements Expr { @@ -115,20 +101,17 @@ public interface TypeCons { // nil = Λ X. (Λ R. λ c: X → (R → R). λ n: R. n) Expr nil = new Forall("X", new Forall("R", new Fun( new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))), - new Fun(new Val("n" , new TVal("R")), new Val("n", new TVal("R")))))).genUUID(); + new Fun(new Val("n" , new TVal("R")), new Val("n"))))).genUUID(); // cons = Λ X. λ h: X. λ t: List X. (Λ R. λ c: X → R → R. λ n: R. c h (t R c n)) Expr cons = new Forall("X", new Fun(new Val("h", new TVal("X")), new Fun( new Val("t", new TApp(List, new TVal("X"))), new Forall("R", new Fun( new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))), new Fun(new Val("n", new TVal("R")), new App( - new App(new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))), - new Val("h", new TVal("X"))), - new App(new App(new AppT(new Val("t", new TApp(List, new TVal("X"))), new TVal("R")), - new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R"))))), - new Val("n", new TVal("R")))))))))).genUUID(); - static void main(String[] args) - throws BadTypeException { + new App(new Val("c"), new Val("h")), + new App(new App(new AppT(new Val("t"), new TVal("R")), + new Val("c")), new Val("n"))))))))).genUUID(); + static void main(String[] args) throws BadTypeException { // (∀ X. (∀ R. ((X → (R → R)) → (R → R)))) System.out.println(nil.checkType()); // (∀ X. (X → ((∀ R. ((X → (R → R)) → (R → R))) → (∀ R. ((X → (R → R)) → (R → R)))))) diff --git a/doc/SystemF.md b/doc/SystemF.md index 371b2d1..be0d2ba 100644 --- a/doc/SystemF.md +++ b/doc/SystemF.md @@ -129,8 +129,7 @@ class TArr implements Type { ```java interface Expr { - Type checkType() throws BadTypeException; - boolean checkApply(Val v); + Type checkType(Env env) throws BadTypeException; Expr genUUID(); Expr applyUUID(TVal v); } @@ -141,16 +140,12 @@ class App implements Expr { /* ... */ } class Forall implements Expr { TVal x; Expr e; - public Type checkType() - throws BadTypeException { - return new TForall(x, e.checkType()); - } - public boolean checkApply(Val v) { - return e.checkApply(v); + public Type checkType() throws BadTypeException { + return new TForall(x, e.checkType(env)); } public Expr genUUID() { if (x.id == null) { - TVal v = new TVal(x.x, UUID.randomUUID); + TVal v = new TVal(x.x, UUID.randomUUID()); return new Forall(v, e.applyUUID(v).genUUID()); } return new Forall(x, e.genUUID()); @@ -164,17 +159,12 @@ class Forall implements Expr { class AppT implements Expr { Expr e; Type t; - public Type checkType() - throws BadTypeException { - Type te = e.checkType(); + public Type checkType(Env env) throws BadTypeException { + Type te = e.checkType(env); if (te instanceof TForall) // 填入类型参数 - return ((TForall) te).e - .apply(((TForall) te).x, t); + return ((TForall) te).e.apply(((TForall) te).x, t); throw new BadTypeException(); } - public boolean checkApply(Val v) { - return e.checkApply(v); - } public Expr genUUID() { return new AppT(e.genUUID(), t.genUUID()); } @@ -193,11 +183,11 @@ public interface SystemF { Expr T = new Forall("a", new Fun( new Val("x", new TVal("a")), new Fun(new Val("y", new TVal("a")), - new Val("x", new TVal("a"))))).genUUID(); + new Val("x")))).genUUID(); Expr F = new Forall("a", new Fun( new Val("x", new TVal("a")), new Fun(new Val("y", new TVal("a")), - new Val("y", new TVal("a"))))).genUUID(); + new Val("y")))).genUUID(); Type Bool = new TForall("x", new TArr( new TVal("x"), new TArr(new TVal("x"), new TVal("x")))).genUUID(); @@ -206,12 +196,11 @@ public interface SystemF { new Fun(new Val("x", new TVal("a")), new Fun( new Val("y", new TVal("a")), new App(new App( - new AppT(new Val("b", Bool), new TVal("a")), - new Val("x", new TVal("a"))), - new Val("y", new TVal("a"))))))).genUUID(); + new AppT(new Val("b"), new TVal("a")), + new Val("x")), new Val("y")))))).genUUID(); static void main(String[] args) throws BadTypeException { - System.out.println(T.checkType()); - System.out.println(IF.checkType()); + System.out.println(T.checkType(new NilEnv())); + System.out.println(IF.checkType(new NilEnv())); } } ``` diff --git a/html/CoC.html b/html/CoC.html index 1d541f3..b6631a8 100644 --- a/html/CoC.html +++ b/html/CoC.html @@ -50,21 +50,24 @@

构造演算

Expr fullReduce(); Expr apply(Val v, Expr e); - Expr checkType() throws BadTypeException; - boolean checkApply(Val v); + Expr checkType(Env env) throws BadTypeException; } + class Sort implements Expr { int x; // 1 为 * ， 2 为 □ } + class Val implements Expr { String x; UUID id; Expr t; // 类型 } + class Fun implements Expr { Val x; Expr e; } + class App implements Expr { Expr f, x; } @@ -75,67 +78,50 @@

构造演算

}

其中 Expr 的接口的函数被分成了三组，第一组是预生成 id 只需要简单递归生成就可以，之前也展示过；第二组是对表达式的化简，只需注意 App 在化简时只应用 Fun 应该忽略 Pi ，并且递归化简时别忘了变量部分的类型也是一个表达式；第三组就是类型检查部分了， Fun 的类型是 Pi ， Pi 的类型是 e 的类型， App 把表达式应用到 Pi 上：

class Sort implements Expr {
-    public Expr checkType() {
+    public Expr checkType(Env env) {
         return new Sort(x + 1);
     }
-    public boolean checkApply(Val v) {
-        return true;
-    }
 }
 
 class Val implements Expr {
-    public Expr checkType() {
+    public Expr checkType(Env env) throws BadTypeException {
+        if (t == null) return env.lookup(id);
         return t.fullReduce();
     }
-    public boolean checkApply(Val v) {
-        if (equals(v))
-            return checkType().equals(v.checkType());
-        return t.checkApply(v);
-    }
 }
 
 class Fun implements Expr {
-    public Expr checkType() throws BadTypeException {
-        Expr pi = new Pi(x, e.checkType());
-        if (pi.checkType() instanceof Sort)
+    public Expr checkType(Env env) throws BadTypeException {
+        Expr pi = new Pi(x, e.checkType(new ConsEnv(x, env)));
+        if (pi.checkType(env) instanceof Sort)
             return pi;
         throw new BadTypeException();
     }
-    public boolean checkApply(Val v) {
-        return x.checkApply(v) &&
-                e.checkApply(v);
-    }
 }
 
 class App implements Expr {
-    public Expr checkType() throws BadTypeException {
-        Expr tf = f.checkType();
+    public Expr checkType(Env env) throws BadTypeException {
+        Expr tf = f.checkType(env);
         if (tf instanceof Pi) {
             Pi pi = (Pi) tf;
-            if (x.checkType().equals(pi.x.checkType()))
+            if (x.checkType(env).equals(pi.x.checkType(env)))
                 return pi.e.apply(pi.x, x);
         }
         throw new BadTypeException();
     }
-    public boolean checkApply(Val v) {
-        return f.checkApply(v) && x.checkApply(v);
-    }
 }
 
 class Pi implements Expr {
-    public Expr checkType() throws BadTypeException {
-        Expr ta = x.checkType().checkType(); // x.t 的类型
-        Expr tb = e.checkType();
+    public Expr checkType(Env env) throws BadTypeException {
+        Expr ta = x.checkType(env).checkType(env); // x.t 的类型
+        Expr tb = e.checkType(new ConsEnv(x, env));
         if (ta instanceof Sort && tb instanceof Sort) {
             return tb;
         }
         throw new BadTypeException();
     }
-    public boolean checkApply(Val v) {
-        return x.checkApply(v) && e.checkApply(v);
-    }
 }
-

所以实际上 Pi 就是一个类型检查期的标识，并不参与最终值的演算。

+

所以实际上 Pi 就是一个类型检查期的标识，并不参与最终值的演算。因为不区分值和类型，其中 Env 保存的内容改为 Val ，并且 lookup 改为用 UUID 检索。

这样就构造出了一个相当强大的类型系统，它的表现力已经超越了几乎所有常见语言的类型系统。之后将会介绍如何利用这个强大的类型系统表达复杂的类型，做一些常见类型系统做不到的事情。

diff --git a/html/STLC.html b/html/STLC.html index e5a9bc9..e7f7298 100644 --- a/html/STLC.html +++ b/html/STLC.html @@ -44,9 +44,6 @@

简单类型 λ 演算

public String toString() { return name; } - public boolean equals(Object o) { - // ... - } } // FunctionType class TArr implements Type { @@ -54,9 +51,6 @@

简单类型 λ 演算

public String toString() { return "(" + src + " → " + tar + ")"; } - public boolean equals(Object o) { - // ... - } }

年轻人的第一个 TypeChecker

然后需把类型嵌入到 λ 演算的语法树中：

@@ -72,81 +66,63 @@

年轻人的第一个 TypeChecker

class App implements Expr { Expr f, x; } -

注意只有变量和函数定义的变量需要标记类型，表达式的类型是可以被简单推导出的。

-

而对于这样简单的模型，类型检查只需要判断 F X 中的 F 需要是函数类型，并且 λ x. E 中 E 里所有的 x 类型匹配，并且 (λ x. F) E 中 x 的类型和 E 的类型一致。

+

注意只有函数定义的变量需要标记类型，表达式的类型是可以被简单推导出的。同时还需要一个环境来保存定义变量的类型（其实是一个不可变链表）：

+
interface Env {
+    Type lookup(String s) throws BadTypeException;
+}
+class NilEnv implements Env {
+    public Type lookup(String s) throws BadTypeException {
+        throw new BadTypeException();
+    }
+}
+class ConsEnv implements Env {
+    Val v;
+    Env next;
+    public Type lookup(String s) throws BadTypeException {
+        if (s.equals(v.x)) return v.type;
+        return next.lookup(s);
+    }
+}
+

而对于这样简单的模型，类型检查只需要判断 F X 中的 F 需要是函数类型，并且 (λ x. F) E 中 x 的类型和 E 的类型一致。

而类型推导也很简单：变量的类型就是它被标记的类型；函数定义的类型就是以它变量的标记类型为源，它函数体的类型为目标的函数类型；而函数应用的类型就是函数的目标类型，在能通过类型检查的情况下。

以上用 Java 代码描述就是：

// 构造函数， toString 已省去
 interface Expr {
-    Type checkType() 
-        throws BadTypeException;
-
-    boolean checkApply(Val val);
+    Type checkType(Env env) throws BadTypeException;
 }
-
 class Val implements Expr {
-    public Type checkType() {
-        return type;
-    }
-
-    public boolean checkApply(Val val) {
-        if (x.equals(val.x))
-            return type.equals(val.type);
-        else return true;
+    public Type checkType(Env env) throws BadTypeException {
+        if (type != null) return type;
+        return env.lookup(x);
     }
 }
-
 class Fun implements Expr {
-    public Type checkType() 
-            throws BadTypeException {
-        if (e.checkApply(x))
-            return new TArr(x.type, 
-                            e.checkType());
-        else throw new BadTypeException();
-    }
-
-    public boolean checkApply(Val val) {
-        if (x.x.equals(val.x)) return true;
-        return e.checkApply(val);
+    public Type checkType(Env env) throws BadTypeException {
+        return new TArr(x.type, e.checkType(new ConsEnv(x, env)));
     }
 }
-
 class App implements Expr {
-    public Type checkType() 
-            throws BadTypeException {
-        Type tf = f.checkType();
-
+    public Type checkType(Env env) throws BadTypeException {
+        Type tf = f.checkType(env);
         if (tf instanceof TArr &&
-                ((TArr) tf).src
-                .equals(x.checkType()))
+                ((TArr) tf).src.equals(x.checkType(env)))
             return ((TArr) tf).tar;
         else throw new BadTypeException();
     }
-
-    public boolean checkApply(Val val) {
-        return f.checkApply(val) 
-            && x.checkApply(val);
-    }
 }

下面的测试代码对

-
(λ (x: int). (y: bool → int)) (1: int)
-

进行了类型检查，会打印输出 (bool → int) ：

+
(λ (x: int). (λ (y: int → bool). (y x)))
+

进行了类型检查，会打印输出 (int → ((int → bool) → bool)) ：

public interface STLambda {
-    static void main(String[] args) 
-    throws BadTypeException {
-        System.out.println(new App(
-            new Fun(
-                new Val("x", 
-                    new TVal("int")),
-                new Val("y", new TArr(
-                    new TVal("bool"),
-                    new TVal("int")))),
-            new Val("1", new TVal("int"))
-        ).checkType());
+    static void main(String[] args) throws BadTypeException {
+        System.out.println(
+            new Fun(new Val("x", new TVal("int")),
+            new Fun(new Val("y", new TArr(new TVal("int"), new TVal("bool"))),
+                new App(new Val("y"), new Val("x")))).checkType(new NilEnv()));
     }
 }

而如果对

-
(λ (x: int). (x: bool → int)) (1: int)
+
(λ (x: bool). (λ (y: int → bool). (y x)))

进行类型检查就会抛出 BadTypeException 。

diff --git a/html/SysFO.html b/html/SysFO.html index b893f8e..f755d7f 100644 --- a/html/SysFO.html +++ b/html/SysFO.html @@ -40,7 +40,6 @@

By 「玩火」

Type fullReduce(); Type apply(TVal v, Type t); Type genUUID(); - Type applyUUID(TVal v); } class TVal implements Type { String x; @@ -60,48 +59,35 @@

By 「玩火」

class TArr implements Type { Type a, b; public Type reduce() { - return new TArr(a.reduce(), - b.reduce()); + return new TArr(a.reduce(), b.reduce()); } public Type fullReduce() { - return new TArr(a.fullReduce(), - b.fullReduce()); + return new TArr(a.fullReduce(), b.fullReduce()); } public Type apply(TVal v, Type t) { - return new TArr(a.apply(v, t), - b.apply(v, t)); + return new TArr(a.apply(v, t), b.apply(v, t)); } }

其中 TVal 、 TFun 和 TApp 的函数实现和无类型 λ 演算中的表达式基本一致，不过注意要加上 equals 函数的实现，并且 TFun 在比较前需要把变量替换成一样的， fullReduce 函数在 Y 组合子那期中给出了实现，这里就不贴出展示了。而 TForall 的实现可以参考 System F ， TArr 的实现也只是简单进行递归调用，非常简单。

而表达式相比系统 F 需要的改动是 TVal 在检查类型时需要先调用 fullReduce 来化简类型：

interface Expr {
-    Type checkType() throws BadTypeException;
-    boolean checkApply(Val v);
+    Type checkType(Env env) throws BadTypeException;
     Expr genUUID();
     Expr applyUUID(TVal v);
 }
 class Val implements Expr {
     String x;
     Type t;
-    public Type checkType() {
+    public Type checkType(Env env) {
+        if (t == null) return env.lookup(x);
         return t.fullReduce();
     }
-    public boolean checkApply(Val v) {
-        if (x.equals(v.x))
-            return t.fullReduce()
-                   .equals(v.t.fullReduce());
-        return true;
-    }
 }
 class Fun implements Expr {
     Val x;
     Expr e;
-    public Type checkType() 
-            throws BadTypeException {
-        if (e.checkApply(x)) 
-            return new TArr(x.checkType(), 
-                            e.checkType());
-        throw new BadTypeException();
+    public Type checkType(Env env) throws BadTypeException {
+        return new TArr(x.checkType(env), e.checkType(env));
     }
 }
 class App implements Expr {
@@ -124,20 +110,17 @@ 
By 「玩火」

     // nil  = Λ X. (Λ R. λ c: X → (R → R). λ n: R. n)
     Expr nil = new Forall("X", new Forall("R", new Fun(
         new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))),
-        new Fun(new Val("n" , new TVal("R")), new Val("n", new TVal("R")))))).genUUID();
+        new Fun(new Val("n" , new TVal("R")), new Val("n"))))).genUUID();
     // cons = Λ X. λ h: X. λ t: List X. (Λ R. λ c: X → R → R. λ n: R. c h (t R c n))
     Expr cons = new Forall("X", new Fun(new Val("h", new TVal("X")), new Fun(
         new Val("t", new TApp(List, new TVal("X"))),
         new Forall("R", new Fun(
             new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))),
             new Fun(new Val("n", new TVal("R")), new App(
-                new App(new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R")))),
-                    new Val("h", new TVal("X"))),
-                new App(new App(new AppT(new Val("t", new TApp(List, new TVal("X"))), new TVal("R")),
-                    new Val("c", new TArr(new TVal("X"), new TArr(new TVal("R"), new TVal("R"))))),
-                    new Val("n", new TVal("R")))))))))).genUUID();
-    static void main(String[] args) 
-            throws BadTypeException {
+                new App(new Val("c"), new Val("h")),
+                new App(new App(new AppT(new Val("t"), new TVal("R")),
+                    new Val("c")), new Val("n"))))))))).genUUID();
+    static void main(String[] args) throws BadTypeException {
         // (∀ X. (∀ R. ((X → (R → R)) → (R → R))))
         System.out.println(nil.checkType());
         // (∀ X. (X → ((∀ R. ((X → (R → R)) → (R → R))) → (∀ R. ((X → (R → R)) → (R → R))))))
diff --git a/html/SystemF.html b/html/SystemF.html
index fda5e75..5946673 100644
--- a/html/SystemF.html
+++ b/html/SystemF.html
@@ -122,8 +122,7 @@ 
By 「玩火」

 
这里的实现和无类型 λ 演算很像。不过要注意 TForall 的 equals 函数实现，在比较前需要先把变量统一一下。

 
再在简单类型 λ 演算的基础上给表达式加上类型函数定义和类型函数应用，同时还需要协助类型系统生成类型的 UUID ：

 
interface Expr {
-    Type checkType() throws BadTypeException;
-    boolean checkApply(Val v);
+    Type checkType(Env env) throws BadTypeException;
     Expr genUUID();
     Expr applyUUID(TVal v);
 }
@@ -134,16 +133,12 @@ 
By 「玩火」

 class Forall implements Expr {
     TVal x;
     Expr e;
-    public Type checkType() 
-            throws BadTypeException {
-        return new TForall(x, e.checkType());
-    }
-    public boolean checkApply(Val v) {
-        return e.checkApply(v);
+    public Type checkType() throws BadTypeException {
+        return new TForall(x, e.checkType(env));
     }
     public Expr genUUID() {
         if (x.id == null) {
-            TVal v = new TVal(x.x, UUID.randomUUID);
+            TVal v = new TVal(x.x, UUID.randomUUID());
             return new Forall(v, e.applyUUID(v).genUUID());
         }
         return new Forall(x, e.genUUID());
@@ -157,17 +152,12 @@ 
By 「玩火」

 class AppT implements Expr {
     Expr e;
     Type t;
-    public Type checkType() 
-            throws BadTypeException {
-        Type te = e.checkType();
+    public Type checkType(Env env) throws BadTypeException {
+        Type te = e.checkType(env);
         if (te instanceof TForall) // 填入类型参数
-            return ((TForall) te).e
-                   .apply(((TForall) te).x, t);
+            return ((TForall) te).e.apply(((TForall) te).x, t);
         throw new BadTypeException();
     }
-    public boolean checkApply(Val v) {
-        return e.checkApply(v);
-    }
     public Expr genUUID() {
         return new AppT(e.genUUID(), t.genUUID());
     }
@@ -181,11 +171,11 @@ 
By 「玩火」

     Expr T = new Forall("a", new Fun(
         new Val("x", new TVal("a")),
         new Fun(new Val("y", new TVal("a")),
-            new Val("x", new TVal("a"))))).genUUID();
+            new Val("x")))).genUUID();
     Expr F = new Forall("a", new Fun(
         new Val("x", new TVal("a")),
         new Fun(new Val("y", new TVal("a")),
-            new Val("y", new TVal("a"))))).genUUID();
+            new Val("y")))).genUUID();
     Type Bool = new TForall("x", new TArr(
         new TVal("x"),
         new TArr(new TVal("x"), new TVal("x")))).genUUID();
@@ -194,12 +184,11 @@ 
By 「玩火」

         new Fun(new Val("x", new TVal("a")), new Fun(
             new Val("y", new TVal("a")),
             new App(new App(
-                new AppT(new Val("b", Bool), new TVal("a")),
-                new Val("x", new TVal("a"))),
-                new Val("y", new TVal("a"))))))).genUUID();
+                new AppT(new Val("b"), new TVal("a")),
+                new Val("x")), new Val("y")))))).genUUID();
     static void main(String[] args) throws BadTypeException {
-        System.out.println(T.checkType());
-        System.out.println(IF.checkType());
+        System.out.println(T.checkType(new NilEnv()));
+        System.out.println(IF.checkType(new NilEnv()));
     }
 }

 
运行会输出：