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 80D237EE99 for ; Tue, 10 Dec 2013 15:24:30 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.212.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 209.85.212.169 as permitted sender) identity=mailfrom; client-ip=209.85.212.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f169.google.com) identity=helo; client-ip=209.85.212.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-wi0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ag8DAAkjp1LRVdSplGdsb2JhbABZhBKCf7YegRUIFg4BAQEBBwsLCRIqgiYBBSMEGQEbHgMMBgMCBAc3AgIiAREBBQEcBogCAQMPlUaPW4wGU4MJhEEKGScNZIYDEQEFDI8AgmyBSASYFJAmGCmEVjs X-IPAS-Result: Ag8DAAkjp1LRVdSplGdsb2JhbABZhBKCf7YegRUIFg4BAQEBBwsLCRIqgiYBBSMEGQEbHgMMBgMCBAc3AgIiAREBBQEcBogCAQMPlUaPW4wGU4MJhEEKGScNZIYDEQEFDI8AgmyBSASYFJAmGCmEVjs X-IronPort-AV: E=Sophos;i="4.93,865,1378850400"; d="scan'208";a="40279382" Received: from mail-wi0-f169.google.com ([209.85.212.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Dec 2013 15:24:29 +0100 Received: by mail-wi0-f169.google.com with SMTP id hn6so5404257wib.0 for ; Tue, 10 Dec 2013 06:24:29 -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 :content-type; bh=eZQDTFUXQ6TNUGutaDr+KIFEajV5RPdlsaqEV3ZjhNk=; b=phZekelXyhMMo+Bq4hEa9lXGiwArONyYN6zD3bw1rqMuKYIdkfo3RyQaY0/QlVGreh CAnkObzlfA81iKsREyPa7TOTjIh4P3tZk0tE7bFzILjpauHNki5zy3QvclP5o/85JkpX Z3BK3WGcbfSXjNQqPshPhfwqza2HN2nvfpXjI+pJ/2jGPyv3AYoL8pIDQ3d+G/i1Z29K zKeegt8EKCCnj/Kf1YgUuHIqSResMgi7KIXO/ugkkDomc+l0MzsM5O5GlSecHGioehc4 TRJEvI3R5ZdGiWcniAQI2J/hL5ur4gZmDJrwzAEWMVDYZmcXJEkyhsvAq2/Ur5nnsO13 gC5g== X-Received: by 10.180.20.15 with SMTP id j15mr19706521wie.4.1386685469527; Tue, 10 Dec 2013 06:24:29 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.36.201 with HTTP; Tue, 10 Dec 2013 06:24:09 -0800 (PST) In-Reply-To: References: From: Lukasz Stafiniak Date: Tue, 10 Dec 2013 15:24:09 +0100 Message-ID: To: Caml Content-Type: multipart/alternative; boundary=bcaec53f3985d399f004ed2ede16 Subject: Re: [Caml-list] Polymorphic recursion and GADTs --bcaec53f3985d399f004ed2ede16 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 --bcaec53f3985d399f004ed2ede16 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I have another challenge for you. Without the redundant an= notations (i.e. with only an annotation on let-rec) it type-checks nicely. = I am providing more annotations as an option.
>= ;>>
type _ term =3D
=
=C2=A0 | Lit : integer -> integer term
<= div class=3D"gmail_extra">=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 t= erm -> (('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>

--bcaec53f3985d399f004ed2ede16--