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 58E6C7EE94 for ; Sat, 5 Jan 2013 17:26:48 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=74.125.82.169; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 74.125.82.169 as permitted sender) identity=mailfrom; client-ip=74.125.82.169; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-f169.google.com) identity=helo; client-ip=74.125.82.169; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-we0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ak0CAPFS6FBKfVKpjWdsb2JhbABFhjm3GAgWDgEBAQEJCQsJEgYjgh4BAQQBIwQZARsdAQMBCwYFCw0CAiYCAiEBAREBBQEcBhOIBAEDCQaZWItkT4J7hB0KGScNWYYQAQUMgRaKRoQagRMDlDWBVos3gzEWKYQW X-IronPort-AV: E=Sophos;i="4.84,415,1355094000"; d="scan'208";a="188563196" Received: from mail-we0-f169.google.com ([74.125.82.169]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 05 Jan 2013 17:26:48 +0100 Received: by mail-we0-f169.google.com with SMTP id t49so8689442wey.14 for ; Sat, 05 Jan 2013 08:26:47 -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=9IB0TW1dvTH04sjB7dUt2PmtSxbn5Id6gMGUbkau6oA=; b=GU3JRiuhFgShyv2TsCfSRvWRrYimTn1YyYw7G9nrltNTk6CzgpyjWS7BqHAxsy0WEz 6JNCJidw56FRYI3B5KpSPLqM7OUmKc9EZr+r1S2tCVyFl9csGjwYzw/It2Wyjnh/SMNa O4qeidEQLZd7rroRBoLZMFp+8RKhwKH+axh9iHHyZhalEI5Sa4Dno/Esy4OFW+yI/Eyx z4QdBgwPzI+eFu2f19vcuduYyMZxtcqIIPckviyYbqkT09QkAkzzZ6LoPp12AlC4O5zH z7km86t/XmS8WyfwGRkvhTP8ufF7mBXoisQxQko0SxEzrrDPZAMNnImLrRTHe1RaOhhZ kxJg== MIME-Version: 1.0 Received: by 10.180.109.201 with SMTP id hu9mr2452950wib.32.1357403207689; Sat, 05 Jan 2013 08:26:47 -0800 (PST) Received: by 10.217.39.129 with HTTP; Sat, 5 Jan 2013 08:26:47 -0800 (PST) In-Reply-To: References: <50E701D3.9070008@free.fr> Date: Sat, 5 Jan 2013 16:26:47 +0000 Message-ID: From: Jeremy Yallop To: Philippe Veber Cc: Jeff Meister , Tiphaine Turpin , Caml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation 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)