Преобразование GADT в типы фантомов

Question

Я играл с GADT и фантомными типами в OCaml. Я понял, что GADT - это удобство для описания определенных видов фантомных типов - поправьте меня, если я ошибаюсь. Поэтому я решил попробовать конвертировать программу с использованием типа GADT в один с ADT и фантомными типами.

Я взял программу GADT от this blog post в качестве отправной точки. Это маленький/выражение INT BOOL оценщик, вот суть его:

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> 

Вот почему наличие фантомного типа недостаточно, и именно поэтому GADT был представлен в OCaml.