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 312787FA83 for ; Fri, 14 Apr 2017 20:11:54 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mandrykin@ispras.ru; spf=Pass smtp.mailfrom=mandrykin@ispras.ru; spf=None smtp.helo=postmaster@smtp.ispras.ru Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of mandrykin@ispras.ru) identity=pra; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of mandrykin@ispras.ru designates 83.149.199.196 as permitted sender) identity=mailfrom; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="mandrykin@ispras.ru"; 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@smtp.ispras.ru) identity=helo; client-ip=83.149.199.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="mandrykin@ispras.ru"; x-sender="postmaster@smtp.ispras.ru"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AL+px/xTJ55DriTLFc1PBeoAdINpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6ybRaN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0li?= =?us-ascii?q?gIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRBDI2i?= =?us-ascii?q?coUBAekPMuhaoInzqFQAogexCBKwBOP20DJEmmP60Kw43uknDArI3BYgH9ULsH?= =?us-ascii?q?nMq9v1NaQSUeCvw6nJyTXIcvRY1i376IfVaBAgofKMXbN2ccHMzkQvEhnKjlON?= =?us-ascii?q?poz/PzKV1eUNs26A4uphTuKvk3QnpBtqojS13Mcsl5DEi4QIwV7K8iV5xZw6Jd?= =?us-ascii?q?y+SENjZd6kEZ1QtzyVNotqXMwiWH1ouCc8yr0Jo5K7ezIKyJs/yx7Yd/OIaY2I?= =?us-ascii?q?4hb5WOaWOzd4i2ppeLO5hxao8Eiv0PfwVseu0FpSsypFisfDtnYL1xDJ9MeIV+?= =?us-ascii?q?Z980G80jiMzwDe8uJJLE4umabGJJMsxqQ8mocXvEnHBCP6hUH7ga6Qe0454Oan?= =?us-ascii?q?8f7nba/jppKEN497lAX+MqM2l8ykBOQ4LhAOU3Ka+eSnzL3j51f2QK5Qgv0sj6?= =?us-ascii?q?nVqJHaJcIFqa6lGwJY0Ygu5wyiAzqp1NkUh2QLIVZBdR6dkoTkP1DDLOj9Dfil?= =?us-ascii?q?glSslDlrx+rBPr3kGpjNK2LMkLH8crZn609cywszzdZE6pJVEbEBOOjzVVXqtN?= =?us-ascii?q?DCFB85LhS4w/z7B9VlyoMeRWWPD7eFP6zItF+I4vsjI+2NZI8OpDbwMOMl5v7r?= =?us-ascii?q?jX8hg1ARZ6ip3Z0NaHC5BPtqOUuZYWC/yusGRGwDuw57SO3xlHWDVyRSbjC8Re?= =?us-ascii?q?Z02DA9A4+gEc/hT4u0nbGalHOlH5tda2ZaIk6NF3zlcZnBWf4HcT+fOYlnnyBS?= =?us-ascii?q?Bpa7TIp08BCttAb7z/JCJ+zY4DwbtJSrgN184eHJhBIz8xR1FNyH2nrLVXwizT?= =?us-ascii?q?BAfCM/wK0q+R818VyEy6UtxqUATdE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DnGwD4D/FY/8THlVNcFjMYB4N8gQuDZ?= =?us-ascii?q?osIkGqMZYh5gg8ugwyCagKEQBYBAQEBAQEBAQEBAWoogjMiAYI/AQEBAQIBIwR?= =?us-ascii?q?XCwkCGAICBSECAg8BRwYBEooPDAqLLZ1dgWw6ixUMASWBC4o7hFeDBoJfAQSJM?= =?us-ascii?q?IdBjCaHBI41gQuGeoZtlAomAy6BBUMvR4ZkPTUBAYlGAQEB?= X-IPAS-Result: =?us-ascii?q?A0DnGwD4D/FY/8THlVNcFjMYB4N8gQuDZosIkGqMZYh5gg8?= =?us-ascii?q?ugwyCagKEQBYBAQEBAQEBAQEBAWoogjMiAYI/AQEBAQIBIwRXCwkCGAICBSECA?= =?us-ascii?q?g8BRwYBEooPDAqLLZ1dgWw6ixUMASWBC4o7hFeDBoJfAQSJMIdBjCaHBI41gQu?= =?us-ascii?q?GeoZtlAomAy6BBUMvR4ZkPTUBAYlGAQEB?= X-IronPort-AV: E=Sophos;i="5.37,199,1488841200"; d="scan'208";a="269125242" Received: from bran.ispras.ru (HELO smtp.ispras.ru) ([83.149.199.196]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Apr 2017 20:11:53 +0200 Received: from molnar.localnet (molnar.intra.ispras.ru [10.10.2.183]) by smtp.ispras.ru (Postfix) with ESMTP id 278EB61296; Fri, 14 Apr 2017 21:11:52 +0300 (MSK) From: Mikhail Mandrykin To: caml-list@inria.fr, Vincent Jacques Date: Fri, 14 Apr 2017 21:11:52 +0300 Message-ID: <2493165.Qrs57diDXJ@molnar> User-Agent: KMail/5.1.3 (Linux/4.4.0-70-generic; KDE/5.18.0; x86_64; ; ) In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] Typing of recursive function with polymorphic variants Hello, On =D0=BF=D1=8F=D1=82=D0=BD=D0=B8=D1=86=D0=B0, 14 =D0=B0=D0=BF=D1=80=D0=B5= =D0=BB=D1=8F 2017 =D0=B3. 17:30:33 MSK Vincent Jacques wrote: > utop # let rec f2 =3D function >=20 > | `A x -> f2 (f2 x) > | `B -> `B;; >=20 > val f2 : ([< `A of 'a | `B > `B ] as 'a) -> 'a =3D > 3) The type of f2 is more generic than the type of f1. Could I use > type annotations to help the typing algorithm choose a more specific > type? >=20 > I tried to annotate f3 (f3 x) but I get different behaviors in utop > and in the compiler. I'm lost :) To give the function f2 the desired type ([< `A of 'a | `B ] as 'a) -> [> `= B ]=20 the type-checker needs to treat the type of this function (f2) as polymorph= ic=20 inside the body of the function to avoid unifying the result type with the= =20 type of the first parameter. In OCaml this can be achieved by using an expl= icit=20 polymorphic type annotation (https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227):=20 let rec f2 : 'a. ([<`A of 'a | `B ] as 'a) -> [`B]=3D function | `A x -> f2 (f2 x) | `B -> `B;; val f2 : ([< `A of 'a | `B ] as 'a) -> [ `B ] =3D > Assuming that > a similar algorithm is used for polymorphic variants Indeed, polymorphic variant types are treated by using constrained=20 polymorphism integrated into usual HM type system, as described in the pape= rs=20 referenced here: (http://ocaml.org/docs/papers.html#PolymorphicVariants). > Why is this needed? The unification is probably done because constrained type variables are tre= ated=20 as normal unification variables. AFAIK type inference for polymorphic recur= sion=20 is undecidable (semidecidable) in general (there are some references in this message http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00924.html) and OCaml doesn't provide any incomplete support for some special cases, bu= t=20 allows to specify polymorphic types explicitly using those annotations. -- Best, Mikhail >=20 > utop # let rec f3 =3D function >=20 > | `A x -> ((f3 (f3 x)):[`B]) > | `B -> `B;; >=20 > Error: This pattern matches values of type [? `A of [ `B ] ] > but a pattern was expected which matches values of type [ `B ] > The second variant type does not allow tag(s) `A >=20 > In a .ml file: >=20 > let rec f3 =3D function >=20 > | `A x -> ((f3 (f3 x)):[`B]) > | `B -> `B >=20 > let () =3D f3 >=20 > Error: This expression has type [ `B ] -> [ `B ] > but an expression was expected of type unit >=20 > Thank you for your help, --=20 Mikhail Mandrykin Linux Verification Center, ISPRAS web: http://linuxtesting.org e-mail: mandrykin@ispras.ru