refl.ml

refl.ml

(* supertype *)
type (_, _) st =
  | Refl : ('a, 'a) st 
  | Fst : ('a, 'a * 'b) st
  | Snd : ('a, 'b) st -> ('a, 'c * 'b) st
  | Left : (('a, 'b) result, 'a) st
        
type _ ttype =
  | Int : int ttype
  | Bool : bool ttype
  | Pair : 'a ttype * 'b ttype -> ('a * 'b) ttype 
      
let rec check_st : type a b . a ttype * b ttype -> (a, b) st option =
  function
  | Int, Int -> Some Refl (* use eq! *)
  | Bool, Bool -> Some Refl  (* use eq! *)
  | Int, Pair (Int, b) -> Some Fst (* use eq! *)
  | Bool, Pair (Bool, b) -> Some Fst (* use eq! *)
  | x,   Pair (a, Pair (b, c)) -> Option.map (fun x -> Snd x) (check_st (x, Pair (b, c)))
  | _ -> None
                            
let rec get : type a b . (a, b) st -> b -> a = 
  function
  | Refl -> (fun x -> x) 
  | Fst -> (fun (x, y) -> x)
  | Snd st -> (fun (x, y) -> get st y)
  | Left -> (fun x -> Ok x)
            
            
let () = 
  let f = match check_st (Int, (Pair (Bool, (Pair (Int, Bool))))) with 
    | Some f -> f
    | None -> Stdlib.failwith "assert"
  in
  Format.printf "%d" (get f (true, (2, false)))