将GADT转换为幻影类型

Question

我在OCaml中玩GADT和幻影类型。我知道GADT是描述某些幻影类型的一种方便--如果我错了，请纠正我。因此，我决定尝试将使用GADT类型的程序转换为具有ADT和幻影类型的程序。

我把这篇博客文章的一个GADT程序作为起点。它是一个小的bool/int表达式计算器，下面是它的要点：

module GADT = struct
  type _ value =
    | Bool : bool -> bool value
    | Int : int -> int value

  type _ expr =
    | Value : 'a value -> 'a expr
    | If : bool expr * 'a expr * 'a expr -> 'a expr
    | Eq : 'a expr * 'a expr -> bool expr
    | Lt : int expr * int expr -> bool expr

  let rec eval : type a. a expr -> a = function
    | Value (Bool b) -> b
    | Value (Int i) -> i
    | If (b, l, r) -> if eval b then eval l else eval r
    | Eq (a, b) -> eval a = eval b
    | Lt (a,b) -> a < b
end

因此，我开始将其转换为ADT +幻影类型，如下所示：

module ADT = struct
  type 'a value =
    | Bool of bool
    | Int of int

  let _Bool b : bool value = Bool b
  let _Int  i :  int value = Int i

  type 'a expr =
    | Value of 'a value
    | If of bool expr * 'a expr * 'a expr
    | Eq of 'a expr * 'a expr
    | Lt of int expr * int expr

  let _Value v : 'a expr = Value v
  let _If (cond, cons, alt) : 'a expr = If (cond, cons, alt)
  let _Eq (left, right) : bool expr = Eq (left, right)
  let _Lt (left, right) : bool expr = Lt (left, right)

  let rec eval : type a. a expr -> a = function
    | Value (Bool b) -> b
    | Value (Int  i) -> i
    | If (cond, cons, alt) -> if eval cond then eval cons else eval alt
    | Eq (left, right) -> eval left = eval right
    | Lt (left, right) -> left < right
end

您无法控制ADT构造函数的类型变量，因此我创建了自己的_Bool、_Int等构造函数，以强制执行必要的类型。

但是，我的ADT模块没有编译：

  let rec eval : type a. a expr -> a = function
    | Value (Bool b) -> b
                        ^
Error: This expression has type bool but an expression was expected of type a 

此时，我假设我的想法是有缺陷的，您不能以这种方式将GADT转换为ADT。不过，我想听听在这个问题上更有经验的人。

Answer 1

如果没有GADT，您就无法做到这一点，因为幻影类型不能作为编译器的见证，因为表达式具有特定类型，因为有了幻影类型，您实际上可以执行以下操作：

let bool b : int value = Bool b;;
val bool : bool -> int value = <fun>

这就是为什么有一个幻影类型是不够的，这也是为什么在OCaml中引入了GADT。