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 C00F57EE9C for ; Fri, 25 Nov 2016 10:19:55 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bmillwood@janestreet.com; spf=Pass smtp.mailfrom=bmillwood@janestreet.com; spf=None smtp.helo=postmaster@mxout1.mail.janestreet.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of bmillwood@janestreet.com) identity=pra; client-ip=38.105.200.78; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of bmillwood@janestreet.com designates 38.105.200.78 as permitted sender) identity=mailfrom; client-ip=38.105.200.78; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.78; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AiipFth+wQlMZCv9uRHKM819IXTAuvvDOBiVQ1KB3?= =?us-ascii?q?0u0cTK2v8tzYMVDF4r011RmSDN6dsKsP1rqempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwtFiCCzbL9vIxm7rQbcvdQKjIV/Lao81gHHqWZSde?= =?us-ascii?q?RMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZ?= =?us-ascii?q?TQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhz?= =?us-ascii?q?kbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFOAI28?= =?us-ascii?q?YYsBAeQCIOhWsZXyqkAUoheiHwShHv/jxiNKi3LwwKY00/4hEQbD3AE4At8Brn?= =?us-ascii?q?LUp8jyOqcTVeC1yKfJzTLEb/xLxDzw75PHchUgofGIWbJxf83RyU4yGA7ejFWf?= =?us-ascii?q?s4rlMC2O1uQRqWiU8fRvVf61h2E7rAFxpyGiy8ExgYfKnoIY0l7J+CZjzIooOd?= =?us-ascii?q?G1SFR3bcC4HJdMrS2XNYh7Tts8T210vCs20L4LtJ6hcCQU1ZgqxwTTZv6af4WO?= =?us-ascii?q?/xntTvyeIS1ii3JgYL+/hwi98UynyuDkU8m131FKrjdZktXRrHwN0gbc6smDSv?= =?us-ascii?q?dn/EeuwzCP2B7I6uFYO0A7i7TUK4I7zrEskZoTtFzPHi7wmErokK+bbksp9+uy?= =?us-ascii?q?5+j6frnrpoWQO5Fohg3iKKgjmM+yDfw9MgcUXmib/eq81Kfk/U38WLhFlfg2kq?= =?us-ascii?q?jdsJDeK8Uboam5DBJO34Yh8Rm/CSmp0M8EnXkdMl1KZg6Hg5L1NFHJJfD0Fe2/?= =?us-ascii?q?jEi0kDd32/DGOaXsDYnXIXjGlLftZLJ9609HyAov1t1f/JJVCrQZIP3pQEPxtd?= =?us-ascii?q?rYDgU4MwOu2ernBs99hcsiXjetH6uYPaWam1uP4O5nd+uRYI4YvnD3L/8j69bh?= =?us-ascii?q?iHY4nRkWeqz/jrUNb3XtNPlga2CYZX7zhdANWTMAuws6SPPtj1GqUzdVam2uRa?= =?us-ascii?q?8x+ncwD4fwXtSLfZyknLHUhHTzJZZRfG0TTwnUSXo=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DfAAC5AThYfU7IaSZdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAYF5B6RWh3KHY4UfggiGIQKBegdBEgEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBCRYJTYIzGgGCGwEBAwESEQQZAQE3AQQLCQIEBzcCAiEBEgEFARwGEyKIM?= =?us-ascii?q?QMPCAOOaI9SgTI/MoppZ4FsPYMMAQEFhCENhAoBAQEBAQUBAQEBAQEBARcIEoY?= =?us-ascii?q?shFuCSIUFgl2OdnuKMzWNMINWkDKJQIQxgkgTHoETJQtTgQcRAoMVghVliDcBA?= =?us-ascii?q?QE?= X-IPAS-Result: =?us-ascii?q?A0DfAAC5AThYfU7IaSZdHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAYF5B6RWh3KHY4UfggiGIQKBegdBEgEBAQEBAQEBAQEBEgEBCRYJTYIzG?= =?us-ascii?q?gGCGwEBAwESEQQZAQE3AQQLCQIEBzcCAiEBEgEFARwGEyKIMQMPCAOOaI9SgTI?= =?us-ascii?q?/MoppZ4FsPYMMAQEFhCENhAoBAQEBAQUBAQEBAQEBARcIEoYshFuCSIUFgl2Od?= =?us-ascii?q?nuKMzWNMINWkDKJQIQxgkgTHoETJQtTgQcRAoMVghVliDcBAQE?= X-IronPort-AV: E=Sophos;i="5.31,546,1473112800"; d="scan'208,217";a="201669602" Received: from mxout1.mail.janestreet.com ([38.105.200.78]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 25 Nov 2016 10:19:54 +0100 Received: from tot-qpr-mailcore2.delacy.com ([172.27.56.106] helo=tot-qpr-mailcore2) by mxout1.mail.janestreet.com with esmtps (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.84_2) (envelope-from ) id 1cACfg-0004xo-Uk for caml-list@inria.fr; Fri, 25 Nov 2016 04:19:52 -0500 X-JS-Flow: external X-JS-Scanner-attachment: (ok) No attachments Received: by tot-qpr-mailcore2 with JS-mailcore (0.1) (envelope-from ) id BYOAI4-AAAEcB-b5; 2016-11-25 04:19:52.894540-05:00 Received: from mail-lf0-f71.google.com ([209.85.215.71]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1cACfg-0004QS-Nr for caml-list@inria.fr; Fri, 25 Nov 2016 04:19:52 -0500 Received: by mail-lf0-f71.google.com with SMTP id h201so24072308lfg.5 for ; Fri, 25 Nov 2016 01:19:52 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=PskQ1Kp+edNKH3TKzoCVpKabXhn7WZMrq0AjMDBl7pM=; b=qLBZY5s4Kcdl4jpMzgwSnINMpMXmBU4eImG8I0SBizDi6czQRh3C7ef8R+CNxoClnC TpQoCd/hH5BtJbf2ddejxO3KF2Fjh/OdwZDycyA2b4cgiO0SJ/wIpE6QCXL48MxK7584 CWyAUKDY2rm9UxfAor/mMdPECmzHI8cRptPzQ= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=PskQ1Kp+edNKH3TKzoCVpKabXhn7WZMrq0AjMDBl7pM=; b=Vx3dRbyQkDk0hpjxZJQ7tmJj1y8/U3hIR18h3f49rwERnLcrRwfaPj/k248hXDLPxH d4YHGfuJ/I9Wc/N4g433Bz2EtO+QbzV5m9jmpbDBoAxn8Y6LXNuTkYYwB50LjeW30YFT gynmN/ltnLzm3WS0KWa3soVLpeWkJSB4UJMpiGFhntt1yLpzu2nh4LH1H3xxhWeuRTFl Z3ndggHIorp3bT7YWqRIwVJICcd++Ma3geLRlQrkIqYS6BjdwfjLQsgq8klWaZP+VR6x 8oc4QFk4GQuQDrBt7WFZScKp25adKNAOsnEIX7eNl7A+9EDoB09VDjM90Q5cQCrvmmIG Z60g== X-Gm-Message-State: AKaTC01vXumocQ0LchpBCNHyezdd54p1R8zV/8BcsxwQS+q0gzz8D1mluINr036c1obttn26KpZQyYz68wVN0GzrBB7V+myEAWmuwmlhYgaZUNvLoLuBZpQ8S8K9u9vvJJPWYHFx7Bbb+lFSDVqF X-Received: by 10.25.29.8 with SMTP id d8mr2350128lfd.18.1480065591405; Fri, 25 Nov 2016 01:19:51 -0800 (PST) X-Received: by 10.25.29.8 with SMTP id d8mr2350117lfd.18.1480065591124; Fri, 25 Nov 2016 01:19:51 -0800 (PST) MIME-Version: 1.0 Received: by 10.25.216.137 with HTTP; Fri, 25 Nov 2016 01:19:30 -0800 (PST) In-Reply-To: References: From:Ben Millwood Date: Fri, 25 Nov 2016 17:19:30 +0800 Message-ID: To:Julien Blond Cc:OCaml mailing-list Content-Type: multipart/alternative; boundary=001a114020bacdc74805421c9f0c X-JS-Processed-by: mailcore X-Sender-Copy: hkg-copy Subject: Re: [Caml-list] Empty polymorphic variant set --001a114020bacdc74805421c9f0c Content-Type: text/plain; charset=UTF-8 After playing around with this for a little while, it looks to me like type t = [] isn't defining t as a synonym for the empty polyvariant, but rather defining t to be an ADT with one constructor, []. In particular, note that type t = [] type s = [] let f (x : s) : t = x (* does not typecheck *) type r = t = [] (* parses fine, showing [] is a constructor *) let f [] = () (* no exhaustivity warnings, inferred type is f : r -> unit *) It's odd that [] is a valid constructor name, but I suppose we want it so for lists, and might as well let other people reuse it. On 25 November 2016 at 16:39, Julien Blond wrote: > Hi, > > Let's try something : > > $ ocaml > OCaml version 4.03.0 > > # let _ : [] list = [];; > Characters 9-10: > let _ : [] list = [];; > > Error: Syntax error > # type empty = [];; > type empty = [] > # let _ : empty list = [];; > - : empty list = [] > # > > Does anyone know if there is a reason to forbid the empty polymorphic > variant set in type expressions or if it's a bug ? > > Regards, > > -- Julien Blond > --001a114020bacdc74805421c9f0c Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
After playing around with this for a little while, it look= s to me like

=C2=A0 =C2=A0 type t =3D []

<= /div>
isn't defining t as a synonym for the empty polyvariant, but = rather defining t to be an ADT with one constructor, []. In particular, not= e that

=C2=A0 =C2=A0 type t =3D []
=C2= =A0 =C2=A0 type s =3D []

=C2=A0 =C2=A0 let f (x : = s) : t =3D x (* does not typecheck *)

=C2=A0 =C2= =A0 type r =3D t =3D [] (* parses fine, showing [] is a constructor *)

=C2=A0 =C2=A0 let f [] =3D () (* no exhaustivity warni= ngs, inferred type is f : r -> unit *)

It's= odd that [] is a valid constructor name, but I suppose we want it so for l= ists, and might as well let other people reuse it.

On 25 November 2016 at 16:39, Julien= Blond <julien.blond@gmail.com> wrote:
Hi,

Let'= s try something :

$ ocaml
=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0 OCaml version 4.03.0

# let _ : [] list =3D [];;
C= haracters 9-10:
=C2=A0 let _ : [] list =3D [];;

Error: Syntax err= or
# type empty =3D [];;
type empty =3D []
# let _ : empty list = =3D [];;
- : empty list =3D []
#

<= div>
Does anyone know if there is a reason to forbid the empty polymorp= hic variant set in type expressions or if it's a bug ?

Regards,

-- Julien Blond

--001a114020bacdc74805421c9f0c--