Abusing exceptions

I was trying to implement Ken Shan, et al's fair backtracking monad (ICFP 2005) yesterday for the InforML typechecker. However, no matter how I tried implementing it, I would become stuck trying to give them a type because SML doesn't have existential data types. It kept gnawing at me and this morning it came to me that by abusing local exception definitions I could work around this. It wouldn't work if, like OCaml, SML only allowed top level exception definitions. It might also be possible to use SML/NJ's callcc, but I had an easier time wrapping my head around this.

 
type env
 
(* Takes an environment, a success "continuation",
and a failure "continuation", and pretends that it
will give you an exception back *)
 
type 'a monad = env -> (env * 'a -> exn) -> exn -> exn
 
infix 5 >>=
infix 5 >>
infix 5 ||
 
(* Unit *)
fun return x =
    (fn s => fn sk => fn fk => raise (sk (s, x)))
 
(* Bind *)
fun (m : 'a monad) >>= (f : 'a -> 'b monad) =
    let
      exception SuccCont of env * 'a
    in
      (fn s => fn sk => fn fk =>
         (m s SuccCont fk)
         handle SuccCont (s', x) => ((f x) s sk fk))
    end
 
(* Sequence *)
fun (m1 : 'a monad) >> (m2 : 'b monad) =
  [| x | _ <~ m1, x <~ m2 |]
 
(* Choice *)
fun (m1 : 'a monad) || (m2 : 'a monad) =
    let
      exception FailCont
    in
      (fn s => fn sk => fn fk =>
         (m1 s sk FailCont)
         handle FailCont => (m2 s sk fk))
    end
 
(* Zero, disjunctive unit *)
val zero = (fn s => fn sk => fn fk => raise fk)
 

Leave a Comment

Powered by WP Hashcash