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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 442397EE99 for ; Tue, 10 Dec 2013 20:08:26 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.50 as permitted sender) identity=mailfrom; client-ip=209.85.214.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f50.google.com) identity=helo; client-ip=209.85.214.50; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f50.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmACAOJlp1LRVdYym2dsb2JhbAA/GoM/U4J/rU6IUYEXCBYOAQEBAQEGCwsJFCiCJQEBBAEjBBkBGx0BAwELBgMCCwM0AgIhAQERAQUBHAYTh28BAwkGDTaVKo9bjAZTgwmEPgoZJw1khgMRAQUMjGeCEgeCbIFIBJYpgWuBMIsqg0wYKYRWOw X-IPAS-Result: AmACAOJlp1LRVdYym2dsb2JhbAA/GoM/U4J/rU6IUYEXCBYOAQEBAQEGCwsJFCiCJQEBBAEjBBkBGx0BAwELBgMCCwM0AgIhAQERAQUBHAYTh28BAwkGDTaVKo9bjAZTgwmEPgoZJw1khgMRAQUMjGeCEgeCbIFIBJYpgWuBMIsqg0wYKYRWOw X-IronPort-AV: E=Sophos;i="4.93,866,1378850400"; d="scan'208";a="48119987" Received: from mail-bk0-f50.google.com ([209.85.214.50]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Dec 2013 20:08:25 +0100 Received: by mail-bk0-f50.google.com with SMTP id e11so2073275bkh.23 for ; Tue, 10 Dec 2013 11:08:24 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=mPoGm4uR1ozVZHC4gyFsdIWZPtFCKNkMjR6pR6OOKA0=; b=fNh+g8V4svf34zA+n7IGMEGiaBGzAAY7lUGsRwxeU25vXI+SGZ01LeTsftGbwv0Cfm V24Ke1q2/DZ1ar+hLIKtgyLSe3jXpLTNuXnN35MXD5/5DpWoxQ7JdA5ZzNUqehIOOrn/ NQveSwjnqipvRaKjsp4E0qPfL8mkTOifCmyWGoWGWWTtFm7Agcuoow6mrvaYLeIESHNo LIHyNDXHk+pMRivIhNh3Ki72SWmvvcLgfqh4uccvO/g/T8bcW8RHmaKpBI+plT2YewWp hBCtcYztMJ5AF/rUKqnQktdKhRK726Opa8EtX66/rDww3v5k+P08oFSTFx2xJVJzvOox W4aw== X-Received: by 10.204.59.67 with SMTP id k3mr908899bkh.58.1386702504550; Tue, 10 Dec 2013 11:08:24 -0800 (PST) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Tue, 10 Dec 2013 11:07:44 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Tue, 10 Dec 2013 20:07:44 +0100 Message-ID: To: Lukasz Stafiniak Cc: Caml Content-Type: multipart/alternative; boundary=001a11c378d431907c04ed32d68f Subject: Re: [Caml-list] Polymorphic recursion and GADTs --001a11c378d431907c04ed32d68f Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable You must not use a type annotation here ('t47), because its (implicit) scope is above. Removing the annotation or using _ in lieu of the free type variable solves your problem. See this recent bugreport where the same question was raised: http://caml.inria.fr/mantis/view.php?id=3D6264 On Tue, Dec 10, 2013 at 3:24 PM, Lukasz Stafiniak wrote: > I have another challenge for you. Without the redundant annotations (i.e. > with only an annotation on let-rec) it type-checks nicely. I am providing > more annotations as an option. > >>> > type _ term =3D > | Lit : integer -> integer term > | Plus : integer term * integer term -> integer term > | IsZero : integer term -> boolean term > | If : (*=E2=88=80'a.*)boolean term * 'a term * 'a term -> 'a term > | Pair : (*=E2=88=80'a, 'b.*)'a term * 'b term -> (('a * 'b)) term > | Fst : (*=E2=88=80'a, 'b.*)(('a * 'b)) term -> 'a term > | Snd : (*=E2=88=80'a, 'b.*)(('a * 'b)) term -> 'b term > and integer > and boolean > > external plus : (integer -> integer -> integer) =3D "plus" > external is_zero : (integer -> boolean) =3D "is_zero" > external if_then : (boolean -> 'a -> 'a -> 'a) =3D "if_then" > let rec eval : type a . (a term -> a) =3D > ((function Lit i -> i | IsZero x -> is_zero (eval x) > | Plus (x, y) -> plus (eval x) (eval y) > | If (b, t, e) -> if_then (eval b) (eval t) (eval e) > | Pair (x, y) -> (eval x, eval y) > | Fst p -> let ((x, y): (a * 't47)) =3D eval p in x > | Snd p -> let ((x, y): ('t59 * a)) =3D eval p in y): a term -> a) > <<< > We get at "eval p" to the right of "let ((x, y): (a * 't47))": > Error: This expression has type a * b#0 > but an expression was expected of type a * b#0 > The type constructor b#0 would escape its scope > > --001a11c378d431907c04ed32d68f Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
You must not use a type annotation here ('t47), becaus= e its (implicit) scope is above. Removing the annotation or using _ in lieu= of the free type variable solves your problem. See this recent bugreport w= here the same question was raised:
=C2=A0 http://ca= ml.inria.fr/mantis/view.php?id=3D6264


On Tue, Dec 10, 2013 at 3:= 24 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
I have another challenge fo= r you. Without the redundant annotations (i.e. with only an annotation on l= et-rec) it type-checks nicely. I am providing more annotations as an option= .
>>>
typ= e _ term =3D
=C2=A0 | Lit : integer -> i= nteger term
=C2=A0 | Plus : integer term * = integer term -> integer term
=C2=A0 | IsZero : integer term -> boolean ter= m
=C2=A0 | If : (*=E2=88=80'a.*)boolean= term * 'a term * 'a term -> 'a term
=C2=A0 | Pair : (*=E2=88=80'a, 'b.*)'a term * = 'b term -> (('a * 'b)) term
=C2=A0 | Fst : (*=E2=88=80'a, 'b.*)((= 9;a * 'b)) term -> 'a term
=C2= =A0 | Snd : (*=E2=88=80'a, 'b.*)(('a * 'b)) term -> '= ;b term
and integer
and boolean
=C2=A0=C2=A0
external plus : (= integer -> integer -> integer) =3D "plus"
external is_zero : (integer -> boolean) =3D "is_zero"
external if_then : (boolean -> 'a -> &= #39;a -> 'a) =3D "if_then"
let rec eval : type a . (a term -> a) =3D
=
=C2=A0 ((function Lit i -> i | IsZero x ->= is_zero (eval x)
=C2=A0 =C2=A0 | Plus (x, y) -> plus (eval x) = (eval y)
=C2=A0 =C2=A0 | If (b, t, e) ->= if_then (eval b) (eval t) (eval e)
= =C2=A0 =C2=A0 | Pair (x, y) -> (eval x, eval y)
=C2=A0 =C2=A0 | Fst p -> let ((x, y): (a * &#= 39;t47)) =3D eval p in x
=C2=A0 =C2=A0 | Sn= d p -> let ((x, y): ('t59 * a)) =3D eval p in y): a term -> a)
<<<
We get at "eval p" to the right of "let ((x, y): (= a * 't47))":
Error: This expression has type a * b#0
=C2=A0 =C2=A0 =C2=A0 =C2=A0but an expression was expected of type a = * b#0
=C2=A0 =C2=A0 =C2=A0 =C2=A0The type constructor b#0 would escape its scope<= /div>


--001a11c378d431907c04ed32d68f--