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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id A2A557FCE0 for ; Wed, 1 Apr 2015 14:16:45 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of andre@digirati.com.br) identity=pra; client-ip=187.73.32.199; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of andre@digirati.com.br designates 187.73.32.199 as permitted sender) identity=mailfrom; client-ip=187.73.32.199; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="andre@digirati.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@mta123.f1.k8.com.br designates 187.73.32.199 as permitted sender) identity=helo; client-ip=187.73.32.199; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="postmaster@mta123.f1.k8.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C+AACj4BtVnMcgSbtcg1hcxVqFcwKBQEwBAQEBAQERAQEBAQEICwkJFC6EFQEFJxkBATYCDwsYCRYPCQMCAQIBDgsCASkGDAEIAQEXiBYLtAGFUgEFgWuSWAEBAQcCARkGiymEFhEBV4QtklSBMlSGCYcEZoxNAoIkHIFqVQGBCoE4AQEB X-IPAS-Result: A0C+AACj4BtVnMcgSbtcg1hcxVqFcwKBQEwBAQEBAQERAQEBAQEICwkJFC6EFQEFJxkBATYCDwsYCRYPCQMCAQIBDgsCASkGDAEIAQEXiBYLtAGFUgEFgWuSWAEBAQcCARkGiymEFhEBV4QtklSBMlSGCYcEZoxNAoIkHIFqVQGBCoE4AQEB X-IronPort-AV: E=Sophos;i="5.11,503,1422918000"; d="asc'?scan'208";a="107914676" Received: from mta123.f1.k8.com.br ([187.73.32.199]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 01 Apr 2015 14:16:43 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id 56D9B6108E for ; Wed, 1 Apr 2015 12:16:36 +0000 (UTC) X-Virus-Scanned: amavisd-new at k8.com.br Received: from smtpz.f1.k8.com.br ([127.0.0.1]) by localhost (mta123.f1.k8.com.br [127.0.0.1]) (amavisd-new, port 10024) with LMTP id isThtVEeEbhL for ; Wed, 1 Apr 2015 12:16:34 +0000 (UTC) Received: from [10.200.12.21] (unknown [201.76.188.234]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtpz.f1.k8.com.br (Postfix) with ESMTPSA id 5086560F7D for ; Wed, 1 Apr 2015 12:16:33 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br 5086560F7D DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1427890594; bh=4LMPDgeUVcJCgmAs2MNy3Dda4xeFMPqCug5s/SiFUtU=; h=Date:From:Reply-To:To:Subject:References:In-Reply-To; b=YEh4/jI06oKjWZvPtZqe6EU4A2YihDJg5NCnDXTtRDmfVkaZtPRX8R1aJMIJEsSa3 TTqczWC7iHwXrCYUueSONeCZT+r2AfZ3KcI30oLAvu2UUyuUYFWAhNbUYRh7wyAdZe D47hFHBKnuBqRK5N8UNPQgeAh93RdETE5a8GLFuY= Message-ID: <551BE19E.3010302@digirati.com.br> Date: Wed, 01 Apr 2015 09:16:30 -0300 From: Andre Nathan Reply-To: Andre Nathan User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0 MIME-Version: 1.0 To: caml users References: <551AE480.1000008@digirati.com.br> <20150331194531.GA12168@yquem.inria.fr> <551B067C.2030006@digirati.com.br> In-Reply-To: <551B067C.2030006@digirati.com.br> Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="v5xVH1BFxwCK4OfCiGq7pa7qPd4vIfOqG" Subject: Re: [Caml-list] GADTs and Menhir This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --v5xVH1BFxwCK4OfCiGq7pa7qPd4vIfOqG Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable On 03/31/2015 05:41 PM, Andre Nathan wrote: > Can you give me an example of what this "GADT of type representations" > would look like? I couldn't understand the Haskell example... I found a reference to an email from Jeremy Yallop to the list from 2013 [1], and managed to get it working with the following solution: (* foo.ml *) open Printf type 'a t =3D | Int : int -> int t | Bool : bool -> bool t type ast =3D [ `Int of int | `Bool of bool ] type any =3D | Any : 'a t -> any let typed =3D function | `Int i -> Any (Int i) | `Bool b -> Any (Bool b) let print : type a. a t -> unit =3D function | Int i -> printf "%d\n" i | Bool b -> printf "%b\n" b The parser now returns a `Foo.ast`: value: | i =3D INTEGER { `Int i } | b =3D BOOL { `Bool b } ; and with that I can print the parsed value with let ast =3D Parser.start Lexer.token lexbuf in let Foo.Any t =3D Foo.typed ast in Foo.print t I'm happy that it works, but the `any` type is a bit of a mistery to me. In Jeremy's email it's explained as "An existential to hide the type index of a well-typed AST, making it possible to write functions that return constructed ASTs whose type is not statically known." Does anyone have a reference to literature that explains this technique (I'm guessing that would be Pierce's book)? The OCaml manual briefly shows an example with a `dyn` type, but not much is said about it. Thanks, Andre [1] https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00013.html --v5xVH1BFxwCK4OfCiGq7pa7qPd4vIfOqG Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.22 (GNU/Linux) iQEcBAEBAgAGBQJVG+GhAAoJED4JW1qwFY2cvOgH/RcHWBv+a23Bg7vFkTAhd3lk 80A06DfIk2R+WPPESRDxbzRi3/t0eG3lUUh0z1F6RxmWH22Hzpc4xjNVVcVUQYK6 mYbkfHGhGzwr3JySIg+EI5FR3pnfw1NGjsadd1TUPGW3/4CdC5dYr87ZymYrn0pC x/X4ZSPNqnHZn/gygVRECIRb9KUWkiEnhR+dokAEnLrsJiIWGgBRT/0HbpwF2vFU 9PhWk89kOASrUwnAu2WCBdweCLJSBvaE0rcSUo5mGuZ1zwbSmQu3LKo5bI+XGN/2 qr/YWt3beUl0unIg3mUIhBdT1S+w25CCiu2tRUlZvi2ztgNRiegqTzqI+pYgzNY= =hCYt -----END PGP SIGNATURE----- --v5xVH1BFxwCK4OfCiGq7pa7qPd4vIfOqG--