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 BCF9A7EE94 for ; Fri, 4 Jan 2013 15:54:04 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yury.sulsky@gmail.com) identity=pra; client-ip=74.125.82.171; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yury.sulsky@gmail.com"; x-sender="yury.sulsky@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of yury.sulsky@gmail.com designates 74.125.82.171 as permitted sender) identity=mailfrom; client-ip=74.125.82.171; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yury.sulsky@gmail.com"; x-sender="yury.sulsky@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-we0-f171.google.com) identity=helo; client-ip=74.125.82.171; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yury.sulsky@gmail.com"; x-sender="postmaster@mail-we0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AukBAIrs5lBKfVKrjWdsb2JhbABFvUQIFg4BAQEBCQkLCRIGI4IeAQEEAScZARsdAQMBCwYFBAc7IQEBEQEFARwGEwiHeQEDCQaZVowzgnuERwoZJw1ZhV4BBQyLXIUtA4hhi1SBVos3gzEWKYQ0 X-IronPort-AV: E=Sophos;i="4.84,409,1355094000"; d="scan'208";a="188477381" Received: from mail-we0-f171.google.com ([74.125.82.171]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2013 15:54:04 +0100 Received: by mail-we0-f171.google.com with SMTP id u3so7586925wey.2 for ; Fri, 04 Jan 2013 06:54:04 -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=D1IcJlcQRZXsuHJpVvpSLwvUduG3VqgPomkHJXulHV4=; b=cY8ydgdIfvn0sETwCmPZ75CD0Z/cgXTUh2Lymijf5BLncMFpgIhNPaW/y37Fc9XNg/ EjpORZKXZCsctEsHI49YTLFB64FCzLYgMoEHehS7g+qShkexJBKw0dAZTRhyrCAF2GZU INd/IGBhPB8XWUqH4WjHVL/Uy1dJ/mXhrwbFK9lfe2+/pcy3MlPatE+XbenfWwO0Ubkv TSjLyeBGtAlFctDopiRx9OigCl5AKOV9p8+MVnXI7FtsJgN+LTOMIJ0M5Fx7dQ3rzrXE kVoN5drVyWLgk97x7hkfHpc/B3oViwAcmyslcuvpA9yzB/BrDby70+j3fjqsTqCnrYIj cY3A== MIME-Version: 1.0 Received: by 10.180.75.135 with SMTP id c7mr82071394wiw.10.1357311243943; Fri, 04 Jan 2013 06:54:03 -0800 (PST) Received: by 10.216.240.198 with HTTP; Fri, 4 Jan 2013 06:54:03 -0800 (PST) In-Reply-To: References: Date: Fri, 4 Jan 2013 09:54:03 -0500 Message-ID: From: Yury Sulsky To: Philippe Veber Cc: caml users Content-Type: multipart/alternative; boundary=f46d043be2408b7cd604d277a63c Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --f46d043be2408b7cd604d277a63c Content-Type: text/plain; charset=ISO-8859-1 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. > --f46d043be2408b7cd604d277a63c Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hi Philippe,

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

type _ expr =3D
| Int : int -> [> `int ] expr<= /div>
| 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> w= rote:
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.

--f46d043be2408b7cd604d277a63c--