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 BFD1C7EE99 for ; Tue, 10 Dec 2013 23:44:00 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBANB8p1KFBoIFnGdsb2JhbABZhxG2HoE3DgEBAQEBCBQJPIIlAQEEASMEHAE1AgMLCw4MAiYCAlcGiA8FsFd2g2IChWGGEBAHgSmNKTMHgmw1gROYGIZFjws X-IPAS-Result: AtEBANB8p1KFBoIFnGdsb2JhbABZhxG2HoE3DgEBAQEBCBQJPIIlAQEEASMEHAE1AgMLCw4MAiYCAlcGiA8FsFd2g2IChWGGEBAHgSmNKTMHgmw1gROYGIZFjws X-IronPort-AV: E=Sophos;i="4.93,867,1378850400"; d="scan'208";a="48162604" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 10 Dec 2013 23:43:58 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id DFCF163F4; Wed, 11 Dec 2013 07:43:54 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id A3E6E2564; Wed, 11 Dec 2013 07:43:54 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from [10.39.20.27] (unknown [180.94.118.6]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 61E382532; Wed, 11 Dec 2013 07:43:53 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.0 \(1822\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Wed, 11 Dec 2013 09:43:48 +1100 Cc: OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: <83E00BC5-3599-4702-873E-0FD6863050CC@math.nagoya-u.ac.jp> References: To: Lukasz Stafiniak X-Mailer: Apple Mail (2.1822) Subject: Re: [Caml-list] Polymorphic recursion and GADTs On 2013/12/11 01:24, 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 >=20=20=20 > 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 As always, Gabriel's answer is correct, but I have two remarks. First, concerning your first example where you needed annotations on the lo= cal function, you can actually avoid that by using pattern matching rather than function = application: let rec walk : type a b . (a place -> b place -> (a, b) nearby) =3D fun x goal -> match compare x goal with | Same -> Here (x, goal) | NotSame -> let Ex1 ((y, to_y)) =3D wander x in Transitive (to_y, walk y goal) Now, for the above example, of course you don't need to annotate the "funct= ion" construct, but if you want to name the rigid variables 't47 and 't59, you can do that = through eta-expansion: 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 -> (fun (type b) p -> let ((x, y): (a * b)) =3D eval p in x) p | Snd p -> (fun (type b) p -> let ((x, y): (b * a)) =3D eval p in y) p Not very clean, so we need to do something about it. Jacques=