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 573777F2E5 for ; Tue, 8 Jan 2013 12:01:20 +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.223.170; 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.223.170 as permitted sender) identity=mailfrom; client-ip=209.85.223.170; 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-ie0-f170.google.com) identity=helo; client-ip=209.85.223.170; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-ie0-f170.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmgBACb761DRVd+qm2dsb2JhbABEvU4IFg4BAQEBAQgJCwkUJ4IeAQEEAScZARsdAQMBCwYFCw0uIQEBEQEFARwGE4gEAQMJBptkjDOBcYEKhH8KGScNWYV2AQUMi1yFLQOUNYFWizeDMRYphBc X-IronPort-AV: E=Sophos;i="4.84,430,1355094000"; d="scan'208";a="188892530" Received: from mail-ie0-f170.google.com ([209.85.223.170]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Jan 2013 12:01:19 +0100 Received: by mail-ie0-f170.google.com with SMTP id k10so302440iea.29 for ; Tue, 08 Jan 2013 03:01:18 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:mime-version:in-reply-to:references:from:date:message-id :subject:to:cc:content-type; bh=ZCMcn1yzykhAcKJKhqK2RpEFIyLiLZqW1wL8ESuEzb8=; b=0YKqiVNPUnYOE3ZDOIw28v/WbQru3q2IvTgDkvf1OrBcJz0v4lV9TMa/mbhTJKvLHR D1L8QySkt85ubD+fpThoOyUSxjICMgJQ4d/E38as8wLMsF9GozYdYbAjotz29lRIyHBq G5bGCBdsCTrpgagu8PJRHT1e8vnzCwnGoppaRcUMY/PS9zMo6/mlFkz/YvukwxtiS5E7 7ocfXC/fbhTpjjMHXpCdVKltsp1BJtH1kG0dX3rvHVzESC5w0Im0QCvMv11Ei2cUES6E ww1qG3vkiWUIWb5tFptG0K23QVUsjUh+nwW5GGI25dHwcYHTuPG99bJCtyP4Stx14kkK kQTA== X-Received: by 10.50.53.175 with SMTP id c15mr8410646igp.106.1357642878028; Tue, 08 Jan 2013 03:01:18 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.6.226 with HTTP; Tue, 8 Jan 2013 03:00:57 -0800 (PST) In-Reply-To: References: <50E701D3.9070008@free.fr> From: Philippe Veber Date: Tue, 8 Jan 2013 12:00:57 +0100 Message-ID: To: Jeremy Yallop Cc: Jeff Meister , Tiphaine Turpin , Caml List Content-Type: multipart/alternative; boundary=f46d04339b147a0aca04d2c4ddb4 X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation --f46d04339b147a0aca04d2c4ddb4 Content-Type: text/plain; charset=ISO-8859-1 Now it looks super nice! Thanks a lot Jeremy, your explanations were really helpful! ph. 2013/1/5 Jeremy Yallop > On 5 January 2013 13:40, Philippe Veber wrote: > > I still have a question though: what is the exact meaning of the _ > > character in the polymorphic type "< rn : 'a. int * 'a expr -> _>" > > and how is it useful/necessary for your example to run? > > It's analogous to '_' in patterns: a kind of anonymous type variable > that you can use to avoid giving a name to a type. (As with "_" in > patterns, there"s no connection between occurrences of "_", so "_ * > int -> _" means "'a * int -> 'b", not "'a * int -> 'a", for example.) > > It's not doing anything special here: you could equally give a name to > the type without changing the meaning of the code. > > > Could your example be written without a record/object type using > > polymorphic type annotations for functions? > > I don't believe it's possible to make function arguments polymorphic > using annotations. However, the code can be significantly simplified > to remove that bit of polymorphism altogether. As written it mixes > two techniques for hiding the type index in the expression GADT during > parsing: CPS (in the inner 'parse' function) and an existential type > (in the return type of 'parse_expr'). In fact, either of these > approaches in isolation is sufficient. Here's a more direct > implementation using only the existential: > > (* Well-typed parser. Incomplete -- it doesn't handle fst and snd -- and a > bit careless about error-checking. Perhaps sufficient to give a > flavour. > *) > let parse_expr : string -> any_expr = > let rec parse s pos = > match s.[pos] with > | 'T' -> pos + 1, Expr True > | 'F' -> pos + 1, Expr False > | '!' -> let pos', Expr e = parse s (pos + 1) in > (* Check that 'e' has boolean type before we can parse it to > Not. This is more than just good practice: without the > type-checking step the parser won't compile. *) > begin match type_of e with > | TBool -> pos', Expr (Not e) > | t -> typing_failure (pos + 1) pos' s TBool t > end > | '(' -> let pos, Expr l = parse s (pos + 1) in > if s.[pos] <> ',' then parsing_failure pos ',' s else > let pos, Expr r = parse s (pos + 1) in > if s.[pos] <> ')' then parsing_failure pos ')' s else > pos + 1, Expr (Pair (l, r)) > in > fun s -> snd (parse s 0) > --f46d04339b147a0aca04d2c4ddb4 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Now it looks super nice!
Thanks a lot Jeremy, your explanations were rea= lly helpful!
ph.

2013/1/5 Jeremy Yallo= p <yallop@gmail.com>
On 5 January 2013 13:40, P= hilippe Veber <philippe.vebe= r@gmail.com> wrote:
> I still have a question though: what is the exact meaning of the _
> character in the polymorphic type "< rn : 'a. int * 'a= expr -> _>"
> and how is it useful/necessary for your example to run?

It's analogous to '_' in patterns: a kind of anonymous ty= pe variable
that you can use to avoid giving a name to a type. =A0(As with "_"= ; in
patterns, there"s no connection between occurrences of "_", = so "_ *
int -> _" means "'a * int -> 'b", not "&#= 39;a * int -> 'a", for example.)

It's not doing anything special here: you could equally give a name to<= br> the type without changing the meaning of the code.

> Could your example be written without a record/object type using
> polymorphic type annotations for functions?

I don't believe it's possible to make function arguments poly= morphic
using annotations. =A0However, the code can be significantly simplified
to remove that bit of polymorphism altogether. =A0As written it mixes
two techniques for hiding the type index in the expression GADT during
parsing: CPS (in the inner 'parse' function) and an existential typ= e
(in the return type of 'parse_expr'). =A0In fact, either of these approaches in isolation is sufficient. =A0Here's a more direct
implementation using only the existential:

(* Well-typed parser. =A0Incomplete -- it doesn't handle fst and snd --= and a
=A0 =A0bit careless about error-checking. =A0Perhaps suff= icient to give a flavour.
*)
let parse_expr : string -> any_expr =3D
=A0 let rec parse s pos =3D
=A0 =A0 match s.[pos] with
=A0 =A0 =A0 | 'T' -> pos + 1, Expr True
=A0 =A0 =A0 | 'F' -> pos + 1, Expr False
=A0 =A0 =A0 | '!' -> let pos', Expr e =3D parse s (pos + 1) = in
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0(* Check that 'e' = has boolean type before we can parse it to
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 Not. =A0This is more than just good pra= ctice: without the
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 type-checking step the parser won't= compile. *)
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0begin match type_of e with
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0| TBool -> pos', Expr (Not e)
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0| t -> typing_failu= re (pos + 1) pos' s TBool t
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0end
=A0 =A0 =A0 | '(' -> let pos, Expr l =3D parse s (pos + 1)= in
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0if s.[pos] <> ',= ' then parsing_failure pos ',' s else
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0let pos, Expr r =3D parse s (pos += 1) in
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0if s.[pos] <> &#= 39;)' then parsing_failure pos ')' s else
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0pos + 1, Expr (Pair (l, r))
=A0 in
=A0 fun s -> snd (parse s 0)

--f46d04339b147a0aca04d2c4ddb4--