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

[Alain Frisch <alain@frisch.fr>]

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