From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 A4D1A800B6 for ; Tue, 3 Jan 2017 16:22:01 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=antronbachin@gmail.com; spf=Pass smtp.mailfrom=antronbachin@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f66.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of antronbachin@gmail.com) identity=pra; client-ip=209.85.214.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="antronbachin@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of antronbachin@gmail.com designates 209.85.214.66 as permitted sender) identity=mailfrom; client-ip=209.85.214.66; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f66.google.com) identity=helo; client-ip=209.85.214.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="antronbachin@gmail.com"; x-sender="postmaster@mail-it0-f66.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AxnyRJRKTsfV8EHJ0ptmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgUKfzxwZ3uMQTl6Ol3ixeRBMOAuq4C0rGd7PyoGTRZp83e4DZaKN0EfiRGoP?= =?us-ascii?q?tVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?dazdU7TfhMWv1u2054abI0AR3GL8MvtOK0CQrAHK/uMbiohvMO5lzBrNuT1Cdu?= =?us-ascii?q?9VyHlAL1OUhgv14Nv24ZhitiRduv4s88RNS6q8c6luHpJCCzFzGmYp48ujnxDI?= =?us-ascii?q?TQqJri8VVHkMlRxCCgPF7RfSUZL4sy+8ve14jnrJdfbqRKw5DGzxp5xgTwXl3W?= =?us-ascii?q?Jeb2Y0?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A1AACHwGtYZ0LWVdFdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgmclAQEBAQEfgWuiHZMMhBeGIgKBR0IRAQEBAQEBAQE?= =?us-ascii?q?BAQESCwsLBx0ygjMEARUBBIIXAQQBIwQZARsdAQMBCwYFCw8CJgICIQIRAQUBH?= =?us-ascii?q?AYTG4g5AQMQCAGiUD+MAoFrGAUBHIMJBYNUChknDVSCNQEBAQEBAQEBAQEBAQE?= =?us-ascii?q?BAQEBAQEBARUCBgkBCHmHPAiCV4JOgXiDBC2CMAWQAopGNY1Fg3mKFYZAiXOEJ?= =?us-ascii?q?4JdMoEUNYEpUQ4BA4FDgX+CKFOGb4FPAQEB?= X-IPAS-Result: =?us-ascii?q?A0A1AACHwGtYZ0LWVdFdGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgmclAQEBAQEfgWuiHZMMhBeGIgKBR0IRAQEBAQEBAQEBAQESCwsLBx0yg?= =?us-ascii?q?jMEARUBBIIXAQQBIwQZARsdAQMBCwYFCw8CJgICIQIRAQUBHAYTG4g5AQMQCAG?= =?us-ascii?q?iUD+MAoFrGAUBHIMJBYNUChknDVSCNQEBAQEBAQEBAQEBAQEBAQEBAQEBARUCB?= =?us-ascii?q?gkBCHmHPAiCV4JOgXiDBC2CMAWQAopGNY1Fg3mKFYZAiXOEJ4JdMoEUNYEpUQ4?= =?us-ascii?q?BA4FDgX+CKFOGb4FPAQEB?= X-IronPort-AV: E=Sophos;i="5.33,455,1477954800"; d="scan'208";a="252695854" Received: from mail-it0-f66.google.com ([209.85.214.66]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Jan 2017 16:22:00 +0100 Received: by mail-it0-f66.google.com with SMTP id c20so50790463itb.0 for ; Tue, 03 Jan 2017 07:22:00 -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=7p/o8tYT7v9eIXDv6L9eq1wGJ0C0sU2s67hc0g4t2RE=; b=a29oY/AP7X1k+p0maPC7zlKzixPvkXSwme0y6zzeWkHl0tkgW0AHzJaFEtT2CD1yRq X0nU97agYVEqFvx2Ywn1/fJwL8rry6kLoeFPZPcKIb2K+qkzPQ6GEfDqRfVBaMvGdmk8 jr/3aNoqZoLqaXtbhyhyy2V429yW496L/JIT3hGfalIgjhOSZkaU/+RWkTjitPN40kPi nTo01ac3X+v3+6TchNz0Qe4a5qzL3OXfFXal72ZazL8ZS2tqwNeD4jk4FIwYqaAozcJd mNnxYNSiX1NlP8c5f4LPnrO6+FCOyh62+0uaRkt3al4g9sgTkfNK4sjVkJPqXkV8V3+I YmeA== 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=7p/o8tYT7v9eIXDv6L9eq1wGJ0C0sU2s67hc0g4t2RE=; b=KthlDkpafof1IbRWXfFHFsqmaD1xny+woPVch2/94eCCB7/u1ovUzKSSSzNBTCE8Hn Ioev7lsiuF1y9LDJMSOzwz9V6L8ZP4ujSXIbysHXGDdx7Htifbpya+IYoavuCwEXbnkZ nnlYPpqG/J549m4oR3krqy0JcXOGhQ/40/wOpfzAAmWA6TwGKCmTQippuZPIVoL4J2Ay RG4z4PEFd95bkQJCNTDhDnITmLr74oE6elAmnrQ/+2HqzSQgGx9/O3FoKirkZPetLBnY 3JB5Zx3E2ohSM4B/jpWS2+ByUdGnS9n6IzWPM1Y3TUX+SGQ/fybdNfXQtakBSu0C12YC 6/Fg== X-Gm-Message-State: AIkVDXLmLwtIKM3VOJYMQFoyoyIghX+udZNnWhktjeJFZ/Bu/R/sYUWSoq7oIX7iq72DNg== X-Received: by 10.36.237.3 with SMTP id r3mr48521177ith.76.1483456919321; Tue, 03 Jan 2017 07:21:59 -0800 (PST) Received: from ?IPv6:2601:240:c600:8bd0:dc65:17eb:cb56:2d7? ([2601:240:c600:8bd0:dc65:17eb:cb56:2d7]) by smtp.gmail.com with ESMTPSA id o65sm33857676ioe.15.2017.01.03.07.21.58 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 03 Jan 2017 07:21:58 -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: <3B567A59-09E1-46B7-8C34-149B886345FD@gmail.com> Date: Tue, 3 Jan 2017 09:22:01 -0600 Cc: "caml-list@inria.fr" X-Mao-Original-Outgoing-Id: 505149721.077115-674bb09a57529f539bc8aae64db497ae Content-Transfer-Encoding: quoted-printable Message-Id: <035A01D7-2424-478A-9C0A-2285AF1F7B5B@gmail.com> References: <40536bf7-5d7f-5528-80c2-45ed5d157d00@bioquant.uni-heidelberg.de> <3B567A59-09E1-46B7-8C34-149B886345FD@gmail.com> To: Nils Becker X-Mailer: Apple Mail (2.2070.6) Subject: Re: [Caml-list] GADT+polymorphic variants quirk I suppose one improvement to that assert false case would be to use R _ for the pattern instead of _, but it=E2=80=99s not the ultimate solutio= n. > El ene 3, 2017, a las 9:09, Anton Bachin escribi= =C3=B3: >=20 > Nils, actually, you can get the expanded M to typecheck as well: >=20 > type integer =3D [ `Integer ] > type rational =3D [ integer | `Rational ] > type real =3D [ rational | `Real ] >=20 > type _ num =3D > | N : int -> [> integer ] num > | Q : int * int -> [> rational ] num > | R : float -> real num >=20 > module M : > sig > val mult : ([< real] as 'a) num -> 'a num -> 'a num >=20 > 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) >=20 > (* 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) >=20 > (* When b =3D R _, the second pattern decides the type of the resul= t, > 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)) >=20 > let to_int : integer num -> int =3D fun (N n) -> n >=20 > let to_num_denom : rational num -> int * int =3D function > | N n -> (n, 1) > | (Q (n, n')) -> (n, n') >=20 > 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 >=20 > let () =3D > M.(mult (R 2.) (Q (3, 2)) |> to_float) |> Printf.printf "%f\n=E2=80= =9D >=20 > 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 = take > this, and keep in mind Jacques=E2=80=99 warning, but there it is :) >=20 > Best, > Anton >=20