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 AD2C77FA83 for ; Fri, 14 Apr 2017 17:30:37 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jacquev6@gmail.com; spf=Pass smtp.mailfrom=jacquev6@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f181.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jacquev6@gmail.com) identity=pra; client-ip=209.85.220.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacquev6@gmail.com"; x-sender="jacquev6@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jacquev6@gmail.com designates 209.85.220.181 as permitted sender) identity=mailfrom; client-ip=209.85.220.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacquev6@gmail.com"; x-sender="jacquev6@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-qk0-f181.google.com) identity=helo; client-ip=209.85.220.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jacquev6@gmail.com"; x-sender="postmaster@mail-qk0-f181.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AithAvBE4NcF0QqK3SOOxvJ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78rs6wAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj?= =?us-ascii?q?8KOT43/m/Ul8J+kr5Urh26qhxj2o7Zep2ZOOZicq7fe94RWGpPXtxWVyxEGo6z?= =?us-ascii?q?YIoPD+wdMulGqYn9u0YFox+kCgawHePv1yFHhmTr1qA9zeQhEAfG0xA+ENIIrH?= =?us-ascii?q?TZt8v1NKYUUe+p0qbIyynDY+pU2Tjn9IfIaw0hru+XXb5qd8re11UvGhrDg16N?= =?us-ascii?q?p4LlODaV2f4Ms2id9+dgS+Ovi2g7pA5vpDiv2t4giovTiY0J01DE6Dt2wJ0vKd?= =?us-ascii?q?2+VkF7fdipG4ZTuSGCL4Z6XN8uTmVytCs5yrAKo4C3cDYWxJg92hLSaOGLfo6V?= =?us-ascii?q?6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJksDPtnwRzhDT5NWLR/?= =?us-ascii?q?hg8ku71jaP0AfT6u5AIU8qj6bUN5khwrsompoSt0TMADP2lV3ogKOKckgo4Oul?= =?us-ascii?q?5uT9brn4uJOQK5V4hhz9P6gzgsC/BP43MgkKX2iV4+S807jj8FX7QLpQkvI2i7?= =?us-ascii?q?TZv47EJckavaO5DApV3Zwi6xa7FTupzNMYnXwfIFJfZB2Hl5TpO03JIP3gEfiw?= =?us-ascii?q?mVGskDNyy/DCP73hGYnNI2PYkLbheLZ981RTxBAyzdBZ/ZJUC6sOLOj9Wk/r55?= =?us-ascii?q?TkCUoyOgmwhuLmE8k1gogXXGbKBq6CLIvTt0WJ76QhOb/fSpUSvWPDKv4u6vjy?= =?us-ascii?q?xV0wkkYAcLLhiYUWbnu1GOhOPUSfanfqnpIDGGwTowclCurnlAvRAnZoe3+uUv?= =?us-ascii?q?dktXkAA4W8ANKbSw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CZAAAq6vBYhrXcVdFcHQEXAQYBCwEXA?= =?us-ascii?q?QYBg3yBCweDX7QGhXIGAoN7B0IVAQEBAQEBAQEBAQESAQEBCAsLCCgvgjMggmw?= =?us-ascii?q?EGQE5Aw0FEA8CJgIkEgEFASIuiWQDFZh7g0U/jASBbDqDCQWDfScNg30CBhJ5h?= =?us-ascii?q?FOFM4gQgl8FiTCTZ4FWhS6LYWqBFYFgg1CKF5JCFB+BFTWBJyYdCCMKWQaCa4E?= =?us-ascii?q?JAQsBgkQ+NYk7AQEB?= X-IPAS-Result: =?us-ascii?q?A0CZAAAq6vBYhrXcVdFcHQEXAQYBCwEXAQYBg3yBCweDX7Q?= =?us-ascii?q?GhXIGAoN7B0IVAQEBAQEBAQEBAQESAQEBCAsLCCgvgjMggmwEGQE5Aw0FEA8CJ?= =?us-ascii?q?gIkEgEFASIuiWQDFZh7g0U/jASBbDqDCQWDfScNg30CBhJ5hFOFM4gQgl8FiTC?= =?us-ascii?q?TZ4FWhS6LYWqBFYFgg1CKF5JCFB+BFTWBJyYdCCMKWQaCa4EJAQsBgkQ+NYk7A?= =?us-ascii?q?QEB?= X-IronPort-AV: E=Sophos;i="5.37,199,1488841200"; d="scan'208";a="269111358" Received: from mail-qk0-f181.google.com ([209.85.220.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 14 Apr 2017 17:30:34 +0200 Received: by mail-qk0-f181.google.com with SMTP id h67so70114442qke.0 for ; Fri, 14 Apr 2017 08:30:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:sender:from:date:message-id:subject:to :content-transfer-encoding; bh=QstFeVEboExU0k2K6U10O6CsoKj5BNM9Uz9u+F7vncw=; b=JCDyAF/5y9rEiYlGBWHNKmnGffUarabEA/m/VqFDYU5IVrhEKI4TurHyJPdwd8TWKJ +J/FQPVcUkGaOVYErIGVuyxBXR/5w4U7mSgZHbBDIJbVreZXyttjEef8rcyHu0Rorg9G a3X4xwHmWQbjhBKkEJgZ+hh+4K3knkuV7bjh3esBtxkggUbVtP6j94/TEjujNJzewd4Q t9gvFhLmkb9fuDImoQkxn217tWuH8BNX68/AceyD7GLAD6xS35Ipa9/ptdmBbHMOAnEV YigRw1egDDxl/z6BMWBgpYgvyLDrCT++ScEeouWsypaih6vp/9fFeNMiIdJRVqNA/Qt2 5EOA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:sender:from:date:message-id:subject :to:content-transfer-encoding; bh=QstFeVEboExU0k2K6U10O6CsoKj5BNM9Uz9u+F7vncw=; b=cqQKdWxv97b08g1E+i5XTyImvaEJMFDSHzeIircPOi9MgR76XeUb+S6lPWJzOWRAfW WWd+Mhv3T2nnG8uac36J2QxkJ8KVFJt1e8jjeI9Zc1tuV/FWbqxewumPJgvIFmriJAHR AVDbtsrAN/EKX+MfFxx6p+0j59kSqQKHaubj07qqIlmpuLVSoW+K2nrjGLg51yJxubg3 Pi/DGwoBUYL0Ngx1uKpSy0divXBa5ft6DGQ9ejAiJcW53hZRrCqaNX9f40ALk0Os0WVw gKI8JcalYiEBZMyx9sNMVBlm8cgQnQxyxwvo/85wo6dnj+f24Pgqt6mZN0BLRKHuHZoc qDqQ== X-Gm-Message-State: AN3rC/5NYPLeuSKMVZRNI4lNFU/3DI5kJ8NLq5ewVdkV9+mQaE8LptPB k1gSQDS6gVWk83kv4sSU3Yv/C1ZB3SMSiTI= X-Received: by 10.55.166.134 with SMTP id p128mr7909376qke.132.1492183833507; Fri, 14 Apr 2017 08:30:33 -0700 (PDT) MIME-Version: 1.0 Sender: jacquev6@gmail.com Received: by 10.55.76.215 with HTTP; Fri, 14 Apr 2017 08:30:33 -0700 (PDT) From: Vincent Jacques Date: Fri, 14 Apr 2017 17:30:33 +0200 X-Google-Sender-Auth: ABHH4qr-QjenypXx_K-7w0Knwto Message-ID: To: caml-list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Validation-by: vincent@vincent-jacques.net Subject: [Caml-list] Typing of recursive function with polymorphic variants Hello, utop # let rec f1 =3D function | `A x -> f1 x | `B -> `B;; val f1 : ([< `A of 'a | `B ] as 'a) -> [> `B ] =3D utop # let rec f2 =3D function | `A x -> f2 (f2 x) | `B -> `B;; val f2 : ([< `A of 'a | `B > `B ] as 'a) -> 'a =3D but I can *see* that f2 never returns an `A so I would give it the same type as f1. 1) Would I be right or am I missing something? 2) Assuming I'm right, can you please give me hints about this limitation of the typing algorithm? I have a basic understanding of the W typing algorithm. Assuming that a similar algorithm is used for polymorphic variants, I imagine that when I call f2 (f2 x), f2's return type is "unified" with f2's parameter type. Why is this needed? 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? I tried to annotate f3 (f3 x) but I get different behaviors in utop and in the compiler. I'm lost :) utop # let rec f3 =3D function | `A x -> ((f3 (f3 x)):[`B]) | `B -> `B;; 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 In a .ml file: let rec f3 =3D function | `A x -> ((f3 (f3 x)):[`B]) | `B -> `B let () =3D f3 Error: This expression has type [ `B ] -> [ `B ] but an expression was expected of type unit Thank you for your help, --=20 Vincent Jacques http://vincent-jacques.net "S'il n'y a pas de solution, c'est qu'il n'y a pas de probl=C3=A8me" Devise Shadock