Re: [Caml-list] GADT in an optional parameter

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/07/18, at 23:03, David Allsopp <dra-news@metastack.com> wrote:

> 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? 

No, clearly no.
Optional arguments have no impact on typing: the absence of an optional
argument cannot force some extra equation.
I agree this would be interesting, but then we would need a way to express
it in the type. Otherwise, why would the user expect (s=t) when there is no
argument, whereas there is no way to see what the default is?
Something like:
val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's Map.Make(String).t -> 't

It would be good to see whether this has many applications.
In the past, there were some request to be able to default to the identity function.

	Jacques