OCaml 中的扩展型方程生成器答案

【问题标题】：expanding type equation generator in OCamlOCaml 中的扩展型方程生成器
【发布时间】：2020-12-03 08:34:09
【问题描述】：

type exp = 
  | CONST of int
  | VAR of var
  | ADD of exp * exp
  | SUB of exp * exp
  | ISZERO of exp
  | IF of exp * exp * exp
  | LET of var * exp * exp
  | PROC of var * exp
  | CALL of exp * exp
and var = string

type typ = TyInt | TyBool | TyFun of typ * typ | TyVar of tyvar
and tyvar = string

type typ_eqn = (typ * typ) list

module TEnv = struct
  type t = var -> typ
  let empty = fun _ -> raise (Failure "Type Env is empty")
  let extend (x,t) tenv = fun y -> if x = y then t else (tenv y)
  let find tenv x = tenv x
end

let rec gen_equations : TEnv.t -> exp -> typ -> typ_eqn 
=fun tenv e ty -> match e with
| CONST n -> [(ty, TyInt)]
| VAR x -> [(ty, TEnv.find tenv x)]
| ADD (e1,e2) -> [(ty, TyInt)]@
    [gen_equations (tenv, e1, TyInt)]@
    [gen_equations (tenv, e2, TyInt)]

Implementing type equation generator in OCaml

我正在根据上面的代码扩展类型检查器

我要做的是添加“EQUAL”表达式，它接受两个输入并返回 TyBool 作为输出

问题是如何制作输入方程，因为输入不是固定类型。

EQUAL 可以同时接受 TyInt 和 TyBool 作为输入

例如）

EQUAL (FALSE, FALSE) 有输出 TRUE（因为 false == false）

EQUAL (5, 3) 的输出为 FALSE（因为 5 != 3）

我该如何做方程？

【问题讨论】：

标签： ocaml typechecking

【解决方案1】：

您的EQUAL 表达式具有多态类型，即它可用于整数和变量。作为语言设计者，您可以选择实现哪种多态性。您可以从经典的parametric polymorphism 开始。在这种情况下，您将输入EQUAL 为'a -> 'a -> bool，或者，用您的表述方式，

TyFun (TyVar a, TyFun (TyVar a, TyBool))

然后，在统一过程中，类型变量a将与TyBool或TyVar统一（好吧，它也可以与函数类型统一，如果你愿意，你可以把它变成类型错误）。

或者，您可以使用ad-hoc polymorphism 实现EQUAL。不过，这将要求您更改类型系统，即将新的构造函数添加到您的类型typ。您可以采用类型类方法并拥有TyCls of string * typ 并为EQUAL 提供以下类型，

TyFun (TyCls ("comparable",t), TyFun (TyCls ("comparable",t), TyBool))

但类型类的推断很困难，而且并不总是可判定的。

【讨论】：