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 58764800B7 for ; Tue, 3 Jan 2017 16:09:52 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=antronbachin@gmail.com; spf=Pass smtp.mailfrom=antronbachin@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f49.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of antronbachin@gmail.com) identity=pra; client-ip=209.85.214.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="antronbachin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of antronbachin@gmail.com designates 209.85.214.49 as permitted sender) identity=mailfrom; client-ip=209.85.214.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="antronbachin@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f49.google.com) identity=helo; client-ip=209.85.214.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="postmaster@mail-it0-f49.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AkQWXxxV3/tanDokbm6c8pK/uUvfV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbBWPt8tkgFKBZ4jH8fUM07OQ6PG8HzVbqsnY+Fk5M7V0Hycfjs?= =?us-ascii?q?sXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6?= =?us-ascii?q?KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG5oAnLq8Ubj4RuJ6QsxhDUvnZGZu?= =?us-ascii?q?NayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnD?= =?us-ascii?q?VhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0ji?= =?us-ascii?q?oMKiU0+3/LhMNukK1boQqhpx1hzI7SfIGVL+d1cqfEcd8HWWZNQsNdWipcCY2+?= =?us-ascii?q?coQPFfIMMvpXoIfgp1UBrxWwCwavCuPh1DFGgWT73bEj0+QkDQ3G3BAsEtAIvX?= =?us-ascii?q?/JrNv1LqASUeWtwaTUyzXDc/RW2THg44XVaB8uvfGMXbN2ccHMzkQgDQXFjkmK?= =?us-ascii?q?qYziOTOazf4CvHSb7+phU+KikGEnqwRrrTiuwscgkJXGhoUQyl3d8yhy3YU7Jc?= =?us-ascii?q?WgRUJlfdKpFIFcuiKaOodsXM8uXm5ltDw1x7ACoZK2fiYHxI4jyhLFafGKcZKE?= =?us-ascii?q?7g/hWeuTJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFl8PDtnEJ1xDK68iHVu?= =?us-ascii?q?dx8l6v2TuA0w3f8O5EIUczlarUL54u3KQ8mYYUsUTGBiP2mUP2g7GKdkg85OSk?= =?us-ascii?q?9+Dqbq/lq5KcLYN4lBzyP6s0lsGwBek0Kg0OUHKa+eS42r3j50r5QLBSg/IslK?= =?us-ascii?q?nZrIraJcMdpqGiGQBazoYj6xe5Dzq939QYmGMILFNBeB6dk4fpPFTOLOjiDfij?= =?us-ascii?q?m1SsjCtrx/feM7L9GJrNK3zDnK7lfbZ88E5c1BE+zctf5pJRErEOOuj/Wk73tN?= =?us-ascii?q?zCDx82KRa4w+j9CIY16oRLf2OLGeezPajRvEXAsuQuJ/LKboIeuzvnA/Ik4Ofz?= =?us-ascii?q?hHkl30IbfOyp0JobZXSyE+5pZUmUNynCmNAERE4Mog04BMbjg12DV3YHbnCuRa?= =?us-ascii?q?U67DgwCIOgJYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJJMXrKLw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CEAABrvWtYhjHWVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgwwBAQEBAYIKqwiKIYQXhiICgUdCEQEBAQEBAQEBAQEBEgEBAQg?= =?us-ascii?q?LCwkdMIIzGgGCGwYjBBkBGx0BAwwGBQsPAiYCAiMRAQUBHAaIZwEDGKJNP4wCg?= =?us-ascii?q?WsYBQEcgwkFg1QKGScNVII1AQEBAQEBAQEBAQEBAQEBAQEBAQEWAgYJAQh5hzy?= =?us-ascii?q?CX4RGgwQtgjAFkAKKe5E+ihUPhjGOGoJdMoEUNYEpUQ4BA4FDgX8ggghTiD4BA?= =?us-ascii?q?QE?= X-IPAS-Result: =?us-ascii?q?A0CEAABrvWtYhjHWVdFdHAEBBAEBCgEBFwEBBAEBCgEBgww?= =?us-ascii?q?BAQEBAYIKqwiKIYQXhiICgUdCEQEBAQEBAQEBAQEBEgEBAQgLCwkdMIIzGgGCG?= =?us-ascii?q?wYjBBkBGx0BAwwGBQsPAiYCAiMRAQUBHAaIZwEDGKJNP4wCgWsYBQEcgwkFg1Q?= =?us-ascii?q?KGScNVII1AQEBAQEBAQEBAQEBAQEBAQEBAQEWAgYJAQh5hzyCX4RGgwQtgjAFk?= =?us-ascii?q?AKKe5E+ihUPhjGOGoJdMoEUNYEpUQ4BA4FDgX8ggghTiD4BAQE?= X-IronPort-AV: E=Sophos;i="5.33,455,1477954800"; d="scan'208";a="206819722" Received: from mail-it0-f49.google.com ([209.85.214.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Jan 2017 16:09:51 +0100 Received: by mail-it0-f49.google.com with SMTP id o141so277586309itc.0 for ; Tue, 03 Jan 2017 07:09:51 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=VJY2dUay5IIGWyxjVfKo28nBXs8wcijDPhlApg8uaOA=; b=NhNEVCoC4l5AYMGUEJXWqE9QLwuNa/em4ocPZ1Hklj9J+MTkOHe5Y2v+6LtDJYdPEO PPBHY0lb9yA/TnhuWhEw3VV9k0OpXuRbPrKGQXLkAJ1sFLotz/aliOZJQsgwkJQQJe1n BKtLaX1/jq7aGFRRMiEEsndBMyo1gEg/+HVga+LpDWKi0cUzUQ51cV7dxjvnt7tSO6ku kD41q/TYSA14PLqc1e82AorbkAlrrVtmADfR3WuB7vv+w9Fz1LBa/ekOqUzkcp1x7TTl Hb7e/Fw8il/MhoJWeGbcf5GnbreTrbf839eG9wJxlAm1d5PrYjJH/FpzoRNjsoiaYlaD Sdow== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=VJY2dUay5IIGWyxjVfKo28nBXs8wcijDPhlApg8uaOA=; b=OouRs0CeTgicpwxew1GD4ue2fWnAtZZL+MfRIc3OkXW/KvX334AgUNX+rmFcpr8VCr 8cCEomfgMZih0CmkEZ1B7FD/Q6W75UX4qR2vgTxINl7vhSiq5FROo2No16/RwbuRetOh rlP+aAFAQNUBrwkl0OP+NhbC0uR/9VjXjlnoK+ZaQR0b24iOu20mpWKXFBmE5TgROGie 5iZBFiK1bt1eqKNIb6Aag6J3UiztMEhxKvAD+PPhsCZRu7NXkr+cObRqQzxICpkxm1tz XxDjw3vwN/DkAFc8dk4E4xuuz516bzGztEbNLbdV4QKnKkxtgGKHI3rsAB+dv4iA7I/7 fRwA== X-Gm-Message-State: AIkVDXIcTSwWeSKKg2+7f4+ghTO8USkGzCch+f4l1fdQWv4WHSu8mLD4+wKeQodT7xCS8w== X-Received: by 10.36.85.151 with SMTP id e145mr48357776itb.15.1483456189922; Tue, 03 Jan 2017 07:09:49 -0800 (PST) Received: from [192.168.0.4] (c-73-9-77-177.hsd1.il.comcast.net. [73.9.77.177]) by smtp.gmail.com with ESMTPSA id a18sm32480662itd.18.2017.01.03.07.09.48 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 03 Jan 2017 07:09:49 -0800 (PST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2070.6\)) From: Anton Bachin In-Reply-To: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> Date: Tue, 3 Jan 2017 09:09:51 -0600 Cc: "caml-list@inria.fr" X-Mao-Original-Outgoing-Id: 505148991.391314-2a394175ee6c406ec857d92f16ad59e6 Content-Transfer-Encoding: quoted-printable Message-Id: <3B567A59-09E1-46B7-8C34-149B886345FD@gmail.com> References: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> To: Nils Becker X-Mailer: Apple Mail (2.2070.6) Subject: Re: [Caml-list] GADT+polymorphic variants quirk Nils, actually, you can get the expanded M to typecheck as well: type integer =3D [ `Integer ] type rational =3D [ integer | `Rational ] type real =3D [ rational | `Real ] type _ num =3D | N : int -> [> integer ] num | Q : int * int -> [> rational ] num | R : float -> real num module M : sig val mult : ([< real] as 'a) num -> 'a num -> 'a num val to_int : integer num -> int val to_num_denom : rational num -> int * int val to_float : real num -> float end =3D struct let mult : type a. a num -> a num -> a num =3D fun a b -> match a, b with (* When b =3D N _, the first pattern decides the type of the result.= *) | N n, N m -> N (n * m) | Q (n, n'), N m -> Q (n * m, n') | R n, N m -> R (n *. float_of_int m) (* This case must be here, not inside the b =3D Q _ nested match expression, to ensure that the typechecker sees real num before [> rational ] num. *) | R n, Q (m, m') -> R (n *. float_of_int m /. float_of_int m') (* These are cases in which we want the typechecker to see b =3D Q _ first. *) | _, Q (m, m') -> (match a with (* Harder to get an exhaustiveness check here, didn't fully think through it. *) | N n -> Q (n * m, m') | Q (n, n') -> Q (n * m, n' * m') | _ -> assert false) (* When b =3D R _, the second pattern decides the type of the result, and that type is real num. *) | _, R m -> (match a with | N n -> R (float_of_int n *. m) | R n -> R (n *. m) | Q (n, n') -> R (float_of_int n /. float_of_int n' *. m)) let to_int : integer num -> int =3D fun (N n) -> n let to_num_denom : rational num -> int * int =3D function | N n -> (n, 1) | (Q (n, n')) -> (n, n') let to_float =3D function | N n -> float_of_int n | Q (n, n') -> float_of_int n /. float_of_int n' | R n -> n end let () =3D M.(mult (R 2.) (Q (3, 2)) |> to_float) |> Printf.printf "%f\n=E2=80=9D I added some comments in the match expressions to try to clarify why they must be written as above. The scheme is, while unifying the patterns, you want the first pattern the typechecker encounters to have the same type as the result. Again, I=E2=80=99m not sure how far you can ta= ke this, and keep in mind Jacques=E2=80=99 warning, but there it is :) Best, Anton