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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id F08677EE94 for ; Fri, 4 Jan 2013 16:05:58 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.210.172; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.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=mail1-smtp-roc.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 (mail1-smtp-roc.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=mail1-smtp-roc.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: AqYBACLv5lDRVdKsm2dsb2JhbABFvUQIFg4BAQEBAQgJCwkUJ4IeAQEEAScZARsdAQMBCwYFCzshAQERAQUBHAYTiAEBAwkGmVyMM4J7hEkKGScNWYVeAQUMi1yFLQOUNYFWizeDMRYphBc X-IronPort-AV: E=Sophos;i="4.84,411,1355094000"; d="scan'208";a="188479110" Received: from mail-ia0-f172.google.com ([209.85.210.172]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2013 16:05:58 +0100 Received: by mail-ia0-f172.google.com with SMTP id z13so13960666iaz.3 for ; Fri, 04 Jan 2013 07:05:56 -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=/5TpEfi8djkEqCQhsV4hRSZM8ROhW9a2V5Lk8iVVLXM=; b=yuU+zxGbzGryDToddcEzBRFZkj3OUtEojmbbnkUWsipuaERbgohPhSsCg5fdiUYyMs Vu1USHpBKY8OO9t7QRMGDM7NtM32SFO8c9SljwrU6OK1LR0FpyeSViMDXPcn33zBY4Mq yj1XUWTKBU2I8n5C/YUZCnEGdTCV7tdLQceek4gOHD+8efwFF5UZ8FdJ9h4BpW/RnIKQ xSqQ0xEr1raWXbSgwyhfIjWG5JgFueJx+EZxgbYw+ITSCnSk4iHoSZSObh39bVeBOQUr kk0mgGpA764b8mJpa5hwlcvxac15nBM81mQqMAwj33AB9gpKQN42gcENAESG7Mg75Myk Ns8g== Received: by 10.50.91.230 with SMTP id ch6mr41028237igb.92.1357311956765; Fri, 04 Jan 2013 07:05:56 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.6.226 with HTTP; Fri, 4 Jan 2013 07:05:36 -0800 (PST) In-Reply-To: References: From: Philippe Veber Date: Fri, 4 Jan 2013 16:05:36 +0100 Message-ID: To: Yury Sulsky Cc: caml users Content-Type: multipart/alternative; boundary=e89a8f3ba0a1084a9404d277d1ca X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --e89a8f3ba0a1084a9404d277d1ca Content-Type: text/plain; charset=ISO-8859-1 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. >> > > --e89a8f3ba0a1084a9404d277d1ca Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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 li= ke to have an 'a expr such that 'a is the type of the value obtaine= d when evaluating the expression. With the polymorphic variants, I cannot w= rite an eval function of type 'a eval -> 'a, which is the main m= otivation behind using GADT in that (canonical) case. Sorry for ommiting th= is point!

ph.


2013/1/4 Yury Sulsky <yu= ry.sulsky@gmail.com>
Hi Philippe,

I think you can do this by= using a polymorphic variant as the type variable:
<= div>
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

<= div class=3D"h5">


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

Suppose I define a GADT fo= r expressions:

typ= e _ expr =3D
| Int : int -> int exp= r
| Float : float -> flo= at expr

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

let parse_expr : type= s. string -> s expr =3D fun x ->
=A0 t= ry Int (int_of_string x)
=A0 with _ -> <= br style=3D"font-family:courier new,monospace">=A0=A0=A0 Float (float_of_string x)
;;
<= br>Which fails with the following error message:

Error: This expressio= n 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 coup= le 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], b= ut I'm not sure that really means something.

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

Cheers,
=A0 ph.


--e89a8f3ba0a1084a9404d277d1ca--