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

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

Thanks for replies on this!

Jacques Garrigue wrote:
> 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

Yes, indeed - a head-crashing-into-the-desk moment!

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

More follows, but both this and my actual application, in which many functions may return both a value and a list of messages but in many instances the messages can be ignored, are quite useful - but I concede that something which boils down to syntactic sugar is not too compelling an application!

oleg@okmij.org wrote:
> > 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?
> 
> Actually a default parameter is syntactic sugar. When the type checker
> sees
> 
>         fun ?(p=v) -> body
> 
> it essentially macro-expands the expression to the following
> 
>    fun xxOpt -> let p = match xxOpt with
>                          | Some xxSth -> xxSth
>                          | None       -> v
>                 in body

<snip>
 
> Again, a function that pattern-matches on GADT can be polymorphic. A
> function/expression that _produces_ GADT (that is, uses GADT constructors
> to produce values) cannot be polymorphic in the resulting GADT.

So if I understand correctly, what would be needed here would be a special case for dealing with optional arguments where the default is a GADT constructor.

Two ideas...

Alain Frisch wrote:
> On 07/19/2013 08:59 AM, Jacques Garrigue wrote:
> > 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.
> 
> The idea would be to have a different kind of optional argument, which
> specifies as part of the function type an expression to be expanded
> syntactically on the call site when the argument is not provided
> explicitly.  (In your example, the Exn constructor would need to be
> available from the call site.  -- Or do you interpret "Exn" as a typed
> reference to the Exn constructor on the value declaration site?)
> 
> If we assume that the "default" can be an arbitrary "parse tree"
> (untyped) expression, I guess that type equality would require these
> expressions to be strictly equal (modulo locations).

That seems very powerful, but presumably similarly hard? I'm guessing that at the moment the .cmi file doesn't contain any indication of whether an optional argument has a default or not (because it's an implementation detail transformed in the code as Oleg explained). Would that be a reasonably easy change to make? It feels very weird suddenly needing code to be included in a type! Or is this is a better halfway house...

Gabriel Scherer wrote:
> Another option could be to keep a non-desugaring explanation of optional
> arguments, but used a GADT type carrying more static information than ('a
> option). Something like:
> 
>   type ('default, _) rich_option =
>     | RSome : 'a -> ('default, 'a) rich_option
>     | RNone : ('default, 'default) rich_option
> 
>   let default : type def s . def -> (def, s) rich_option -> s = fun def ->
> function
>     | RNone -> def
>     | RSome v -> v

I'd experimented with something along these lines - I even tried seeing if redefining 'a option could trick the compiler, but it was not to be fooled!

> If optional keywords desugared to rich_option instead of option, we could
> maybe (I haven't tested) write something like
> 
>   let find_mode : type s t . (s, t) wrap -> (s -> bool) -> s list -> t =
> fun mode p li ->
>     match mode with
>       | Exn -> List.find p li
>       | Option -> try Some (List.find p li) with Not_found -> None
> 
>   let find : type s t . ?mode:(((s,s) wrap, (s,t) wrap) rich_option)
> -> (s -> bool) -> s list -> t =
>     fun ?mode p li -> find_mode (default Exn mode) p li
> 
> Remark: The OCaml syntax for optional argument uses ?mode:'a rather than
> ?mode:('a option), talking of the value type instead of the option type.
> This isn't possible anymore with rich_option whose type cannot be deduced
> from its second parameter, and arguably using ?mode:('a option) would make
> slightly clearer the type of "mode" in the call (f ?mode ...).

This seems quite nice. So, thinking of the syntax used for GADTs themselves we could have something like (note using equals instead of colon):

let find : type s t . ?mode = ((s, s) wrap, (s, t) wrap) rich_option -> (s -> bool) -> s list -> t = ...

with the requirement that the type used for an optional argument specified with equals instead of colon must have at least one constant constructor which should be used as the default. That feels as though it would be pretty easy for both type checking and implementation?

The final question is would one or both of these suggestions be likely to be made/accepted and, if so, is it worth opening a feature request in Mantis?


David