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 1D625800FD for ; Tue, 28 Mar 2017 05:11:14 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jacques.garrigue@gmail.com; spf=Pass smtp.mailfrom=jacques.garrigue@gmail.com; spf=None smtp.helo=postmaster@mail-pg0-f41.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jacques.garrigue@gmail.com) identity=pra; client-ip=74.125.83.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jacques.garrigue@gmail.com designates 74.125.83.41 as permitted sender) identity=mailfrom; client-ip=74.125.83.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="jacques.garrigue@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-pg0-f41.google.com) identity=helo; client-ip=74.125.83.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacques.garrigue@gmail.com"; x-sender="postmaster@mail-pg0-f41.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AjD47aR92Fh1H6P9uRHKM819IXTAuvvDOBiVQ1KB2?= =?us-ascii?q?1e4cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/?= =?us-ascii?q?8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1?= =?us-ascii?q?Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+?= =?us-ascii?q?RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTF?= =?us-ascii?q?UACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiC?= =?us-ascii?q?gZMT457HrXgdF0gK5CvR6tuwBzz4vSbY6SKfR+Y7jdfcsESmVdQsZfWStBAoam?= =?us-ascii?q?YIsOCeoKIOJUoob5qlcLqxa1GAuiC/71yjJQnX/5waI13fkhHw7E0gIuENEAsH?= =?us-ascii?q?rKotvyL6oSTfm1zKzUwTXDc/9b2zHw45XIfBA7pvGMWKp9f87LxkYzDgPFk0uf?= =?us-ascii?q?qZf4ND2UzOsNqXKb7+tvVeKylWEstgZ8oje1ycc2kInJh40Vyk3a+ihixYY6P8?= =?us-ascii?q?G4SE5hbd6iCpRQuCaaNotsTc87XmFkojw1xaEctZ65ZCgH0ZIqzAPRZfyAdoiH?= =?us-ascii?q?+BPjVOCJLDd5gnJlYrO/iAyo/Uiu0O3wTsm130xKripCldnArGwC1xvW6sWBV/?= =?us-ascii?q?Bz/V+h1C6N2g3c8O1IPF44mKrBJ5MizLM8jJUevVnbEiL2m0j6lrKae0Un9+Sy?= =?us-ascii?q?9ujrfLbrqoWBO4J0iAzzNLkllNalDuQiKAcOWnCW+eSi273n+k30WLBKgec3kq?= =?us-ascii?q?ndqZzaPcsbqrKgDw9b3Ysv9gyzDzih0NQfknkHKExKdAibgIjuPlHCOPH4DfGh?= =?us-ascii?q?jFSwiDpmxf/LMqf8DpnTLnXPirTscLhn50NT1QY/1dVf6IhVCrEFLvLzQEjxtN?= =?us-ascii?q?nAAx87KQO73//nCMhj2YMFQ26PDbWWMLnIsV+J6eIvPveDaZQauDb4Mfcl5vru?= =?us-ascii?q?gWUlll8aeKmlxYEXZ2ygHvR6P0WZZmLhjcsbHmcPugoyVejqiFyZUT5PfHuyRK?= =?us-ascii?q?I95jQjCI28F4vDR4atgKaA3CihBJFWaHpGWRixF2z1fdCER+sUc3DVZdRwlyQN?= =?us-ascii?q?E7mnUY4okx+08xTrzqJuaePO8WoTvJfnkdx0/PGAqRZn2iZpCtyMmzWCVXxxhn?= =?us-ascii?q?IgSyUw2+ZyvBou5E2E1P1aivdBCNFIr9xASB07OoPRh7h1AsroWw3cc/+MQUqm?= =?us-ascii?q?BNOvDjYgR5cshdYFJURlTYbxxivf1janVudG34eAA4Y5p+eBhnU=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DuAQDZ09lYhilTfUpdGgEBAQMBAQEJA?= =?us-ascii?q?QEBFwEBAQMBAQEJAQEBhAqBC4NiiwKQXYI6BZMMgg8phXQCAoMgQRYBAQEBAQE?= =?us-ascii?q?BAQEBARIBAQEICwsIKC+CMwQCAxkFgjsBAQICASMEGQEtCwEDAQsBBQUYAgIJD?= =?us-ascii?q?wsDAgI0AQUBCgERBhMSiV0DDQcBDp9QP4wDgWw6gwkFhAInAworGoJGAQEBBwE?= =?us-ascii?q?BAQEBAQEBGAIGCQEIeYdIgmqEVIMGLoIxBYcVByYMiRGLfIZ7i1GCUId7hmaPK?= =?us-ascii?q?4JyM4EVJg6BJzo0QREBgjU4g2hmAYgFgWcBAQE?= X-IPAS-Result: =?us-ascii?q?A0DuAQDZ09lYhilTfUpdGgEBAQMBAQEJAQEBFwEBAQMBAQE?= =?us-ascii?q?JAQEBhAqBC4NiiwKQXYI6BZMMgg8phXQCAoMgQRYBAQEBAQEBAQEBARIBAQEIC?= =?us-ascii?q?wsIKC+CMwQCAxkFgjsBAQICASMEGQEtCwEDAQsBBQUYAgIJDwsDAgI0AQUBCgE?= =?us-ascii?q?RBhMSiV0DDQcBDp9QP4wDgWw6gwkFhAInAworGoJGAQEBBwEBAQEBAQEBGAIGC?= =?us-ascii?q?QEIeYdIgmqEVIMGLoIxBYcVByYMiRGLfIZ7i1GCUId7hmaPK4JyM4EVJg6BJzo?= =?us-ascii?q?0QREBgjU4g2hmAYgFgWcBAQE?= X-IronPort-AV: E=Sophos;i="5.36,235,1486422000"; d="scan'208";a="266467041" Received: from mail-pg0-f41.google.com ([74.125.83.41]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 28 Mar 2017 05:11:12 +0200 Received: by mail-pg0-f41.google.com with SMTP id 21so58895983pgg.1 for ; Mon, 27 Mar 2017 20:11:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=+PaUi/IaMeCP10x4wZujyJkIk+z0KyQuoPfnxkSOPJc=; b=FpnN8PXBmv1DOeIlbusAF+OdnSV7wVIgdnVT5TBym30WKgd/P2q55+DjPbo8ZfHkJ9 Bm4xs5Q6kK2vF31GKrxsU6lEoygf5WEVSF3b9qIXeMGd8DOs0P63XnJ0qF7t0EKqJUGF FEphB4G0xvg4Veo9PihNOSHVpl6/x6GdMGRPjIl7A9CcfoUC3rHEMxWJQ1dBzD+HlSqN TNwYRoHZDnfABjJuNEKv1cwkG9MRqDWeC/Rh/0wjN4RSGGADHOExfdkPgVb6zoy4hZfj Hqc6jr2JRIdDrMj7wsfvN3f3f0L3g13KtBvtbJAjORBuyP5aAk5JAR9k40XrMwfMPHVZ zUqQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:sender:mime-version:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references:to; bh=+PaUi/IaMeCP10x4wZujyJkIk+z0KyQuoPfnxkSOPJc=; b=rSHSlRaTBam/3flInqIycSz4+XpzzGWdzuTG4CE+SgRmY5A/9FfHZ26jB+dwey3Rac XdOW/fsC8uxvNtvIYd4N/dgwI3xVDjqecltP/NADN9TVWv1pwM2WLUFN1Y+8BJz02uUN AoobpbPLujvxhY9thgpmt83rC+UT7jdWtA12A8Tp0m3XCDb7zh0TvN2gsZ4BKMMI/9U8 7o3MkiP/HzcEzij7Tb2ePRWcvKKSAFJjaL7+06bBpcOR9J4P8oiebCvlLtvd+3NnHDA1 K3Si/eHfX53IcF2fkZhdpiqApHYTtXngQxQ+7/D1vadsWq2XORI//1qD8ZkiON0wC26l Po8Q== X-Gm-Message-State: AFeK/H09AQ5aZE/FArN82ybocaXdE45mpflJUyNx3s0C97P02H8BtaJM0d9JFvsF1lzGDA== X-Received: by 10.98.80.208 with SMTP id g77mr29445934pfj.249.1490670671395; Mon, 27 Mar 2017 20:11:11 -0700 (PDT) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp. [58.158.128.157]) by smtp.gmail.com with ESMTPSA id e7sm3703767pgp.2.2017.03.27.20.11.09 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 27 Mar 2017 20:11:10 -0700 (PDT) Sender: Jacques Garrigue Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: <317e04aa-de79-bf61-e1fd-f4d467b5a484@drno.eu> Date: Tue, 28 Mar 2017 12:11:25 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <5EF5FCB7-36B2-47A8-B783-7CE794468A46@math.nagoya-u.ac.jp> References: <167e229f-2ffc-14ab-8725-5d1af71c167b@drno.eu> <317e04aa-de79-bf61-e1fd-f4d467b5a484@drno.eu> To: Grumpy X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] Type inference curiosity On 2017/03/24 19:13, Grumpy wrote: >=20 > This does not explain why the compiler accepts as well typed the > function eval2, after inferring a =3D int from the first branch. > Do I miss something ? What is happening here is that the typing for (type a) is different interna= lly and externally. Inside the function, a is a locally abstract type, which can be refined both in int and (int exp -> int). Outside, it is a (not yet generalized) type variable. The recursive call forces this type variable to be unified with int, with no impact on the internal view. It works because there is only one recursive call. All this is perfectly sound. I admit this is confusing, so writing recursive function types as in eval i= s the right way. Jacques > Le 24/03/2017 =C3=A0 10:55, Nicol=C3=A1s Ojeda B=C3=A4r a =C3=A9crit : >> Hello, >>=20 >> Recursive definitions need to be explicitly annotated to be >> polymorphic. The (type a) annotation >> introduces an abstract type a in the body of the function but does not >> make it polymorphic. >> The annotation type a. on the other hand, does both. >>=20 >> See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227 >> for the >> details. >>=20 >> Cheers, >> Nicolas >>=20 >>=20 >> On Fri, Mar 24, 2017 at 10:20 AM, Grumpy > > wrote: >>=20 >> Hello, >>=20 >> I think there is an incoherency or a bug somewhere in the type inferen= ce >> engine with the following code with version 4.02.3 (I have not tested = in >> previous versions). Both functions eval and eval2 are identical but the >> inferred types are different, and the type inferred for eval2 is >> actually wrong. >>=20 >> The function eval is typed correcly ('a exp -> 'a) while the type >> inferred for funcion function eval2 is (int exp -> int), which is wrong >> because of the Inc case returning ('a exp -> 'a). >>=20 >> It seems the syntax (type a) leads to this incorrect behaviour... >>=20 >>=20 >> type _ exp =3D >> | Stop : int exp >> | Inc : (int exp -> int) exp >>=20 >> let rec eval : type a. a exp -> a =3D function >> | Stop -> 0 >> | Inc -> (fun (p : int exp) -> 1 + eval p) >>=20 >> let rec eval2 (type a) (p : a exp) : a =3D >> match p with >> | Stop -> 0 >> | Inc -> (fun (p : int exp) -> 1 + eval2 p) >>=20 >> -- >> Caml-list mailing list. Subscription management and archives: >> https://sympa.inria.fr/sympa/arc/caml-list >> >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> >> Bug reports: http://caml.inria.fr/bin/caml-bugs >>