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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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

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

On Fri, Jul 19, 2013 at 12:37 PM, Alain Frisch <alain@frisch.fr> 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).
>
> This could have several interesting usages:
>
>   - Passing the "identity" function as a continuation, or a GADT to
> customize the return type.
>
>   - Implicit arguments, capturing an identifier from the scope of the call
> site:
>
>
>      let rec eval ??(env = env) x =
>      ...
>        | ... -> eval y  (* pass "env" implicitly *)
>        | ... -> eval env' z
>
>
>   - Implement the implicit passing of "runtime type representations":
>
>       let variant ??(t : 'a ty = (type of _)) (x : 'a) = ....
>
>     or of values synthesized by -ppx rewriters on the call site:
>
>       let debug ??(loc = [%self_loc]) x =
>         Format.eprintf "%a %s@." pp_loc loc x
>
>     (this uses the syntax of extension nodes in the extension_points branch,
> and assumes that the call site will be processed with a -ppx rewriter which
> substitutes a value representing the current location in the source code for
> the [%self_loc] extension node.)
>
>
> Alain
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs