(* The standard type representation and comparison machinery Some day it would be built-in into OCaml, and teq would be built-in The present code is fully generic and extensible: whenever a user defines their own data type, all they need to do is to extend the trep (and register the extension to teq -- although the latter can be gotten around of). *) (* Type representation GADT -- extensible *) type _ trep = .. type (_,_) eq = Refl : ('a,'a) eq (* The initial registry, for common data types *) type _ trep += | Unit : unit trep | Int : int trep | Bool : bool trep | String : string trep | Option : 'a trep -> 'a option trep | List : 'a trep -> 'a list trep | Pair : 'a trep * 'b trep -> ('a * 'b) trep | Fun : 'a trep * 'b trep -> ('a -> 'b) trep (* Type comparison function The following is the generic implementation that works once and for all, for any future extensions of trep let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> if Obj.repr x = Obj.repr y then Some (Obj.magic Refl) else None *) (* But we foreswear magic, and implement teq strictly above the board *) type teq_t = {teq: 'a 'b. 'a trep -> 'b trep -> ('a,'b) eq option} let teqref : teq_t ref = ref {teq = fun x y -> None} (* default case *) let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> (!teqref).teq x y (* Registering an extension of teq *) let teq_extend : teq_t -> unit = fun {teq = ext} -> let {teq=teq_old} = !teqref in teqref := {teq = fun x y -> match ext x y with None -> teq_old x y | r -> r} (* Registering the initial extension *) let () = let teq_init : type a b. a trep -> b trep -> (a,b) eq option = fun x y -> match (x,y) with | (Unit,Unit) -> Some Refl | (Int,Int) -> Some Refl | (Bool,Bool) -> Some Refl | (String,String) -> Some Refl | (Option x, Option y) -> begin match teq x y with | Some Refl -> Some Refl | _ -> None end | (List x, List y) -> begin match teq x y with | Some Refl -> Some Refl | _ -> None end | (Pair (x1,x2), Pair (y1,y2)) -> begin match (teq x1 y1, teq x2 y2) with | (Some Refl, Some Refl) -> Some Refl | _ -> None end | (Fun (x1,x2), Fun (y1,y2)) -> begin match (teq x1 y1, teq x2 y2) with | (Some Refl, Some Refl) -> Some Refl | _ -> None end | _ -> None in teq_extend {teq = teq_init} ;;