From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 84C477EE94 for ; Fri, 4 Jan 2013 23:00:12 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nanaki@gmail.com) identity=pra; client-ip=209.85.212.41; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="nanaki@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of nanaki@gmail.com designates 209.85.212.41 as permitted sender) identity=mailfrom; client-ip=209.85.212.41; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="nanaki@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vb0-f41.google.com) identity=helo; client-ip=209.85.212.41; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="postmaster@mail-vb0-f41.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuoBAK5P51DRVdQpk2dsb2JhbABFuWGDZAgWDgEBAQEJCQsJFAQjgh4BAQQBJxkBGx0BAwELBgULDS4hAQERAQUBHAYTiAEBAwYDBgyYTIwzgnuEQQoZJwwBWYV9AQEEDItchS0DiGGLVIFWizeDMRYphDc X-IronPort-AV: E=Sophos;i="4.84,412,1355094000"; d="scan'208";a="188512613" Received: from mail-vb0-f41.google.com ([209.85.212.41]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2013 23:00:11 +0100 Received: by mail-vb0-f41.google.com with SMTP id l22so17169143vbn.28 for ; Fri, 04 Jan 2013 14:00:10 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=+JFZ1/MGSIB2R08qhiGpC1UvMUYo4WD0mOZn0bzAyRQ=; b=PPZj1UsciCe6GtAfeMHapmtJq/GzLki9Q+Iur9E20DSxqcImk8Yn6lCtsF66eJtXyl bFz+wkXhw7V7NVjRwt1cRJW3nA/opAT8YyglhhfDXrS7+acUbEEMC0Cgr6XaLTOjavog j1pC3WxxanPfEG6AIPxC33G0OfNUgrFv+DrGlI5hdOGf54lI+T8DlRlxgvLwb8R7Egr1 tXKJcj5iBqEyEpvGRbfyuAvRMpll23x7vbXPnlJPtEr4w8qXpskYZYbmHUf0fRE/0bkS Ub6+HbHenSE5R+DSolg+NjMoFBxz4ee+JuHlDsws2swS61H8F7JYNIkufM84vJRdQkBr EiaA== MIME-Version: 1.0 Received: by 10.221.2.69 with SMTP id nt5mr77782649vcb.68.1357336810420; Fri, 04 Jan 2013 14:00:10 -0800 (PST) Received: by 10.58.161.170 with HTTP; Fri, 4 Jan 2013 14:00:10 -0800 (PST) In-Reply-To: References: <50E701D3.9070008@free.fr> Date: Fri, 4 Jan 2013 14:00:10 -0800 Message-ID: From: Jeff Meister To: Philippe Veber Cc: Tiphaine Turpin , Caml List Content-Type: multipart/alternative; boundary=90e6ba211fbf6cfb2504d27d9a68 Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --90e6ba211fbf6cfb2504d27d9a68 Content-Type: text/plain; charset=ISO-8859-1 However, by using an existential type like that, you're losing the additional type checking benefits of GADTs. The return type of parse_expr is now any_expr, not 'a expr. You can write e.g. the function extract_int_value : int expr -> int, where OCaml knows you don't need to match the Float case, but you'll never have an int expr to pass to this function, at least not as a result of parsing. Anything handling a parsed any_expr must match the Expr case, which of course can have any expr inside. At this point, it seems like just a cumbersome way to write the traditional expr type. I went through basically this same thought process while trying to understand how I could apply the new OCaml GADT features, and I concluded that GADTs weren't providing any extra utility in the case where they must be constructed by parsing an input string. That's a shame since parsing and transformation is such a canonical use of OCaml, so I would love to be proven wrong here! On Fri, Jan 4, 2013 at 9:25 AM, Philippe Veber wrote: > 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. >>>> >>> >>> >> >> >> > --90e6ba211fbf6cfb2504d27d9a68 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
However, by using an existential type like that, you&= #39;re losing the additional type checking benefits of GADTs. The return ty= pe of parse_expr is now any_expr, not 'a expr. You can write e.g. the f= unction extract_int_value : int expr -> int, where OCaml knows you don&#= 39;t need to match the Float case, but you'll never have an int expr to= pass to this function, at least not as a result of parsing. Anything handl= ing a parsed any_expr must match the Expr case, which of course can have an= y expr inside. At this point, it seems like just a cumbersome way to write = the traditional expr type.

I went through basically this same thought process while trying t= o understand how I could apply the new OCaml GADT features, and I concluded= that GADTs weren't providing any extra utility in the case where they = must be constructed by parsing an input string. That's a shame since pa= rsing and transformation is such a canonical use of OCaml, so I would love = to be proven wrong here!


On Fri,= Jan 4, 2013 at 9:25 AM, Philippe Veber <philippe.veber@gmail.com> wrote:
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.






--90e6ba211fbf6cfb2504d27d9a68--