From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 B10A27ED25 for ; Fri, 19 Jul 2013 18:34:13 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.48 as permitted sender) identity=mailfrom; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f48.google.com) identity=helo; client-ip=209.85.214.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f48.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBABtq6VHRVdYwk2dsb2JhbABSCYM7UK4jkiaBCAgWDgEBAQEHCwsJFAQkgiQBAQUnGQEbEgsBAwwGBQsNDSEiAREBBQEKEgYTCAqHawEDDwyZJYxPgn+ESgoZJwMKZId0AQUMjkiBOweDfgOXXYEpjj8WKYQ6Og X-IPAS-Result: AtEBABtq6VHRVdYwk2dsb2JhbABSCYM7UK4jkiaBCAgWDgEBAQEHCwsJFAQkgiQBAQUnGQEbEgsBAwwGBQsNDSEiAREBBQEKEgYTCAqHawEDDwyZJYxPgn+ESgoZJwMKZId0AQUMjkiBOweDfgOXXYEpjj8WKYQ6Og X-IronPort-AV: E=Sophos;i="4.89,702,1367964000"; d="scan'208";a="21721266" Received: from mail-bk0-f48.google.com ([209.85.214.48]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Jul 2013 18:34:12 +0200 Received: by mail-bk0-f48.google.com with SMTP id jf17so1680349bkc.21 for ; Fri, 19 Jul 2013 09:34:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=Aj2p5rJtWCCPGrk+ucEojWFMqbXac4BF18pxJCGdAP8=; b=xJW3KZEgHDy2xKfmvzZ8aSmbQfnsGGumE2ZxIFvHU5UD/twpWhYxxTazNqycCEVrCl 9uIwhy5CpXb0HZeMbGwyN9UQCDD2tub0hLqsp3k8rE3CubiR2xe1ekmU1tZgT2oD8Q6Q lNF3STlC0EJa/4ERbzw38DM+IH+0WDAJcl0gvpZALkuGTM9tzJleRDdAQz2R0B0SDfWV l+2fiN808yIBtVEQ6XpW/KcZ9kL0XHkKR2Ot63t/msNFt5V7VZAVZYY6ROopRczu6FdR eBpwi0Gd/OV6MMVlJni6IXhaukg/Xyas/rekswGLNxbL3pkq+8q59Zf/Bk4CWvuIRzpZ 9QAw== X-Received: by 10.204.76.141 with SMTP id c13mr2670796bkk.42.1374251652321; Fri, 19 Jul 2013 09:34:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.20.131 with HTTP; Fri, 19 Jul 2013 09:33:32 -0700 (PDT) In-Reply-To: <51E91707.60002@frisch.fr> References: <000001ce83bf$879e6520$96db2f60$@metastack.com> <37C2C45C-A317-408E-8545-4FD426E3C817@math.nagoya-u.ac.jp> <51E91707.60002@frisch.fr> From: Gabriel Scherer Date: Fri, 19 Jul 2013 18:33:32 +0200 Message-ID: To: Alain Frisch Cc: Jacques Garrigue , David Allsopp , OCaml List Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADT in an optional parameter 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 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