Skip to content

Commit

Permalink
fix(Lambda) Env
Browse files Browse the repository at this point in the history
  • Loading branch information
@niltok
niltok committed Dec 25, 2020
1 parent 7ff833c commit f8b76ae
Show file tree
Hide file tree
Showing 8 changed files with 161 additions and 290 deletions.
50 changes: 18 additions & 32 deletions doc/CoC.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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` 检索。

这样就构造出了一个相当强大的类型系统，它的表现力已经超越了几乎所有常见语言的类型系统。之后将会介绍如何利用这个强大的类型系统表达复杂的类型，做一些常见类型系统做不到的事情。
97 changes: 38 additions & 59 deletions doc/STLC.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,19 +28,13 @@ class TVal implements Type {
public String toString() {
return name;
}
public boolean equals(Object o) {
// ...
}
}
// FunctionType
class TArr implements Type {
Type src, tar;
public String toString() {
return "(" + src + " → " + tar + ")";
}
public boolean equals(Object o) {
// ...
}
}
```

Expand All @@ -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` 的类型一致。

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

Expand All @@ -74,87 +87,53 @@ 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()));
}
}
```

而如果对

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

进行类型检查就会抛出 `BadTypeException` 。
43 changes: 13 additions & 30 deletions doc/SysFO.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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));
}
}
```
Expand All @@ -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 {
Expand All @@ -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))))))
Expand Down
Loading

0 comments on commit f8b76ae

Please sign in to comment.