9

我想使用该unification-fd包为 Hindley-Milner 类型系统实现一个简单的类型检查器。这需要多态（“forall”）类型的表示。

表示这些类型的最佳方式是什么？提供的变量unification-fd，即这些UVar东西，是用于统一（元）变量，而不是用于对象语言中的变量。我考虑过的一些可能性：

  1. 将类型变量的构造函数添加到表示类型的基本函子中：

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

    只有zipMatch 统一等于TVars。类型实例化始终将 every 替换UTerm (TVar a)为freeVar.

  2. (Ab) 使用s 表示类型变量，并在实例化时UVar将其替换为s。freeVar需要跟踪通用与存在UVar的 s 以了解要替换哪些。

  3. 在类型检查期间对单态类型、从外部可见的多态类型以及在对中间绑定变量TVar进行类型检查期间TyF，不使用 , 单独使用。UTerm (TyF tcon) IntVarUTerm (TyF tcon) tvUTerm (TyF tcon) (Either tv IntVar)let

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

4

0 回答 0