Converting GADT to phantom types

Question

I was playing around with GADT and phantom types in OCaml. I understood that GADT is a convenience for describing certain kinds of phantom types—correct me if I'm wrong. So I decided to try out to convert a program using GADT type into an one with ADT and phantom types.

I took an GADT program from this blog post as a starting point. It's a small bool/int expression evaluator, here's the gist of it:

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

So I started converting it into ADT + phantom types as follows:

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

You don't have control over type variable of ADT constructors, so I created my own _Bool, _Int, etc. constructors to force the necessary type.

However, my ADT module does not compile:

  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

At this point I assume that my idea is flawed and you can't convert GADT to ADT in this way. However I would like to hear someone more experienced on this topic.

ivg ivg · Accepted Answer · 2015-05-03T19:16:56

You can't do this without GADT, as phantom type cannot serve as a witness for a compiler, that an expression has specific type, since with phantom type you actually can do the following:

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

That's why having a phantom type is not sufficient, and that's why the GADT was introduced in OCaml.

Converting GADT to phantom types

1 Answers