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 6D6277FCE0 for ; Wed, 1 Apr 2015 20:12:34 +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: A0C5AAAUNBxVnMcgSbtchDTLVAKBR0wBAQEBAQERAQEBAQEICwkJFC6EFQEFJxkBATYBAQ8LDgoJFg8JAwIBAgEOCwIBKQYMAQEHAQGILbR3hVIBBZQhAQEBAQEFAQEBAQEXBosphHkHhC2SVIEyhl2HBWaMTgKEKlWCQwEBAQ X-IPAS-Result: A0C5AAAUNBxVnMcgSbtchDTLVAKBR0wBAQEBAQERAQEBAQEICwkJFC6EFQEFJxkBATYBAQ8LDgoJFg8JAwIBAgEOCwIBKQYMAQEHAQGILbR3hVIBBZQhAQEBAQEFAQEBAQEXBosphHkHhC2SVIEyhl2HBWaMTgKEKlWCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,505,1422918000"; d="asc'?scan'208";a="107959808" 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 20:12:32 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id 7DAB4614A0; Wed, 1 Apr 2015 18:12:26 +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 vTZpLgPORHgv; Wed, 1 Apr 2015 18:12:25 +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 ED04D614BE; Wed, 1 Apr 2015 18:12:24 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br ED04D614BE DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1427911945; bh=bbTGykUvHL1w49vQvx5BFEOlafycJJHros0GLcVJ++U=; h=Date:From:To:CC:Subject:References:In-Reply-To; b=e9i/EvBERQfY65gRQ6F+2sdIrNETcanch92D5Z6wlLLQBd43XKFHWAAhLs8KiTkoK OkwGN8zIsOgL7kF8fmA6LBLY2QjTlsgKaGpyTYUMWIkS6LxmePVnbU92cRcoY8xFdN Ajn3yHXCPaAmkDYCZuNYbYhPrZiQuFuLjSA6d+Lg= Message-ID: <551C3504.6050209@digirati.com.br> Date: Wed, 01 Apr 2015 15:12:20 -0300 From: 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: Gerd Stolpmann CC: caml users References: <551AE480.1000008@digirati.com.br> <20150331194531.GA12168@yquem.inria.fr> <551B067C.2030006@digirati.com.br> <551BE19E.3010302@digirati.com.br> <1427894198.16182.68.camel@e130.lan.sumadev.de> In-Reply-To: <1427894198.16182.68.camel@e130.lan.sumadev.de> Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="uj6CgMiKgUac0r0NvlVfSiCqQkE1ngb9l" Subject: Re: [Caml-list] GADTs and Menhir This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --uj6CgMiKgUac0r0NvlVfSiCqQkE1ngb9l Content-Type: text/plain; charset=iso-8859-15 Content-Transfer-Encoding: quoted-printable Hi Gerd On 04/01/2015 10:16 AM, Gerd Stolpmann wrote: > You need Any if you want to put several t values into a container, e.g. >=20 > Does not work: [ Int 34; Bool true ] > Does work: [ Any(Int 34); Any(Bool true) ] >=20 > This nice thing with GADTs is that you can "undo" this change of > perspective by matching against the cases: But is there any way to, say, write some sort of lookup function for values in such containers? Eg. given an eval function, this doesn't work: let rec find k l =3D match l with | [] -> raise Not_found | (k', v)::rest -> if k =3D k' then v else find k rest let foo () =3D let dict =3D ["int", Any (Int 1); "bool", Any (Bool true)] in let Any x =3D find "int" dict in eval x ^^^^^^ Error: This expression has type a#0 but an expression was expected of type a#0 The type constructor a#0 would escape its scope I don't understand why `eval` can be written but it's result cannot be returned from another function. I tried introducing a type variable but it still doesn't work let foo (type a) () : a =3D let dict =3D ["x", Any (Int 1); "y", Any (Bool true)] in let Any (x : a t) =3D find "x" dict in eval x ^^^^^^^^^ Error: This pattern matches values of type a t but a pattern was expected which matches values of type a#0 t Type a is not compatible with type a#0 Thanks, Andre --uj6CgMiKgUac0r0NvlVfSiCqQkE1ngb9l 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) iQEcBAEBAgAGBQJVHDUHAAoJED4JW1qwFY2cyRYH/RY7Mmh4/ozd+lf1uAbLUoQ4 Kgafza4NPPdExm5zzeZMKg0kJSiRbskvgFlkzBQcV7Tq2+Wqkdp6wu9MFyVL4NQG Zf4Ww7heQs+nDluJx0J4a1zIFydzyrYz8iGFK/qcfoqtN7/G2dhVXa96Ul8XP9Wl 5ZezgNwcUAtnBGjw/Q63CLKreuuI5x7FLUrJLuIif055fhup7oZdxnJDdTp68PAz vh3Br3wM7FVxAoeVYzaNm4U/ajYm1JuXZMibvV9p6hZ3xnMcMKPb6J++u2rx85dS ApH0Ouyeh30V0vzdkSAjqKbmvgQ/tIqdk6btogHpeC8LaxNzE6gjKPfkORvqOh0= =MHbg -----END PGP SIGNATURE----- --uj6CgMiKgUac0r0NvlVfSiCqQkE1ngb9l--