为什么要引入类型?

如果每个变量都没有类型,那又如何?

类型信息,可被用来判断一个表达式是否是可求值的。

即,在不知道这个表达式的各变量的值的情况下,
之根据上下文类型信息,
静态判断该表达式是否是可求值的,且推导出该表达式的的结果类型。

什么样的表达式是合法,但是不适合作静态类型推导的?
例如这样的
x?3:true
我们无法得知该表达式究竟是会返回一个整数类型的值还是一个bool类型的值。
于是无论是C还是ocaml,都规定其两个分支必须返回相同类型的值。

再例如:

struct Pair{
    int first;
    int last
};
int x;
Pair p;
...
if(x?3:p){
}

如果这样的代码也合法,那么我们无法静态的检查if条件语句的语法有效性。
再设想一下,C是完全没有动态类型信息的。C++本来也没有。
如果我们是在运行时才发现我们将错误的类型传递给了if的条件子句。那么……
1。程序只能异常的执行,或者突然终止而且我们不知道它为什么会终止
2。我们无法给出任何有价值的出错信息。只能告诉用户if语句执行失败。

于是我们为项引入类型信息。
但是,我们希望:
去处类型信息后再求值,与求值后再去除类型信息,应该得到相同的结果。

就好比一致连续性对于函数算子的可交换性一样,上面的限制,对于有类型项的求值运算,至关重要。

我希望能在图书馆找到martin-lof类型理论方面的书籍,尽管这已经是40年前的理论了。

再说序列点。
C/C++中的分号被称作一种senqence point,它标志着一个语句的结束。
那么,其语义是什么?

如果把每一行语句都抽象成一个函数。那么可以把其变量值的上下文理解为函数参数,把其返回值,作为下一个函数的参数。
只不过,下一个函数的执行过程中永远用不到这个参数。

从lambda演算的角度来讲。
m;t
可以被理解为
λx.t m
其中项t中不含有x.

此博客中的热门博文

少写代码,多读别人写的代码

在windows下使用llvm+clang

tensorflow distributed runtime初窥