From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id D54097EE94 for ; Fri, 4 Jan 2013 18:25:29 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.210.172; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 209.85.210.172 as permitted sender) identity=mailfrom; client-ip=209.85.210.172; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ia0-f172.google.com) identity=helo; client-ip=209.85.210.172; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-ia0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYBAAoQ51DRVdKsm2dsb2JhbABFuWGDZAgWDgEBAQEBCAkLCRQngh4BAQQBJxkBGx0BAwELBgULDS4hAQERAQUBHAYTiAEBAwYDBgyZbIwzgnuETgoZJwwBWYVeAQEEDItchS0DlDWBVos3gzEWKYQX X-IronPort-AV: E=Sophos;i="4.84,411,1355094000"; d="scan'208";a="167453511" Received: from mail-ia0-f172.google.com ([209.85.210.172]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2013 18:25:28 +0100 Received: by mail-ia0-f172.google.com with SMTP id z13so13835916iaz.17 for ; Fri, 04 Jan 2013 09:25:27 -0800 (PST) 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=+Sletv/ppV2qH3ewF8trj64kVNUT4bzb3wnlbMabS/Y=; b=V1C2sAtLc7rjbPpT3myNR4ph8Kfm2zp5v2A3UsYCJEj0K+Ik9gQJEdAbponzm+Am7k sFHSuQ75LA/8zFBn8FAwS3CxGv6xWDBat40bY25+RM838ThwCfnclO4ksJBrF92x57wr 7foCgUQD0LgHUOnFZu7IBa5c0d8V4iRQodQgn+R8qiTuqcS8MrH7Ls8u43sdkI+xhrav 4/RXfGDaU+QhmxELk+P8KFN0/vO9W/YN22MsrYWyxSiVV2PHUzSWIV7UpuEM2BLYuW6J 6APtawtnt7QHkjkagAU0cnmb+4QT1UIAdRt03eACQ7oiMBq1c+ymHf9RrtUPgbLPpL+s aRxA== Received: by 10.50.13.162 with SMTP id i2mr46215875igc.38.1357320327118; Fri, 04 Jan 2013 09:25:27 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.6.226 with HTTP; Fri, 4 Jan 2013 09:25:07 -0800 (PST) In-Reply-To: <50E701D3.9070008@free.fr> References: <50E701D3.9070008@free.fr> From: Philippe Veber Date: Fri, 4 Jan 2013 18:25:07 +0100 Message-ID: To: Tiphaine Turpin Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d044469eff1bfaf04d279c369 X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --f46d044469eff1bfaf04d279c369 Content-Type: text/plain; charset=ISO-8859-1 This is pretty much what I asked for, thanks Tiphaine! ph. 2013/1/4 Tiphaine Turpin > Hi Philippe, > > I don't think that you can achieve what you are you are asking exactly, > unless ressorting to an existential type. You can do it using GADT too, as > described in the "existential types" section of > > https://sites.google.com/site/ocamlgadt/ > > For your example, you can write: > > type any_expr = > | Expr : _ expr -> any_expr > ;; > > let parse_expr x = > try Expr (Int (int_of_string x)) > with _ -> > Expr (Float (float_of_string x)) > ;; > > Cheers, > > Tiphaine > > > On 01/04/13 16:05, Philippe Veber wrote: > > Hi Yury, > > Thanks for your answer! It is true your fix is accepted by the compiler, > but this is not what I was looking for: in the end I'd like to have an 'a > expr such that 'a is the type of the value obtained when evaluating the > expression. With the polymorphic variants, I cannot write an eval function > of type 'a eval -> 'a, which is the main motivation behind using GADT in > that (canonical) case. Sorry for ommiting this point! > > ph. > > > 2013/1/4 Yury Sulsky > >> Hi Philippe, >> >> I think you can do this by using a polymorphic variant as the type >> variable: >> >> type _ expr = >> | Int : int -> [> `int ] expr >> | Float : float -> [> `float ] expr >> >> let parse_expr : string -> [ `int | `float ] expr = fun x -> >> try Int (int_of_string x) >> with _ -> >> Float (float_of_string x) >> ;; >> >> - Yury >> >> >> >> On Fri, Jan 4, 2013 at 8:32 AM, Philippe Veber wrote: >> >>> Dear list, >>> >>> Suppose I define a GADT for expressions: >>> >>> type _ expr = >>> | Int : int -> int expr >>> | Float : float -> float expr >>> >>> Now I want to write a parser, that will build an ['a expr] from a >>> string. Without thinking much, I tried the following: >>> >>> let parse_expr : type s. string -> s expr = fun x -> >>> try Int (int_of_string x) >>> with _ -> >>> Float (float_of_string x) >>> ;; >>> >>> Which fails with the following error message: >>> >>> Error: This expression has type int expr but an expression was expected >>> of type s expr >>> >>> That makes sense, since [s] is a locally abstract type. I tried a couple >>> of variants and finally realised that I could not even write the type of >>> [parse_expr]: it should be [string -> 'a expr] for some ['a], but I'm not >>> sure that really means something. >>> >>> So to put it simple, how does one construct a GADT value from a string ? >>> >>> Cheers, >>> ph. >>> >> >> > > > --f46d044469eff1bfaf04d279c369 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable This is pretty much what I asked for, thanks Tiphaine!
ph.

2013/1/4 Tiphaine Turpin <Tiphaine.Turpin@free.= fr>
=20=20 =20=20=20=20 =20=20
Hi Philippe,

I don't think that you can achieve what you are you are asking exactly, unless ressorting to an existential type. You can do it using GADT too, as described in the "existential types" secti= on of

= https://sites.google.com/site/ocamlgadt/

For your example, you can write:

type any_expr =3D
=A0 | Expr : _ expr -> any_expr
;;

let parse_expr x =3D
=A0 try Expr (Int (int_of_string x))
=A0 with _ ->
=A0=A0=A0 Expr (Float (float_of_string x))
;;

Cheers,

Tiphaine


On 01/04/13 16:05, Philippe Veber wrote:
Hi Yury,

Thanks for your answer! It is true your fix is accepted by the compiler, but this is not what I was looking for: in the end I'd like to have an 'a expr such that 'a is the type of the value obtained when evaluating the expression. With the polymorphic variants, I cannot write an eval function of type 'a eval -> 'a, which is the main motivation behind using GADT in that (canonical) case. Sorry for ommiting this point!

ph.


2013/1/4 Yury Sulsky <= ;yury.sulsky@gma= il.com>
Hi Philippe,

I think you can do this by using a polymorphic variant as the type variable:

type _ expr =3D
| Int : int -> [> `int ] expr
| Float : float -> [> `float ] expr

let parse_expr : string -> [ `int | `float ] expr =3D fun x ->=A0
=A0 try Int (int_of_string x)=A0
=A0 with _ ->=A0
=A0 =A0 Float (float_of_string x)
;; =A0 =A0 =A0 =A0=A0

- Yury



On Fri, Jan 4, 2013 at 8:32 AM, Philippe Veber <philippe.veber@gmail.com><= /span> wrote:
Dear list,

Suppose I define a GADT for expressions:

type _ expr =3D
| Int : int -> int expr
| Float : float -> float expr

Now I want to write a parser, that will build an ['a expr] from a string. Without thinking much, I tried the following:

let parse_expr : type s. string -> s expr =3D fun x ->
=A0 try Int (int_of_string x)
=A0 with _ ->
=A0= =A0=A0 Float (float_of_string x)
;;

Which fails with the following error message:

Error: This expression has type int expr but an expression was expected of type s expr

That makes sense, since [s] is a locally abstract type. I tried a couple of variants and finally realised that I could not even write the type of [parse_expr]: it should be [string -> 'a expr] for some ['a], but I'm not sure that really mea= ns something.

So to put it simple, how does one construct a GADT value from a string ?

Cheers,
=A0 ph.





--f46d044469eff1bfaf04d279c369--