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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id D7FD37EE94 for ; Fri, 4 Jan 2013 16:26:15 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Tiphaine.Turpin@free.fr) identity=pra; client-ip=212.27.42.1; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="Tiphaine.Turpin@free.fr"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Tiphaine.Turpin@free.fr) identity=mailfrom; client-ip=212.27.42.1; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="Tiphaine.Turpin@free.fr"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp1-g21.free.fr) identity=helo; client-ip=212.27.42.1; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="Tiphaine.Turpin@free.fr"; x-sender="postmaster@smtp1-g21.free.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AioBAAj05lDUGyoBlGdsb2JhbABFjBexNhYOAQEBAQkLCQkUAySCHgEBBScsJRELGAkWCAcJAwIBAgEPJRETBgIBAYd9AQMTCK1BCUENhjkEi2iFLQOUNYFWhWuFTIgH X-IronPort-AV: E=Sophos;i="4.84,411,1355094000"; d="scan'208,217";a="167444292" Received: from smtp1-g21.free.fr ([212.27.42.1]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Jan 2013 16:26:14 +0100 Received: from [192.168.0.1] (bur91-2-82-231-161-160.fbx.proxad.net [82.231.161.160]) (Authenticated sender: tiphaine.turpin) by smtp1-g21.free.fr (Postfix) with ESMTPA id 41FEE940217 for ; Fri, 4 Jan 2013 16:26:10 +0100 (CET) Message-ID: <50E701D3.9070008@free.fr> Date: Fri, 04 Jan 2013 17:22:43 +0100 From: Tiphaine Turpin User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.3) Gecko/20120501 Thunderbird/10.0.3 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: Content-Type: multipart/alternative; boundary="------------070700080002050304030105" Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation This is a multi-part message in MIME format. --------------070700080002050304030105 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit 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. > > > --------------070700080002050304030105 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit 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 <yury.sulsky@gmail.com>
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 <philippe.veber@gmail.com> 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.




--------------070700080002050304030105--