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 86C0481799 for ; Thu, 25 Jul 2013 11:31:38 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of dra-news@metastack.com) identity=pra; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.com"; x-conformance=sidf_compatible Received-SPF: Neutral (mail3-smtp-sop.national.inria.fr: domain of dra-news@metastack.com does not assert whether or not 81.103.221.48 is permitted sender) identity=mailfrom; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.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@mtaout02-winn.ispmail.ntl.com) identity=helo; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="postmaster@mtaout02-winn.ispmail.ntl.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am4BAKHv8FFRZ90wlGdsb2JhbABRCYJlgSa9XoEYFg4BAQEBBw0JCRQDJYIkAQEBAwEnE0QLAgEIGAoUEDIlAQEEEwgSh3AHA7oTjkWBBziDEm4Dl1+UYYIq X-IPAS-Result: Am4BAKHv8FFRZ90wlGdsb2JhbABRCYJlgSa9XoEYFg4BAQEBBw0JCRQDJYIkAQEBAwEnE0QLAgEIGAoUEDIlAQEEEwgSh3AHA7oTjkWBBziDEm4Dl1+UYYIq X-IronPort-AV: E=Sophos;i="4.89,742,1367964000"; d="scan'208";a="22216692" Received: from mtaout02-winn.ispmail.ntl.com ([81.103.221.48]) by mail3-smtp-sop.national.inria.fr with ESMTP; 25 Jul 2013 11:31:37 +0200 Received: from aamtaout04-winn.ispmail.ntl.com ([81.103.221.35]) by mtaout02-winn.ispmail.ntl.com (InterMail vM.7.08.04.00 201-2186-134-20080326) with ESMTP id <20130725093136.CZQV23282.mtaout02-winn.ispmail.ntl.com@aamtaout04-winn.ispmail.ntl.com> for ; Thu, 25 Jul 2013 10:31:36 +0100 Received: from romulus.metastack.com ([81.98.252.242]) by aamtaout04-winn.ispmail.ntl.com (InterMail vG.3.00.04.00 201-2196-133-20080908) with ESMTP id <20130725093136.BAFM21648.aamtaout04-winn.ispmail.ntl.com@romulus.metastack.com> for ; Thu, 25 Jul 2013 10:31:36 +0100 Received: from remus.metastack.local (remus.metastack.com [172.16.0.1]) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id r6P9VXWG031721 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=FAIL) for ; Thu, 25 Jul 2013 10:31:33 +0100 Received: from Remus.metastack.local ([fe80::547c:3c42:e1da:eda2]) by Remus.metastack.local ([fe80::547c:3c42:e1da:eda2%10]) with mapi id 14.03.0123.003; Thu, 25 Jul 2013 10:31:33 +0100 From: David Allsopp To: OCaml List Thread-Topic: [Caml-list] GADT in an optional parameter Thread-Index: Ac6Dvpb+WbS2X7LISNO32SrC2vIKLgAhpU+AAAee3IAADGrdAAEgZeIA Date: Thu, 25 Jul 2013 09:31:32 +0000 Message-ID: References: <000001ce83bf$879e6520$96db2f60$@metastack.com> <37C2C45C-A317-408E-8545-4FD426E3C817@math.nagoya-u.ac.jp> <51E91707.60002@frisch.fr> In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [195.99.217.188] Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Organization: MetaStack Solutions Ltd. X-Scanned-By: MIMEDefang 2.65 on 172.16.0.20 X-Cloudmark-Analysis: v=1.1 cv=AUhbpHVS+xhHrj9wLCYAQoYnFLYUZdbP8UM0GmH2jwk= c=1 sm=0 a=olPXNMZe71cA:10 a=sEKNk4ebCGwA:10 a=cTs9vV391PwA:10 a=kj9zAlcOel0A:10 a=xqWC_Br6kY4A:10 a=SGJpDYsEAAAA:8 a=kH7fHfpiAAAA:8 a=7oJd2F0TcGr8_VDfCyMA:9 a=CjuIK1q_8ugA:10 a=dTth3pfvbawA:10 a=04wikQgyBYcA:10 a=HpAAvcLHHh0Zw7uRqdWCyQ==:117 Subject: RE: [Caml-list] GADT in an optional parameter Thanks for replies on this! Jacques Garrigue wrote: > On 2013/07/18, at 23:03, David Allsopp wrote: >=20 > > 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 =3D > > struct > > include Map.Make(String) > > > > let find : type s t . ?mode:(s, t) wrap -> string -> s > > Map.Make(String).t -> t =3D fun ?(mode =3D 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? >=20 > 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=3Dt) when there is > no argument, whereas there is no way to see what the default is? > Something like: > val find : ?mode:(('s,'t) wrap =3D 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 functi= ons may return both a value and a list of messages but in many instances th= e 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? >=20 > Actually a default parameter is syntactic sugar. When the type checker > sees >=20 > fun ?(p=3Dv) -> body >=20 > it essentially macro-expands the expression to the following >=20 > fun xxOpt -> let p =3D match xxOpt with > | Some xxSth -> xxSth > | None -> v > in body =20 > 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 constr= uctor. Two ideas... Alain Frisch wrote: > On 07/19/2013 08:59 AM, Jacques Garrigue wrote: > > val find : ?mode:(('s,'t) wrap =3D Exn) -> string -> 's > > Map.Make(String).t -> 't > > > > It would be good to see whether this has many applications. >=20 > 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?) >=20 > 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 op= tional argument has a default or not (because it's an implementation detail= transformed in the code as Oleg explained). Would that be a reasonably eas= y 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: >=20 > type ('default, _) rich_option =3D > | RSome : 'a -> ('default, 'a) rich_option > | RNone : ('default, 'default) rich_option >=20 > let default : type def s . def -> (def, s) rich_option -> s =3D 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 >=20 > let find_mode : type s t . (s, t) wrap -> (s -> bool) -> s list -> t = =3D > fun mode p li -> > match mode with > | Exn -> List.find p li > | Option -> try Some (List.find p li) with Not_found -> None >=20 > let find : type s t . ?mode:(((s,s) wrap, (s,t) wrap) rich_option) > -> (s -> bool) -> s list -> t =3D > fun ?mode p li -> find_mode (default Exn mode) p li >=20 > 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 =3D ((s, s) wrap, (s, t) wrap) rich_option -> (= s -> bool) -> s list -> t =3D ... with the requirement that the type used for an optional argument specified = with equals instead of colon must have at least one constant constructor wh= ich 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 b= e made/accepted and, if so, is it worth opening a feature request in Mantis? David