I played with GADT and phantom types in OCaml. I realized that GADT is a convenience for describing certain types of phantom types — correct me if I'm wrong. Therefore, I decided to try to convert the program using the GADT type into one with the ADT and phantom types.
As a starting point, I took the GADT program from this blog post . This is a small evaluator of the bool / int expression, here is its essence:
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 to 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 have no control over a variable like ADT constructors, so I created my own constructors _Bool, _Intetc. to force the creation of the required type.
However, my module ADTdoes 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
, , GADT ADT . - .