From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alain@frisch.fr>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id 2B6147ED25
	for <caml-list@sympa.inria.fr>; Fri, 19 Jul 2013 12:38:05 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=pra; client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  alain@frisch.fr) identity=mailfrom; client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr"; x-sender="alain@frisch.fr";
  x-conformance=sidf_compatible
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@msa.smtpout.orange.fr) identity=helo;
  client-ip=193.252.23.211;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="alain@frisch.fr";
  x-sender="postmaster@msa.smtpout.orange.fr";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AikBAGIW6VHB/BfTlGdsb2JhbABRCQ6DLr4egnaBJw4BAQEBCQsJCRQDJYIkAQEFJxFBEAsYCSUPAkYGAQwBBwEBiBC2R45UgQgzB4N8A5ddhiONfkA
X-IPAS-Result: AikBAGIW6VHB/BfTlGdsb2JhbABRCQ6DLr4egnaBJw4BAQEBCQsJCRQDJYIkAQEFJxFBEAsYCSUPAkYGAQwBBwEBiBC2R45UgQgzB4N8A5ddhiONfkA
X-IronPort-AV: E=Sophos;i="4.89,700,1367964000"; 
   d="scan'208";a="21681511"
Received: from msa02.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.211])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 19 Jul 2013 12:38:04 +0200
Received: from [192.168.1.111] ([92.151.112.23])
	by mwinf5d06 with ME
	id 2Adz1m00E0WLdRo03Ae0nU; Fri, 19 Jul 2013 12:38:04 +0200
Message-ID: <51E91707.60002@frisch.fr>
Date: Fri, 19 Jul 2013 12:37:59 +0200
From: Alain Frisch <alain@frisch.fr>
User-Agent: Mozilla/5.0 (X11; Linux i686 on x86_64; rv:23.0) Gecko/20100101 Thunderbird/23.0
MIME-Version: 1.0
To: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>, 
 David Allsopp <dra-news@metastack.com>
CC: OCaml List <caml-list@inria.fr>
References: <000001ce83bf$879e6520$96db2f60$@metastack.com> <37C2C45C-A317-408E-8545-4FD426E3C817@math.nagoya-u.ac.jp>
In-Reply-To: <37C2C45C-A317-408E-8545-4FD426E3C817@math.nagoya-u.ac.jp>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] GADT in an optional parameter

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