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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id D9B41800B6 for ; Mon, 2 Jan 2017 14:51:56 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A+F0ZIxeNY6dx1pQoPsu5SrHDlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcW6YR7h7PlgxGXEQZ/co6odzbGH7+a5ACdbuN6oizMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVr?= =?us-ascii?q?O+/7BpDdj9it1+C15pbffxhEiCCzbL52Ixi6txjdutQZjYZsN6o61wfErGZPd+?= =?us-ascii?q?lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLe?= =?us-ascii?q?TQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgz?= =?us-ascii?q?ocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6z?= =?us-ascii?q?b5EXAuUdMulWsonzqFkAoxWxBgesCv3hxDhTi3/qxK061vgtEQHa0AA+Gd8FrX?= =?us-ascii?q?TarM/yNKcXSe27yLPHwinab/NLxzj985XDfBE7rvGWR7JwcMXRyVQxGAjYiViQ?= =?us-ascii?q?ppbqPymP1uQMvGib8vRvWPmqi2E9twFxoiKjxsE2hYnGgYIUykrL+TxkwIovP9?= =?us-ascii?q?K3VFR3Ydy8EJZJsSyRKoV4QsQnQ25yuSY6zKULuYWnfCcQ1JsnxBnfa+KZfIiS?= =?us-ascii?q?7BLjUOGRIDliiH15f7K/ghC/+lWjxO3kTsS4zVhHoyRfntTNrHwByhLe5tSdRv?= =?us-ascii?q?Z95kus2TWC2xrO5uxEIk04j7fXJ4Aiz7Iqi5YesUbOEynrk0vslqCWbF8r+u2w?= =?us-ascii?q?5uTnfLrmopicOpdxig7kM6Qunsy/AeMjMggSRWSb/P6z1KHj/UHjRrVFlPI2kq?= =?us-ascii?q?7ZsZ/APMgbu7S1DBVJ3Yo56Ra/Fy+q0NUenXYZMFJIYA+LgobnNl3UIf30F+qz?= =?us-ascii?q?jlqwnDtxx/3KJrjhDY/MLnjHnrfhZ7F960tExQo8199f/YhUCrAOIPLuRED8r9?= =?us-ascii?q?nYAQUlMwy02ernDs9y1owZWWOPGKCVKb7SvUWS6e0zOeWMZpcVtC7nK/c5//7u?= =?us-ascii?q?kWM5mVgFcKa1x5QXbXS4Eu1iI0WYenrsnswMEXwKvwo7VOzlkkeOUT9VZ3aoXq?= =?us-ascii?q?Iz/Cs3CIy8DdSLeof4qbqd2yHzNJRdZmFAQgSFF2vycIOOUvwMaSS6LcpokzhC?= =?us-ascii?q?Xr+kHdwPzxar4S3zwKN6I/Gc1SQCr5PsydU9s+Lajwsz+iF5J8GUz2HLSWh7mX?= =?us-ascii?q?IBAiJw1as5o1QrmQTL6rRxn/ENTY8b3PhOSApvcMeEl+E=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CtAAAdWmpYlwWCBoVeGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFQEBAQECAQEBAQgBAQEBgwwBAQEBAX6BDAGOSJNRlyMBKYV4AoIiEAE?= =?us-ascii?q?BAQEBAQEBAQEBEgEBAQEBCBYHTYIzGgGCGwEFJxMGAwEnAwsBAQ4LDgocElcGL?= =?us-ascii?q?ohUD64zglM6gwgHAoRJGoJEAQEBAQEBBAEBAQEBAQEYAQiIRwiCV4RGgzGCMIZ?= =?us-ascii?q?rB4kUinyGVIpqgkaOD44aFIQPNoFLLg4BgUaCH4F4Y4kZAQEB?= X-IPAS-Result: =?us-ascii?q?A0CtAAAdWmpYlwWCBoVeGgEBAQECAQEBAQgBAQEBFQEBAQE?= =?us-ascii?q?CAQEBAQgBAQEBgwwBAQEBAX6BDAGOSJNRlyMBKYV4AoIiEAEBAQEBAQEBAQEBE?= =?us-ascii?q?gEBAQEBCBYHTYIzGgGCGwEFJxMGAwEnAwsBAQ4LDgocElcGLohUD64zglM6gwg?= =?us-ascii?q?HAoRJGoJEAQEBAQEBBAEBAQEBAQEYAQiIRwiCV4RGgzGCMIZrB4kUinyGVIpqg?= =?us-ascii?q?kaOD44aFIQPNoFLLg4BgUaCH4F4Y4kZAQEB?= X-IronPort-AV: E=Sophos;i="5.33,432,1477954800"; d="scan'208";a="206694233" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 02 Jan 2017 14:51:54 +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 71C81638C for ; Mon, 2 Jan 2017 22:51:51 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172.math.nagoya-u.ac.jp [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id EB97F415F; Mon, 2 Jan 2017 22:51:49 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=h4s3A5ERovCTwr6hVXRY4H96Tic=; b=0IBa9aCZ9WTsNkM0kPO6OH2ZXz9O woXsj22vkWYzcROdP5jmopSbLNpAexu4YNbhMTkCOvg/2JmFcq2g2JCPYGWq9iYw bUCoKsZXJHnE7S1HJ9QyPpDR8irZGqvNRLb0Gv7xDBjqy2wyzeSfIJPPmH3tjXDf ukcfWg9AEjVgjeo= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=Tjpj/cE4YuMOtiT0kssRDhhClOuInmHlMNEXAaiHh/l0xoQQzXc6R1cdbYIVsUTGOm+B5D2AsoqpNcQgy7MXs0HP0qFW1U7u7nW5KyL687TwiU7Cq1Obzbc3xk10+pJPybmB1E4B/lLakhKcbt9gK3tghjdUCbOqI8qez/n7ejw=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 3975A4F3; Mon, 2 Jan 2017 22:55:36 +0900 (JST) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Jacques Garrigue In-Reply-To: Date: Mon, 2 Jan 2017 22:51:59 +0900 Cc: OCaML List Mailing Content-Transfer-Encoding: quoted-printable Message-Id: <196E26F9-81AD-4899-A7E5-FC572D985319@math.nagoya-u.ac.jp> References: To: Anton Bachin X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] GADT+polymorphic variants quirk Let us just say that using polymorphic variant or object types as indices of GADTs are not explicitly supported. In your case, it seems that the problem is that unification including abstract rows does not work correctly. This can be classified as a (known) bug, but it is not clea= r yet when we will fix it. I would suggest avoid using polymorphic variants here, using rather a simple encoding: type whole =3D Whole type general =3D General type _ num =3D | I : int -> _ num | F : float -> general num This should avoid these problems without any real loss of expressivity. Jacques Garrigue On 2016/12/28 05:04, Anton Bachin wrote: >=20 > Hello, >=20 > Consider this code for simulating an ad-hoc polymorphic addition > function: >=20 > type whole =3D [ `Integer ] > type general =3D [ whole | `Float ] >=20 > type _ num =3D > | I : int -> [> whole ] num > | F : float -> general num >=20 > module M : > sig > val add : ([< general ] as 'a) num -> 'a num -> 'a num > val to_int : whole num -> int > val to_float : general num -> float > end =3D > struct > let add : type a. a num -> a num -> a num =3D fun a b -> > match a, b with > | I n, I m -> I (n + m) > | F n, I m -> F (n +. float_of_int m) > | F n, F m -> F (n +. m) > | _ -> > (* ----NOTE---- *) > match b, a with > | F m, I n -> F (float_of_int n +. m) > | _ -> assert false >=20 > let to_int : whole num -> int =3D fun (I n) -> n >=20 > let to_float =3D function > | I n -> float_of_int n > | F n -> n > end >=20 > let () =3D > M.add (I 1) (I 2) |> M.to_int |> Printf.printf "%i\n"; > M.add (I 1) (F 2.) |> M.to_float |> Printf.printf "%f\n" >=20 > Instead of the nested match expression (marked with (* NOTE *)), I would > have expected to just write >=20 > | I n, F m -> ... >=20 > However, if I actually do that, the result is an error on the expression > in the case: >=20 > Error: This expression has type general num > but an expression was expected of type a num > Type general =3D [ `Float | `Integer ] is not compatible with t= ype > a =3D [> `Integer ]=20 > The second variant type does not allow tag(s) `Float >=20 > While the reversed case type-checks successfully. I can imagine why this > would be so, but I want to ask the experts on the mailing list. >=20 > Is this a known quirk of the typechecker? A bug? Is there some > alternative syntax I am missing that would allow the I n pattern to be > written first? >=20 > Note that there is a way to rewrite the nested match cases to avoid _ > and maintain the exhaustiveness check. I wrote them out as above for > clarity. The actual solution I have settled on for now is: >=20 > let add : type a. a num -> a num -> a num =3D fun a b -> > match a, b with > | I n, I m -> I (n + m) > | F n, I m -> F (n +. float_of_int m) > | _, F m -> > match a with > | I n -> F (float_of_int n +. m) > | F n -> F (n +. m) >=20 > Best, > Anton >=20 >=20 > P.S. If interested, the code was for this Stack Overflow question: >=20 > http://stackoverflow.com/questions/41214000 >=20 > answer: >=20 > http://stackoverflow.com/a/41334879/2482998