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 F275F7FCE0 for ; Tue, 31 Mar 2015 22:41:46 +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.186; 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.186 as permitted sender) identity=mailfrom; client-ip=187.73.32.186; 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@mta114.f1.k8.com.br designates 187.73.32.186 as permitted sender) identity=helo; client-ip=187.73.32.186; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="andre@digirati.com.br"; x-sender="postmaster@mta114.f1.k8.com.br"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ArAQC6BRtVnLogSbtchDTLdgKBREwBAQEBAQERAQEBAQEICwkJFC6EFAEBAQMBJxkBATYBAQQLCxgJFg8JAwIBAgEOCwIBKRIBAQcBAYgjCrQYhVIBBZQiAQEBAQYCGgaLKYR4BxaEF45Yg3uBMoZcgRiFbGaJBINGAoQqVYJDAQEB X-IPAS-Result: A0ArAQC6BRtVnLogSbtchDTLdgKBREwBAQEBAQERAQEBAQEICwkJFC6EFAEBAQMBJxkBATYBAQQLCxgJFg8JAwIBAgEOCwIBKRIBAQcBAYgjCrQYhVIBBZQiAQEBAQYCGgaLKYR4BxaEF45Yg3uBMoZcgRiFbGaJBINGAoQqVYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,503,1422918000"; d="asc'?scan'208";a="107833840" Received: from mta114.f1.k8.com.br ([187.73.32.186]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 31 Mar 2015 22:41:42 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id 8E577209F0; Tue, 31 Mar 2015 20:41:37 +0000 (UTC) X-Virus-Scanned: amavisd-new at k8.com.br Received: from smtpz.f1.k8.com.br ([127.0.0.1]) by localhost (mta114.f1.k8.com.br [127.0.0.1]) (amavisd-new, port 10024) with LMTP id SmhMBw+R598D; Tue, 31 Mar 2015 20:41:36 +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 8A6A820A19; Tue, 31 Mar 2015 20:41:36 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br 8A6A820A19 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1427834496; bh=DEfV20TyL4PiTuoFDaa12d0d3IYiAUnnDIKqdVfvISU=; h=Date:From:To:CC:Subject:References:In-Reply-To; b=iqyjuRiHFDa1g/Uy9LwMWhRswiac6XdQmkjg6C+bjiK6bLmQdAkkA+9vUApsOjM4g JsueEIYOgZ9gylgICRe33wgBDd4IdYRi6SlgbVcpysckbf1ES3ZumPlVQCk8aNYEb6 1px5sEvxoUtjuBgI93WAG4YECmb/T0A4XQ4+4alU= Message-ID: <551B067C.2030006@digirati.com.br> Date: Tue, 31 Mar 2015 17:41:32 -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: Francois.Pottier@inria.fr CC: caml users References: <551AE480.1000008@digirati.com.br> <20150331194531.GA12168@yquem.inria.fr> In-Reply-To: <20150331194531.GA12168@yquem.inria.fr> Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="tSOJtqkScJR0DVwgex4Ogl2RuhXuRU2p1" Subject: Re: [Caml-list] GADTs and Menhir This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --tSOJtqkScJR0DVwgex4Ogl2RuhXuRU2p1 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable On 03/31/2015 04:45 PM, Francois Pottier wrote: > The problem lies here. What is the OCaml type of the symbol "value"? I see now. > 2- perform type-checking (or type inference). > If you insist on using GADTs, you will probably need > a GADT of terms (your type 'a Foo.t) and > a GADT of type representations ('a ty) > and the type-checking function will have type > ast -> 'a ty -> 'a Foo.t option > which means that, given an untyped term and > a representation of an expected type, it > either fails or succeeds and produces a typed term. Can you give me an example of what this "GADT of type representations" would look like? I couldn't understand the Haskell example... Thanks, Andre --tSOJtqkScJR0DVwgex4Ogl2RuhXuRU2p1 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) iQEcBAEBAgAGBQJVGwZ/AAoJED4JW1qwFY2cqe8H/RZFbNtSYxQeh8/J5tmhCCXF V5JKLJmoB28vp16QSLEh+5S5eYwBCtWuCQ0mZAW31Qm6wx8WimjeTRI9m/avuSHu e8WE15WO78HHbApsiDC+JJ4HsfpnaVcXncam0aKP08FvDfmR8Gg6kMyDh8As0k2+ 5HvjxvBttvyr+QEYegb4du7HrMyzqA/XR2sDPlRor753Eob+lpgQ/EFyZjLQ5vA0 EL1wag+WHzlu4uvEyW5U0EPDVXryn++PA6STTR3ZhHL9bsM77NSlPq8T19gyTYOv MZ3V7uL7v1U9CmZ0Jt2u+yTp7GP2TqCymSJXSfVTtAJdsbgWihBfuUoOHgxch08= =RmG8 -----END PGP SIGNATURE----- --tSOJtqkScJR0DVwgex4Ogl2RuhXuRU2p1--