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 A59987EE94 for ; Fri, 4 Jan 2013 14:33:20 +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.223.175; 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.223.175 as permitted sender) identity=mailfrom; client-ip=209.85.223.175; 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-ie0-f175.google.com) identity=helo; client-ip=209.85.223.175; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-ie0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYBAKPZ5lDRVd+vm2dsb2JhbABFvUUIFg4BAQEBAQgJCwkUJ4JMGQEbHgMSCQddAREBBQEiG4d5AQMPlleCbYwzgnuESgoZJw1ZhgQBBQyRCQOWC45oFimEFw X-IronPort-AV: E=Sophos;i="4.84,409,1355094000"; d="scan'208";a="167434938" Received: from mail-ie0-f175.google.com ([209.85.223.175]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jan 2013 14:32:51 +0100 Received: by mail-ie0-f175.google.com with SMTP id qd14so19316318ieb.6 for ; Fri, 04 Jan 2013 05:32:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=J9Gt/aI3PqJfEAt38yeYSgqBsImKCxIWTSk03rCJVbg=; b=lSOmpeF+SqKC777uNEJFdHsL+ztX+HBwBwFaf1fYVA3fpgwQhQtAvRmLg7UNOeZLOd HAnyOAE+Yov5cOJv+Bg8vutCUqFlnXlhUrB17vsPsqN1MtwIS/QT9qw2kIazM40RmhPS oDbBXsGY+n+sM45gPw2FpFC8p3lGm8LgwpabfGc7KW7xjStvuInZIj0nqXrRo16HCrzi pbuqfSZLByKjRyyL9ivub1r0nDaQfK9lGRLJTZLLH7unBeWhI0sjOy2rU87AJXhwbLX1 +HezqXCWTFPFBTEuYJHdcqOd9fOj4/ah7KTOKGXkmBBxvOVyMBCWpWE3qqhYaAM5OSz8 KIpA== Received: by 10.50.170.66 with SMTP id ak2mr46026924igc.38.1357306370443; Fri, 04 Jan 2013 05:32:50 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.6.226 with HTTP; Fri, 4 Jan 2013 05:32:30 -0800 (PST) From: Philippe Veber Date: Fri, 4 Jan 2013 14:32:30 +0100 Message-ID: To: caml users Content-Type: multipart/alternative; boundary=e89a8f2351a90fc98b04d2768455 X-Validation-by: philippe.veber@gmail.com Subject: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --e89a8f2351a90fc98b04d2768455 Content-Type: text/plain; charset=ISO-8859-1 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. --e89a8f2351a90fc98b04d2768455 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Dear list,

Suppose I define a GADT for expressions:

type _ expr =3D
| Int : int -> int expr
| 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.
--e89a8f2351a90fc98b04d2768455--