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 86C947FCE0 for ; Tue, 31 Mar 2015 20:16: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.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: A0C2AACE4xpVnMcgSbtcg1hcgxTCYwKHQUwBAQEBAQERAQEBAQEICwkJFC6EPgQZAQE2AjsWCwILAwIBAgEOCwIBLwwBCAEBiC20CHCEYgEFlE8GklUMLxKBM5JTgTJUhgiHBGaMSgKBZwyCN1WCQwEBAQ X-IPAS-Result: A0C2AACE4xpVnMcgSbtcg1hcgxTCYwKHQUwBAQEBAQERAQEBAQEICwkJFC6EPgQZAQE2AjsWCwILAwIBAgEOCwIBLwwBCAEBiC20CHCEYgEFlE8GklUMLxKBM5JTgTJUhgiHBGaMSgKBZwyCN1WCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,502,1422918000"; d="asc'?scan'208";a="107823861" Received: from mta123.f1.k8.com.br ([187.73.32.199]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 31 Mar 2015 20:16:45 +0200 Received: from localhost (localhost [127.0.0.1]) by smtpz.f1.k8.com.br (Postfix) with ESMTP id 7BCF3611FF for ; Tue, 31 Mar 2015 18:16:40 +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 NiYu4szBfT7h for ; Tue, 31 Mar 2015 18:16:38 +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 E762C6142C for ; Tue, 31 Mar 2015 18:16:37 +0000 (UTC) X-DKIM: OpenDKIM Filter v2.6.8 smtpz.f1.k8.com.br E762C6142C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=digirati.com.br; s=default; t=1427825798; bh=qAAmMhPolq2Du5OnYyUfVGWhQ7YbZEb92ErKQ1HirFI=; h=Date:From:To:Subject; b=ilLNRulcgnVd3/8o8siOJd6i4fzlBBkCFv3hgN8Lm6oo+8FMXc9xNskYVlM0gleJJ cr1kip0OU+qohz38uvtvD/ZspSb9SqsnElo/sIxgvpkpCLkQfq2ldfGIUQwxDSCk5F ulXFkPT4GCPOxqeW7R/dYWYPly4OX1TIC/BCx9cs= Message-ID: <551AE480.1000008@digirati.com.br> Date: Tue, 31 Mar 2015 15:16: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: caml users Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="Lg1RXtQ7MIwSpuFJkmdILFwcCVtn064aA" Subject: [Caml-list] GADTs and Menhir This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --Lg1RXtQ7MIwSpuFJkmdILFwcCVtn064aA Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Hello I'm trying to learn a bit about GADTs, but I can't figure out how to make them work with Menhir. I have defined the following GADT: (* foo.ml *) type 'a t =3D | Int : int -> int t | Bool : bool -> bool t With this definition I can write an "eval" function as let eval (type t) (foo : t Foo.t) : t =3D match foo with | Foo.Int i -> i | Foo.Bool b -> b Now considering the simple parser and lexer below, (* parser.mly *) %{ open Foo %} %token INTEGER %token BOOL %token EOF %start <'a Foo.t> start %% start: | value; EOF { $1 } ; value: | i =3D INTEGER { Int i } | b =3D BOOL { Bool b } ; (* lexer.mll *) { open Parser } let digit =3D ['0'-'9'] let boolean =3D "true" | "false" rule token =3D parse | [' ' '\t'] { token lexbuf } | '\n' { Lexing.new_line lexbuf; token lexbuf } | digit+ as i { INTEGER (int_of_string i) } | boolean as b { BOOL (bool_of_string b) } | eof { EOF } when I try to compile this I get the error below: File "parser.mly", line 15, characters 43-52: Error: This expression has type int Foo.t but an expression was expected of type bool Foo.t Type int is not compatible with type bool This is the | b =3D BOOL { Bool b } line. I believe the error comes from not having the locally-abstract type annotations in the code generated by Menhir. Is there any way around this? Thanks in advance, Andre --Lg1RXtQ7MIwSpuFJkmdILFwcCVtn064aA 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) iQEcBAEBAgAGBQJVGuSEAAoJED4JW1qwFY2cN5IIAK37M/QVqMtby050T3rnN9hr jWHIy0vaksfrz4MmyOSgULWsnJzk3CY6VdTTUgTySxzmNYdWus05jxxa9oAO2LbS Y6rAanfr+OdLaRDz0iVEH+xCuawg+YCUddsV/M1+I1BcUtiQaH+kjsxEkB7MXdx2 H3DDcEucFvViPDRzcuZx5hAf8KS8wmJL0z7wiJht/1PIAmYLFqKLVpN2MfNYHUBX 3CkgZPcAvzDVqMSEWwk55H8bglnpLBKWQfun3nb2dAqrgzTufEMCpUi7jces7Iqo AUhR17L5jFYC3RjrP46RjQ+A4Qa9PqWvyQeeAcbRzd4FlKkmlKBOTIrbb/ugyPY= =7jRH -----END PGP SIGNATURE----- --Lg1RXtQ7MIwSpuFJkmdILFwcCVtn064aA--