我正在为一种新的函数式编程语言实现一种类型系统,目前正在编写将两种类型统一的函数。需要考虑四种情况:
+---------+---------+-------------------------------------------------------+
| k1 | k2 | action |
+=========+=========+=======================================================+
| var | var | k1 := k2 ^ k2 := k1 |
+---------+---------+-------------------------------------------------------+
| var | non var | if (!occurs(k1, k2)) k1 := k2 |
+---------+---------+-------------------------------------------------------+
| non var | var | if (!occurs(k2, k1)) k2 := k1 |
+---------+---------+-------------------------------------------------------+
| non var | non var | ensure same name and arity, and unify respective args |
+---------+---------+-------------------------------------------------------+
- 当
k1
和k2
都是变量时,它们会互相实例化。 - 当只有
k1
是变量时,如果k1
不出现在k2
中,则将其实例化为k2
。 - 当只有
k2
是变量时,如果k2
不出现在k1
中,则将其实例化为k1
。 - 否则,我们将检查
k1
和k2
是否具有相同的名称和arity,并统一它们各自的参数。
对于第二种和第三种情况,我们需要实现“出现检查”以避免陷入无限循环。但是,我怀疑程序员能够构造出无限的类型。
在Haskell中,构造无限类型很容易:
let f x = f
不过,我尽力了但是没有成功构建出无限种类。请注意,我没有使用任何语言扩展。
我问这个问题的原因是,如果根本无法构建无限种类,那么我就不会费心在我的种类系统中实现出现检查。