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 058697F60B for ; Fri, 24 Mar 2017 10:55:43 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nicolas.ojeda.bar@lexifi.com; spf=None smtp.mailfrom=nicolas.ojeda.bar@lexifi.com; spf=None smtp.helo=postmaster@vrout30.yaziba.net Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nicolas.ojeda.bar@lexifi.com) identity=pra; client-ip=185.56.204.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ojeda.bar@lexifi.com"; x-sender="nicolas.ojeda.bar@lexifi.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nicolas.ojeda.bar@lexifi.com) identity=mailfrom; client-ip=185.56.204.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ojeda.bar@lexifi.com"; x-sender="nicolas.ojeda.bar@lexifi.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@vrout30.yaziba.net) identity=helo; client-ip=185.56.204.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ojeda.bar@lexifi.com"; x-sender="postmaster@vrout30.yaziba.net"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AR34eGBP3mARg75Z/I9Al6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0I/T4rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPde?= =?us-ascii?q?RWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbY?= =?us-ascii?q?UwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiC?= =?us-ascii?q?cfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvdxeb7Tfc4BRWpZQMleSzBBDI27?= =?us-ascii?q?b4sKFeUBPOBYpJT5q1YBqRayAA+hD/7txDBVnH/7xa810+ohHw/I3wIuAswAv2?= =?us-ascii?q?jPodrvKKsfS/q4wLXUwTjBaf5dxDfz6JLPchAkufyCRbNwftbWyUkrFQTFlU2f?= =?us-ascii?q?p5XnPzyLy+sCqXCU4vdlUuK1lmUqrAdxojmzyccrjonGnJkVxkrD9SV73ok6OM?= =?us-ascii?q?e3RFRgbtG+CptdrCWaOJV5Q8MjTWFouTw2xaEBuZ6+ZSUHzoksyRDYa/yCaYeI?= =?us-ascii?q?4xTjWf6QITd+nnJleaiwiwy88Ui60uH9VtO70FZNripCiNXDqncN1xnV58OaSf?= =?us-ascii?q?V95l+s1SuM2g3T8O1JIUE5mbDFJ5I9zbM8jJQevETbEiPohEn7iLWae0Yk9+Sy?= =?us-ascii?q?9ejrf7TrqoWBO4J3lA3zNLkllNalDuQiKAcOWnCW+eSi273n+k30WKtKjucxkq?= =?us-ascii?q?nErJDXK9gXqrS5AgBP04cj6g2wAC283NQeg3YHMEpJeBOBj4f3J1HDOO30APS/?= =?us-ascii?q?jli2kDpmxurKMqP9DpjCNHTOnrfsca5460FGyQozyd5f54hTCrEEOP/zXE7xu8?= =?us-ascii?q?DfDh89KQO02PzrCNJ/1owARG2AGLWVP7jIvl+S/e8vJ/eDZYAUuDbzKvgp/eLh?= =?us-ascii?q?jXg8mVMFZ6mmwYMXaGykHvRhO0iWfWDjgtIFEWsTugo+TffqiEGZXD5IZ3eyWr?= =?us-ascii?q?o86SshBIKnC4fDXIGtj6ab0Ce1BJ1afmVGCleRHnj2b4iEQPIMaD6KIs9mjzwE?= =?us-ascii?q?Sevpdok6yBv7tBPm06E1aa3P6ygAvNTi0sJ07qvdj1Yp5DlsBoOUyWrKRGhxmi?= =?us-ascii?q?YMRiQqj5x49GNn11KbwOAsjOZFEMRCz/9TVAB8OIOKnMJgDNWnfAPKedMAU2GB?= =?us-ascii?q?QNiqCAYbwsh5l9kPaEF5Es7kiRLO0yPsCbYPv7iGFJ068+TX2H2ndJU18GrPyK?= =?us-ascii?q?R01wpuecBIL2Dzw/Mm+g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BRAgDE7NRYhyPMOLldHQYMGgYMhAqBC?= =?us-ascii?q?wEGg1uLApBbEIIqlR0qhXgCgxlKFAEBAQEBAQEBAQEBEgEBAQoLCQgoL4IzBAI?= =?us-ascii?q?DGQWCPAECAgEjBEcLBQsLBAcaHQICIhIBBQEKEgYTEoldAw0IBAEJnG4/jAOBb?= =?us-ascii?q?DqHNQODDAEBAQcBAQEBAQEBIYs9h1qCXwWBWIVqDIFXkzSGe4tQglCBC41Vkh0?= =?us-ascii?q?UH4ETAg8ngSVZVhcGhAJKgXB0AYgGgWcBAQE?= X-IPAS-Result: =?us-ascii?q?A0BRAgDE7NRYhyPMOLldHQYMGgYMhAqBCwEGg1uLApBbEII?= =?us-ascii?q?qlR0qhXgCgxlKFAEBAQEBAQEBAQEBEgEBAQoLCQgoL4IzBAIDGQWCPAECAgEjB?= =?us-ascii?q?EcLBQsLBAcaHQICIhIBBQEKEgYTEoldAw0IBAEJnG4/jAOBbDqHNQODDAEBAQc?= =?us-ascii?q?BAQEBAQEBIYs9h1qCXwWBWIVqDIFXkzSGe4tQglCBC41Vkh0UH4ETAg8ngSVZV?= =?us-ascii?q?hcGhAJKgXB0AYgGgWcBAQE?= X-IronPort-AV: E=Sophos;i="5.36,214,1486422000"; d="scan'208,217";a="266021239" Received: from vrout30-bl.yaziba.net (HELO vrout30.yaziba.net) ([185.56.204.35]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 24 Mar 2017 10:55:42 +0100 Received: from mtaout20.int.yaziba.net (mtaout20.int.yaziba.net [10.4.20.37]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by vrout30.yaziba.net (mx10.yaziba.net) with ESMTPS id 97AB652127 for ; Fri, 24 Mar 2017 10:55:41 +0100 (CET) Received: from localhost (localhost [127.0.0.1]) by mtaout20.int.yaziba.net (Postfix) with ESMTP id 9E288160270 for ; Fri, 24 Mar 2017 10:55:41 +0100 (CET) X-Virus-Scanned: amavisd-new at mtaout20.int.yaziba.net Received: from mtaout20.int.yaziba.net ([127.0.0.1]) by localhost (mtaout20.int.yaziba.net [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id lAFKA6lDIWBC for ; Fri, 24 Mar 2017 10:55:41 +0100 (CET) Received: from mail-qt0-f182.google.com (mail-qt0-f182.google.com [209.85.216.182]) by mtaout20.int.yaziba.net (Postfix) with ESMTPSA id C3E581601AD for ; Fri, 24 Mar 2017 10:55:40 +0100 (CET) Received: by mail-qt0-f182.google.com with SMTP id i34so6572324qtc.0 for ; Fri, 24 Mar 2017 02:55:40 -0700 (PDT) X-Gm-Message-State: AFeK/H0fvV8CEXgYTAo6BP3PyYCkA9H8N+JEABHuGzWgcfDGIedvGRqx++sTQtTomtCYlMprrR451jjqI9sY8g== X-Received: by 10.200.49.66 with SMTP id h2mr6961847qtb.252.1490349323454; Fri, 24 Mar 2017 02:55:23 -0700 (PDT) MIME-Version: 1.0 Received: by 10.200.58.230 with HTTP; Fri, 24 Mar 2017 02:55:02 -0700 (PDT) In-Reply-To: <167e229f-2ffc-14ab-8725-5d1af71c167b@drno.eu> References: <167e229f-2ffc-14ab-8725-5d1af71c167b@drno.eu> From: =?UTF-8?Q?Nicol=C3=A1s_Ojeda_B=C3=A4r?= Date: Fri, 24 Mar 2017 10:55:02 +0100 X-Gmail-Original-Message-ID: Message-ID: To: Grumpy Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=001a11412778041127054b76fed6 X-DRWEB-SCAN: ok X-VRSPAM-SCORE: -51 X-VRSPAM-STATE: legit X-VRSPAM-CAUSE: gggruggvucftvghtrhhoucdtuddrfeelhedrjeehgddutdcutefuodetggdotefrucfrrhhofhhilhgvmecuggftfghnshhusghstghrihgsvgenuceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepjghfhfffkffuvfgtsegrtderredttdejnecuhfhrohhmpefpihgtohhljohspgfqjhgvuggrpgeumohruceonhhitgholhgrshdrohhjvggurgdrsggrrheslhgvgihifhhirdgtohhmqeenucffohhmrghinhepihhnrhhirgdrfhhrpdihrghhohhordgtohhmnecukfhppedvtdelrdekhedrvdduiedrudekvdenucfrrghrrghmpehmohguvgepshhmthhpohhuth X-VRSPAM-EXTCAUSE: mhhouggvpehsmhhtphhouhht Subject: Re: [Caml-list] Type inference curiosity --001a11412778041127054b76fed6 Content-Type: text/plain; charset=UTF-8 Hello, 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. See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227 for the details. Cheers, Nicolas On Fri, Mar 24, 2017 at 10:20 AM, Grumpy wrote: > Hello, > > I think there is an incoherency or a bug somewhere in the type inference > 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. > > 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). > > It seems the syntax (type a) leads to this incorrect behaviour... > > > type _ exp = > | Stop : int exp > | Inc : (int exp -> int) exp > > let rec eval : type a. a exp -> a = function > | Stop -> 0 > | Inc -> (fun (p : int exp) -> 1 + eval p) > > let rec eval2 (type a) (p : a exp) : a = > match p with > | Stop -> 0 > | Inc -> (fun (p : int exp) -> 1 + eval2 p) > > -- > 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 > --001a11412778041127054b76fed6 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hello,

Recursive definitions need to be= explicitly annotated to be polymorphic.=C2=A0 The (type a) annotation
introduces an abstract type a in the body of the function but does no= t make it polymorphic.
The annotation type a. on the other hand, = does both.


Cheers,
Nicolas


On Fri, Mar 24= , 2017 at 10:20 AM, Grumpy <grumpy@drno.eu> wrote:
Hello,

I think there is an incoherency or a bug somewhere in the type inference
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.

The function eval is typed correcly ('a exp -> 'a) while the typ= e
inferred for funcion function eval2 is (int exp -> int), which is wrong<= br> because of the Inc case returning ('a exp -> 'a).

It seems the syntax (type a) leads to this incorrect behaviour...


type _ exp =3D
=C2=A0 | Stop : int exp
=C2=A0 | Inc : (int exp -> int) exp

let rec eval : type a. a exp -> a =3D function
=C2=A0 | Stop -> 0
=C2=A0 | Inc -> (fun (p : int exp) -> 1 + eval p)

let rec eval2 (type a) (p : a exp) : a =3D
=C2=A0 match p with
=C2=A0 | Stop -> 0
=C2=A0 | Inc -> (fun (p : int exp) -> 1 + eval2 p)

--
Caml-list mailing list.=C2=A0 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

--001a11412778041127054b76fed6--