用unification-fd表示多态性

Question

我想使用该unification-fd软件包为Hindley-Milner类型系统实现一个简单的类型检查器.这需要表示多态("forall")类型.

表示这些类型的最佳方式是什么？提供的变量unification-fd,即在UVar东西,是统一的(元)变量,而不是在对象语言的变量.我考虑过的一些可能性:

1. 将类型变量的构造函数添加到表示类型的基本仿函数:

   data TyF tcon tv a
       = TCon tcon [a]
       | TVar tv
   

   与zipMatch 只有统一平等TVar秒.类型实例化始终UTerm (TVar a)用a 替换每个freeVar.

2. (Ab)将UVars用于类型变量,并freeVar在实例化时用s 替换它们.需要跟踪普遍性与存在性,UVar以了解要替换哪些.

3. 退出TVar,在类型检查期间TyF单独使用单一UTerm (TyF tcon) IntVar类型,UTerm (TyF tcon) tv从外部可见的多态类型,以及UTerm (TyF tcon) (Either tv IntVar)在中间,let绑定变量的类型检查期间.

哪个最好？还有其他一些我没有想过的方法吗？