refl.ml

(* from https://okmij.org/ftp/ML/first-class-modules/ *)
module Eq = struct
  type ('a,'b) eq = Refl of 'a option ref * 'b option ref

  let refl () = let r = ref None in Refl (r,r)

  let symm : ('a,'b) eq -> ('b,'a) eq = function 
      Refl (x,y) -> Refl (y,x)


  let apply_eq : ('a,'b) eq -> 'a -> 'b = function
      Refl (rx,ry) -> fun x ->
        rx := Some x;
        match !ry with
	| Some y -> rx := None; y
	|     _  -> failwith "Impossible"

  let apply_eq' : ('a,'b) eq -> 'a -> 'b = function
      Refl _ -> Fun.id
end

open Eq

module Example: sig
        type t
        val x: t
        val eq: (t, int) eq
end = struct
    type t = int
    let x = 3
    let eq : (t, int) eq = refl ()
end

let z: int = apply_eq Example.eq Example.x