[Caml-list] GADT in an optional parameter

["David Allsopp" <dra-news@metastack.com>]

So, continuing my forays into sections of type theory I clearly don't
properly understand! Although I was trying to use it for something else, my
problem here is equivalent to a rather over-discussed problem on this list -
namely, raising exceptions vs wrapping results in 'a option

I defined the following GADT:

type ('a, 'b) wrap = Option : ('a, 'a option) wrap
                   | Exn : ('a, 'a) wrap

I then created the following alternate implementation of Map where find
takes that GADT as its first parameter:

module StringMap =
  struct
    include Map.Make(String)

    let find : type s t . (s, t) wrap -> string -> s Map.Make(String).t -> t
= fun mode key map ->
      match mode with
        Exn ->
          find key map
      | Option ->
          try
            Some (find key map)
          with Not_found -> None
  end

So far so good, as we can have:

StringMap.find Option "foo" StringMap.empty;; (* None *)
StringMap.find Exn "foo" StringMap.empty;;    (* Not_found raised *)

which is quite nice (ignoring any quite optimisable and probably negligible
overhead of the extra match clause verses having two functions find and
find_option).

I then wanted to try to make the first parameter optional, defaulting to Exn
(so you'd get the vanilla behaviour of Map.find):

module StringMap =
  struct
    include Map.Make(String)

    let find : type s t . ?mode:(s, t) wrap -> string -> s
Map.Make(String).t -> t = fun ?(mode = Exn) key map ->
      match mode with
        Exn ->
          find key map
      | Option ->
          try
            Some (find key map)
          with Not_found -> None
  end

But I get: This expression has type (s, s) wrap but an expression was
expected of type (s, t) wrap on the Exn default value.

Now, in my woolly way, I thought that the default value for an optional
parameter behaved /almost/ like syntactic sugar, but clearly not. Is there a
way to annotate this to achieve what I'm after? 


David