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 754847FCE0 for ; Wed, 1 Apr 2015 15:16:56 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=pra; client-ip=212.227.17.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=mailfrom; client-ip=212.227.17.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.kundenserver.de) identity=helo; client-ip=212.227.17.10; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="postmaster@mout.kundenserver.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C+AACx7htVnAoR49Rcg1hcxVAKhXMCgT5MAQEBAQEBEQEBAQEBBg0JCRQuhBUBBAEnLiQFCwtGVwYTCYgeDAnOOgEBAQEBAQEBAQEBAQEBAR2LKYQWEQEqJgeCLQxBgTMFhh2LEQGDJoYEgR2FaQOJbYNIgiQcgVJtAYEKgTgBAQE X-IPAS-Result: A0C+AACx7htVnAoR49Rcg1hcxVAKhXMCgT5MAQEBAQEBEQEBAQEBBg0JCRQuhBUBBAEnLiQFCwtGVwYTCYgeDAnOOgEBAQEBAQEBAQEBAQEBAR2LKYQWEQEqJgeCLQxBgTMFhh2LEQGDJoYEgR2FaQOJbYNIgiQcgVJtAYEKgTgBAQE X-IronPort-AV: E=Sophos;i="5.11,503,1422918000"; d="asc'?scan'208";a="107924335" Received: from mout.kundenserver.de ([212.227.17.10]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 01 Apr 2015 15:16:50 +0200 Received: from office1.lan.sumadev.de ([188.107.29.5]) by mrelayeu.kundenserver.de (mreue103) with ESMTPSA (Nemesis) id 0Lr4bL-1Z799f2N9P-00eafS; Wed, 01 Apr 2015 15:16:48 +0200 Received: from [192.168.65.10] (unknown [192.168.65.10]) by office1.lan.sumadev.de (Postfix) with ESMTPSA id 58780DC05D; Wed, 1 Apr 2015 15:16:46 +0200 (CEST) Message-ID: <1427894198.16182.68.camel@e130.lan.sumadev.de> From: Gerd Stolpmann To: Andre Nathan Cc: caml users Date: Wed, 01 Apr 2015 15:16:38 +0200 In-Reply-To: <551BE19E.3010302@digirati.com.br> References: <551AE480.1000008@digirati.com.br> <20150331194531.GA12168@yquem.inria.fr> <551B067C.2030006@digirati.com.br> <551BE19E.3010302@digirati.com.br> Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="=-xv2J+pia/IuGch1bvW6F" X-Mailer: Evolution 3.10.4-0ubuntu2 Mime-Version: 1.0 X-Provags-ID: V03:K0:d07pND+IRiDxRNjC5D2pk3d0KXsUD9XNcg4JMiyghgnFYdocExt I9kRtD0fFNq7ovTzytos8YhNucuk9cE2vXmae1ZqAziPm2EBi/OUAMveMRPfoXM7QepFIW6 IBb7d/vKgTaTn767ngySA8OmUiBVc0LXfI7/wUE3oUkqYzFIQAFAx50WkdLjf1RySqEiaut UyzOjgWtk8BJxRKN55qMw== X-UI-Out-Filterresults: notjunk:1; Subject: Re: [Caml-list] GADTs and Menhir --=-xv2J+pia/IuGch1bvW6F Content-Type: text/plain; charset="ISO-8859-15" Content-Transfer-Encoding: quoted-printable Am Mittwoch, den 01.04.2015, 09:16 -0300 schrieb Andre Nathan: > type 'a t =3D > | Int : int -> int t > | Bool : bool -> bool t >=20 > type ast =3D > [ `Int of int > | `Bool of bool > ] >=20 > type any =3D > | Any : 'a t -> any ... > 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 >=20 > "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." A couple of weeks ago I ran into the same problem. It is just a matter of not being accustomed to how GADTs work, and not having the right design patterns in your mind. OCaml users are used to expose any polymorphism and that it is not directly possible to hide it. So, normally if there is a variable 'a on the right side of the type definition, it must also appear on the left side (e.g. type 'a foo =3D Case1 of 'a | Case2 of ...). This is not required for GADTs, because the variable is bound by the case it applies to (i.e. for the Int case you have 'a=3Dint and for the Bool case you have 'a=3Dbool). So it is implicitly known. Because of this, many people prefer to write type _ t =3D (* look here, no 'a anymore *) | Int : int -> int t | Bool : bool -> bool t and=20 type any =3D | Any : _ t -> any The type parameter still exists because t is still polymorphic, but you cannot do anything with it unless you match against the cases. Now, "any" goes a step further, and even discards this parameter. It's a matter of perspective: if 'a is case-dependent but not dependent to anything outside t, you can also consider t as monomorphic. In other words: Knowing all cases binds 'a.=20 You need Any if you want to put several t values into a container, e.g. Does not work: [ Int 34; Bool true ] Does work: [ Any(Int 34); Any(Bool true) ] This nice thing with GADTs is that you can "undo" this change of perspective by matching against the cases: let print =3D ... (* as you defined it *) let print_any (Any x) =3D print x let () =3D List.iter print_any [ Any(Int 34); Any(Bool true) ] Gerd > 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. >=20 > Thanks, > Andre >=20 > [1] https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00013.html >=20 --=20 ------------------------------------------------------------ Gerd Stolpmann, Darmstadt, Germany gerd@gerd-stolpmann.de My OCaml site: http://www.camlcity.org Contact details: http://www.camlcity.org/contact.html Company homepage: http://www.gerd-stolpmann.de ------------------------------------------------------------ --=-xv2J+pia/IuGch1bvW6F Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iQEcBAABAgAGBQJVG++2AAoJEAaM4b9ZLB5TzqMH/2H5WE2H6XFB7i7pl0YmYBKm 905Ep7PLLhI73N2To7hsKJteqkHgJz0o14ACtBpIw+I+IudCyepvdP6fAPiReY2D TTtvUdLhW6vQ6mG0sZqq/aOlZjUkJjPTYmAqQ8mPhJCxE1FbtdWzqnFr9rJ1I24Y oNtQkCtfTTE/rFKvGetZTy8GBkFh49R17zfLk4zxTHwNsejnjlt3ke79s0Rk0q/y dwfAOOki1ZYeIwKNZlipjUgJUEJAfyTx+yefVe0+Zx98QJneWcDv360TRpXFTYJ6 bO0AnjOjGugXRP2lIhrRbPVLReJzVjerHwW2T+Fie4brCCb7lcxrMWHYaDjs6aY= =bDWw -----END PGP SIGNATURE----- --=-xv2J+pia/IuGch1bvW6F--