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 A9DED7EE9C for ; Fri, 25 Nov 2016 17:50:21 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stedolan@stedolan.net; spf=None smtp.mailfrom=stedolan@stedolan.net; spf=None smtp.helo=postmaster@mail-wj0-f174.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=pra; client-ip=209.85.210.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=mailfrom; client-ip=209.85.210.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wj0-f174.google.com) identity=helo; client-ip=209.85.210.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="postmaster@mail-wj0-f174.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Ar4r/khWSEr+BNdXuBKRJ6kgzKLzV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZhaFt8tkgFKBZ4jH8fUM07OQ6PG7HzdaqsbZ+DBaKdoXCE9D0Z?= =?us-ascii?q?1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f//6mI9pbSewRFgiamKfM3dU3u7FaZis5DqI1uMKs40VPzpWBTce?= =?us-ascii?q?lMyis8P1WIhBzx/MiY+YZitj9PoLQm7cEWAovgeKFtdqBVFDQrNSgZ48nis1GX?= =?us-ascii?q?VheC/nsRVCMalR5BBSDO6FfxV5K3uyC8q+kri3rSBtH/Ub1hAWfq1KxsUhK9zX?= =?us-ascii?q?5fbzM=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CsAACeajhYhq7SVdFeGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgmkkAQEBAQGBeQekV4dyjQKCCRwBh2AHQRIBAQEBAQE?= =?us-ascii?q?BAQEBARIBAQEICwsJHTCCMwQBFQEEghYBAQEDAQECDxEdAQE3AQQLAQoEAQYNK?= =?us-ascii?q?gICIQESAQUBHAYTCBqIMQMPCAGda4EyPzKKaWeCKYMMAQEFhB8NKxqDRQwBHAg?= =?us-ascii?q?ShiyEW4JIhQWCXZokNYF2izqDVpAyiUCEMYJIEx6BEyUOgRdAEQKDFYIIcgGGZ?= =?us-ascii?q?4FPAQEB?= X-IPAS-Result: =?us-ascii?q?A0CsAACeajhYhq7SVdFeGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgmkkAQEBAQGBeQekV4dyjQKCCRwBh2AHQRIBAQEBAQEBAQEBARIBAQEIC?= =?us-ascii?q?wsJHTCCMwQBFQEEghYBAQEDAQECDxEdAQE3AQQLAQoEAQYNKgICIQESAQUBHAY?= =?us-ascii?q?TCBqIMQMPCAGda4EyPzKKaWeCKYMMAQEFhB8NKxqDRQwBHAgShiyEW4JIhQWCX?= =?us-ascii?q?ZokNYF2izqDVpAyiUCEMYJIEx6BEyUOgRdAEQKDFYIIcgGGZ4FPAQEB?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208,217";a="246748323" Received: from mail-wj0-f174.google.com ([209.85.210.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 17:50:21 +0100 Received: by mail-wj0-f174.google.com with SMTP id mp19so63646239wjc.1 for ; Fri, 25 Nov 2016 08:50:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=stedolan-net.20150623.gappssmtp.com; s=20150623; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=b49aRLhBbJQXayHlZneoeQMSRr52Qz9p3JVvJDDbALs=; b=gTeiqO19ocpbVYHeUq+6Y7ZUAfXifq815hefbbVGMfmvFGCYH7p+fKX0H5bZqgnKW/ nN3b9cLz4i0vLxjqkLsXQgcir0h8zSgMDgddB9jaHCCjw0ev1Oa99+jGGVH4HZST7Z0s Sv6CFWLec0tWVEXgBwMO9IOqMIRZbrU308t13s6sPNtl9IDkhbRoBX9Jkxf+FogKZSfK Z4N79tbxN/eha8NWMbe6iThG2p938mqpc4za/e8FzyxleXqPAWcZgjsdA7aPcADsEO4m vng1HgfyX0jOI39S2ecfv28VK0ki8JffCfwsQCTj6Al/K/J/dAnnpsK40mprvYESuJSA 5Psg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to:cc; bh=b49aRLhBbJQXayHlZneoeQMSRr52Qz9p3JVvJDDbALs=; b=SODWOQqMqbqTzcZPFbZueFbPhCmfrE9IBj445VTzBkCccqG1cCzHTzGtFx/5rkSW25 zdwj5RK5OLEdqzkf9mGhBgCG8lJJmho9Fa5s9zVH5eflq7Cnn88aspjqkXRLcVb7LkvQ 0oXK6jGigDlbAUNrl6L4gs6qWZWN42M9kv16/72mQN4lZ2wd8cnzuAuMQFksWn7BHUcB D0BOKUjhM6RYvGVIPBJ6zqw2W53edA85q+6cwg5P5Pukju1YJWKO2rn3s26hEsr1/yT5 jKquhzzPZSuLNwERqZiiQIMzMzQoj9TfoAis+o36l9e0e7bI16pXC4+frhy6CpP6QFU/ PVIg== X-Gm-Message-State: AKaTC00Dqf99qtPlHy5YhrGH5quxRJLX//VDSmrZZro2v+YKNnb4rH79Ts8tATkiTlutCQx24pyzlSMIeXliyQ== X-Received: by 10.194.201.103 with SMTP id jz7mr9031986wjc.70.1480092620472; Fri, 25 Nov 2016 08:50:20 -0800 (PST) MIME-Version: 1.0 Sender: stedolan@stedolan.net Received: by 10.80.146.170 with HTTP; Fri, 25 Nov 2016 08:50:19 -0800 (PST) X-Originating-IP: [2001:630:212:238:ec4:7aff:fea9:f376] In-Reply-To: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Stephen Dolan Date: Fri, 25 Nov 2016 16:50:19 +0000 X-Google-Sender-Auth: tV26jSgsuv907V8R-CUOMmvGI1k Message-ID: To: Andreas Rossberg Cc: Gabriel Scherer , Julien Blond , David Allsopp , OCaml mailing-list Content-Type: multipart/alternative; boundary=047d7bae4384e0d17a054222ea92 Subject: Re: [Caml-list] Empty polymorphic variant set --047d7bae4384e0d17a054222ea92 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Fri, Nov 25, 2016 at 1:52 PM, Andreas Rossberg wrote: > > > On Nov 25, 2016, at 14:46 , Gabriel Scherer > wrote: > > > > I would agree that OCaml lacks a convenient way to define the empty > > type. > > Isn=E2=80=99t > > type empty > > (as a definition) a sufficiently convenient way to define an empty type? > I agree that that defines the empty type, but OCaml disagrees. OCaml takes that as declaring an abstract type, just as if you'd included a module exposing an opaque type. So, the compiler won't conclude that 'empty' is actually an empty type (viewing it as an unknown abstract type), nor will it refute (int, empty) eq. Stephen --047d7bae4384e0d17a054222ea92 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On F= ri, Nov 25, 2016 at 1:52 PM, Andreas Rossberg <rossberg@mpi-sws.org= > wrote:

> On Nov 25, 2016, at 14:46 , Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
>
> I would agree that OCaml lacks a convenient way to define the empty
> type.

Isn=E2=80=99t

=C2=A0 type empty

(as a definition) a sufficiently convenient way to define an empty type?

I agree that that defines the empty type,= but OCaml disagrees. OCaml takes that as declaring an abstract type, just = as if you'd included a module exposing an opaque type. So, the compiler= won't conclude that 'empty' is actually an empty type (viewing= it as an unknown abstract type), nor will it refute (int, empty) eq.
=

Stephen
--047d7bae4384e0d17a054222ea92--