unification in Eff

unification.eff

type fresh = effect
 operation gensym : unit -> int
end

let run s = handler
 | val y -> (fun s -> y)
 | s#gensym () k -> (fun s -> k s (s+1))
 | finally f -> f 0;;

let g = new fresh in with run g handle
    g#gensym () :: g#gensym () :: g#gensym () :: [] ;;


type 'a var = Ref of int | Concrete of 'a

type 'a logic = effect
 operation fresh : unit -> 'a var
 operation walk : 'a var -> 'a var
 operation associate : (int * 'a var) -> unit
end

let g = new fresh

let runL s = handler
 | val y -> (fun store -> y)
 | s#fresh () k -> (fun store -> k (Ref (g#gensym ())) store)
 | s#walk var k ->
  (fun store ->
    let rec walk' var =
      match var with
      | Ref i -> (match assoc i store with
                  | None -> k var store (* fresh! *)
                  | Some var'' -> walk' var'')
      | Concrete var' -> k var store
    in walk' var)
 | s#associate (i, v) k -> (fun store ->
    k () ((i, v) :: store))
 | finally f -> f [];;

type foo = X | Y

let l = new logic

type 'a result = Failure | Success of 'a

type 'a unify = effect
 operation eq : ('a * 'a) -> 'a
end

let runU u = handler
 | val y -> Success y
 | u#eq (x,y) k ->
   (match ((l#walk x), (l#walk y)) with
    | (Concrete X, Concrete X) -> k (Concrete X)
    | (Concrete Y, Concrete Y) -> k (Concrete Y)
    | (Ref i, Ref j) -> if i = j then k (Ref i) else let _ = l#associate (i,Ref j) in k (Ref j)
    | (Ref i, v) -> (let _ = l#associate (i,v) in k v)
    | (v, Ref i) -> (let _ = l#associate (i,v) in k v)
    | _ -> Failure)

let u = new unify

(*
# with run g handle with runL l handle l#fresh () :: l#fresh () :: [] ;;
- : foo var list = [Ref 0; Ref 1]
*)

(*

# with run g handle with runL l handle with runU u handle let x = l#fresh () in let y = l#fresh () in let _ = u#eq (x,x) in l#walk x :: l#walk y :: [] ;;
- : foo var list result = Success [Ref 0; Ref 1]
# with run g handle with runL l handle with runU u handle let x = l#fresh () in let y = l#fresh () in let _ = u#eq (x,y) in l#walk x :: l#walk y :: [] ;;
- : foo var list result = Success [Ref 1; Ref 1]

# with run g handle with runL l handle with runU u handle let x = l#fresh () in let y = l#fresh () in let _ = u#eq (x,Concrete X) in l#walk x :: l#walk y :: [] ;;
- : foo var list result = Success [Concrete X; Ref 1]
# with run g handle with runL l handle with runU u handle let x = l#fresh () in let y = l#fresh () in let _ = u#eq (x,Concrete X) :: u#eq (x,y) :: [] in l#walk x :: l#walk y :: [] ;;
- : foo var list result = Success [Concrete X; Concrete X]
# with run g handle with runL l handle with runU u handle let x = l#fresh () in let y = l#fresh () in let _ = u#eq (x,Concrete X) :: u#eq (x,y) :: u#eq (y,Concrete Y) :: [] in l#walk x :: l#walk y :: [] ;;
- : foo var list result = Failure

*)