fix(CoC SysFO)

doc/CoC.md

@@ -6,9 +6,11 @@
 
 ## λ 立方
 
-表达式非类型部分叫做项（Term），类型部分叫做类型（Type），其中项的类型为类型也写作 `*` 而类型的类型也就是种类（Kind）写作 `□`。简单类型 λ 演算中项和类型是分离的，其中只有针对项的函数，它接收一个项返回另一个项，其类型是 `* → *` 。系统 F 对类型系统进行了扩充，在项中增加了一种函数，接收一个类型返回一个项，其类型是 `□ → *` 。而系统 F ω 进一步增加了接收类型返回类型的函数，也就是 `□ → □` 。那么可以想象应该还存在一类函数接收一个值产生一个类型，其类型应该是 `* → □` 。
+表达式非类型部分叫做项（Term），类型部分叫做类型（Type），其中类型的类型为种类（Kind）也写作 `*` 而种类的类型写作 `□`。表达式中的函数结构为 `λ x: A. (M: B)` ，如果记 `A` 的类型为 `S1` ， `B` 的类型为 `S2` ，那么可以得到一个对子 `(S1, S2)` 。
 
-对于所有 λ 演算都存在 `* → *` 的函数，而另外三种不同函数是三种额外的特性，可以自由组合来构造新的类型系统，一共能组合出六种不同的类型系统：
+简单类型 λ 演算中项和类型是分离的，其中只有针对项的函数，它接收一个项返回另一个项，其得到的对子是 `(*, *)` 。系统 F 对类型系统进行了扩充，在项中增加了一种函数，接收一个类型返回一个项，其得到的对子是 `(□, *)` 。而系统 F ω 进一步增加了接收类型返回类型的函数，也就是 `(□, □)` 。那么可以想象应该还存在一类函数接收一个值产生一个类型，其得到的对子应该是 `(*, □)` 。
+
+对于所有 λ 演算都存在 `(*, *)` 的函数，而另外三种不同函数是三种额外的特性，可以自由组合来构造新的类型系统，一共能组合出六种不同的类型系统：
 
 ```
     ω ------ C
@@ -19,13 +21,13 @@
 → ------ P
 ```
 
-左下角的 λ→ 就是简单类型 λ 演算，和它相连的三条边对应在其基础上分别添加了三种不同函数的 λ 演算。 λ2 就是系统 F ，包含 `□ → *` 函数。 λ<u>ω</u> 就是去除了系统 F 对应特性的系统 F ω ，也叫系统 F <u>ω</u> 。右下的 λP 就是在简单类型 λ 中加入了 `* → □` 的 λ 演算，而这样的类型系统中类型依赖值所以也叫依赖类型系统（Dependent Type System），在 C++ 中模板可以有值参数所以实际上 C++ 的类型系统中包括依赖类型（Dependent Type）。
+左下角的 λ→ 就是简单类型 λ 演算，和它相连的三条边对应在其基础上分别添加了三种不同函数的 λ 演算。 λ2 就是系统 F ，包含 `(□, *)` 函数。 λ<u>ω</u> 就是去除了系统 F 对应特性的系统 F ω ，也叫系统 F <u>ω</u> 。右下的 λP 就是在简单类型 λ 中加入了 `(*, □)` 的 λ 演算，而这样的类型系统中类型依赖值所以也叫依赖类型系统（Dependent Type System），在 C++ 中模板可以有值参数所以实际上 C++ 的类型系统中包括依赖类型（Dependent Type）。
 
 这个立方体就被称为 λ 立方（Lambda Cube）。
 
 ## 构造演算
 
-在 λ 立方的顶端放着 λC ，也叫构造演算（Calculus of Construction, CoC），它的类型系统被称为纯类型系统（Pure Type System, PTS）。在构造演算中类型可以作为函数的输入，也可以作为函数的输出，那么实际上我们可以把项和函数作为相同的东西，不再加以区分。这样四种不同的函数也可以不加以区分放在一起，同时加入类别（Sort）来表达类型和类型的类型。而且因为 `A → B` 等价于 `∀ _: A. B` ，那么系统 F ω 中的 `TForall` 和 `TArr` 也可以合并。这样 CoC 的语法树表示如下：
+在 λ 立方的顶端放着 λC ，也叫构造演算（Calculus of Construction, CoC）。在构造演算中类型可以作为函数的输入，也可以作为函数的输出，那么实际上我们可以把项和函数作为相同的东西，不再加以区分。这样四种不同的函数也可以不加以区分放在一起，同时加入类别（Sort）来表达类型和类型的类型。而且因为 `A → B` 等价于 `∀ _: A. B` ，那么系统 F ω 中的 `TForall` 和 `TArr` 也可以合并。这样 CoC 的语法树表示如下：
 
 ```java
 interface Expr {
@@ -76,7 +78,7 @@ class Sort implements Expr {
 class Val implements Expr {
     public Expr checkType(Env env) throws BadTypeException {
         if (t == null) return env.lookup(id);
-        return t.fullReduce();
+        return t;
     }
 }
 
@@ -94,7 +96,8 @@ class App implements Expr {
         Expr tf = f.checkType(env);
         if (tf instanceof Pi) {
             Pi pi = (Pi) tf;
-            if (x.checkType(env).equals(pi.x.checkType(env)))
+            if (x.checkType(env).fullReduce().equals(
+                	pi.x.checkType(env).fullReduce()))
                 return pi.e.apply(pi.x, x);
         }
         throw new BadTypeException();

doc/SysFO.md

@@ -67,7 +67,7 @@ class Val implements Expr {
     Type t;
     public Type checkType(Env env) {
         if (t == null) return env.lookup(x);
-        return t.fullReduce();
+        return t;
     }
 }
 class Fun implements Expr {

html/CoC.html

@@ -30,18 +30,19 @@ <h3 id="by-「玩火」">By 「玩火」</h3>
 <p>前置技能：Java 基础，ADT，系统 F ω</p>
 </blockquote>
 <h2 id="λ-立方">λ 立方</h2>
-<p>表达式非类型部分叫做项（Term），类型部分叫做类型（Type），其中项的类型为类型也写作 <code>*</code> 而类型的类型也就是种类（Kind）写作 <code>□</code>。简单类型 λ 演算中项和类型是分离的，其中只有针对项的函数，它接收一个项返回另一个项，其类型是 <code>* → *</code> 。系统 F 对类型系统进行了扩充，在项中增加了一种函数，接收一个类型返回一个项，其类型是 <code>□ → *</code> 。而系统 F ω 进一步增加了接收类型返回类型的函数，也就是 <code>□ → □</code> 。那么可以想象应该还存在一类函数接收一个值产生一个类型，其类型应该是 <code>* → □</code> 。</p>
-<p>对于所有 λ 演算都存在 <code>* → *</code> 的函数，而另外三种不同函数是三种额外的特性，可以自由组合来构造新的类型系统，一共能组合出六种不同的类型系统：</p>
+<p>表达式非类型部分叫做项（Term），类型部分叫做类型（Type），其中类型的类型为种类（Kind）也写作 <code>*</code> 而种类的类型写作 <code>□</code>。表达式中的函数结构为 <code>λ x: A. (M: B)</code> ，如果记 <code>A</code> 的类型为 <code>S1</code> ， <code>B</code> 的类型为 <code>S2</code> ，那么可以得到一个对子 <code>(S1, S2)</code> 。</p>
+<p>简单类型 λ 演算中项和类型是分离的，其中只有针对项的函数，它接收一个项返回另一个项，其得到的对子是 <code>(*, *)</code> 。系统 F 对类型系统进行了扩充，在项中增加了一种函数，接收一个类型返回一个项，其得到的对子是 <code>(□, *)</code> 。而系统 F ω 进一步增加了接收类型返回类型的函数，也就是 <code>(□, □)</code> 。那么可以想象应该还存在一类函数接收一个值产生一个类型，其得到的对子应该是 <code>(*, □)</code> 。</p>
+<p>对于所有 λ 演算都存在 <code>(*, *)</code> 的函数，而另外三种不同函数是三种额外的特性，可以自由组合来构造新的类型系统，一共能组合出六种不同的类型系统：</p>
 <pre><code>    ω ------ C
   / |      / |
 2 ------ P2  |
 |   _ω --|- _Pω
 | /      | /
 → ------ P</code></pre>
-<p>左下角的 λ→ 就是简单类型 λ 演算，和它相连的三条边对应在其基础上分别添加了三种不同函数的 λ 演算。 λ2 就是系统 F ，包含 <code>□ → *</code> 函数。 λ<u>ω</u> 就是去除了系统 F 对应特性的系统 F ω ，也叫系统 F <u>ω</u> 。右下的 λP 就是在简单类型 λ 中加入了 <code>* → □</code> 的 λ 演算，而这样的类型系统中类型依赖值所以也叫依赖类型系统（Dependent Type System），在 C++ 中模板可以有值参数所以实际上 C++ 的类型系统中包括依赖类型（Dependent Type）。</p>
+<p>左下角的 λ→ 就是简单类型 λ 演算，和它相连的三条边对应在其基础上分别添加了三种不同函数的 λ 演算。 λ2 就是系统 F ，包含 <code>(□, *)</code> 函数。 λ<u>ω</u> 就是去除了系统 F 对应特性的系统 F ω ，也叫系统 F <u>ω</u> 。右下的 λP 就是在简单类型 λ 中加入了 <code>(*, □)</code> 的 λ 演算，而这样的类型系统中类型依赖值所以也叫依赖类型系统（Dependent Type System），在 C++ 中模板可以有值参数所以实际上 C++ 的类型系统中包括依赖类型（Dependent Type）。</p>
 <p>这个立方体就被称为 λ 立方（Lambda Cube）。</p>
 <h2 id="构造演算">构造演算</h2>
-<p>在 λ 立方的顶端放着 λC ，也叫构造演算（Calculus of Construction, CoC），它的类型系统被称为纯类型系统（Pure Type System, PTS）。在构造演算中类型可以作为函数的输入，也可以作为函数的输出，那么实际上我们可以把项和函数作为相同的东西，不再加以区分。这样四种不同的函数也可以不加以区分放在一起，同时加入类别（Sort）来表达类型和类型的类型。而且因为 <code>A → B</code> 等价于 <code>∀ _: A. B</code> ，那么系统 F ω 中的 <code>TForall</code> 和 <code>TArr</code> 也可以合并。这样 CoC 的语法树表示如下：</p>
+<p>在 λ 立方的顶端放着 λC ，也叫构造演算（Calculus of Construction, CoC）。在构造演算中类型可以作为函数的输入，也可以作为函数的输出，那么实际上我们可以把项和函数作为相同的东西，不再加以区分。这样四种不同的函数也可以不加以区分放在一起，同时加入类别（Sort）来表达类型和类型的类型。而且因为 <code>A → B</code> 等价于 <code>∀ _: A. B</code> ，那么系统 F ω 中的 <code>TForall</code> 和 <code>TArr</code> 也可以合并。这样 CoC 的语法树表示如下：</p>
 <pre><code class="language-java"><span class="hljs-class"><span class="hljs-keyword">interface</span> <span class="hljs-title">Expr</span> </span>{
     <span class="hljs-function">Expr <span class="hljs-title">genUUID</span><span class="hljs-params">()</span></span>;
     <span class="hljs-function">Expr <span class="hljs-title">applyUUID</span><span class="hljs-params">(Val v)</span></span>;
@@ -86,7 +87,7 @@ <h2 id="构造演算">构造演算</h2>
 <span class="hljs-class"><span class="hljs-keyword">class</span> <span class="hljs-title">Val</span> <span class="hljs-keyword">implements</span> <span class="hljs-title">Expr</span> </span>{
     <span class="hljs-function"><span class="hljs-keyword">public</span> Expr <span class="hljs-title">checkType</span><span class="hljs-params">(Env env)</span> <span class="hljs-keyword">throws</span> BadTypeException </span>{
         <span class="hljs-keyword">if</span> (t == <span class="hljs-keyword">null</span>) <span class="hljs-keyword">return</span> env.lookup(id);
-        <span class="hljs-keyword">return</span> t.fullReduce();
+        <span class="hljs-keyword">return</span> t;
     }
 }
 
@@ -104,7 +105,8 @@ <h2 id="构造演算">构造演算</h2>
         Expr tf = f.checkType(env);
         <span class="hljs-keyword">if</span> (tf <span class="hljs-keyword">instanceof</span> Pi) {
             Pi pi = (Pi) tf;
-            <span class="hljs-keyword">if</span> (x.checkType(env).equals(pi.x.checkType(env)))
+            <span class="hljs-keyword">if</span> (x.checkType(env).fullReduce().equals(
+                    pi.x.checkType(env).fullReduce()))
                 <span class="hljs-keyword">return</span> pi.e.apply(pi.x, x);
         }
         <span class="hljs-keyword">throw</span> <span class="hljs-keyword">new</span> BadTypeException();

html/SysFO.html

@@ -80,7 +80,7 @@ <h3 id="by-「玩火」">By 「玩火」</h3>
     Type t;
     <span class="hljs-function"><span class="hljs-keyword">public</span> Type <span class="hljs-title">checkType</span><span class="hljs-params">(Env env)</span> </span>{
         <span class="hljs-keyword">if</span> (t == <span class="hljs-keyword">null</span>) <span class="hljs-keyword">return</span> env.lookup(x);
-        <span class="hljs-keyword">return</span> t.fullReduce();
+        <span class="hljs-keyword">return</span> t;
     }
 }
 <span class="hljs-class"><span class="hljs-keyword">class</span> <span class="hljs-title">Fun</span> <span class="hljs-keyword">implements</span> <span class="hljs-title">Expr</span> </span>{