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 407A17EE9C for ; Fri, 25 Nov 2016 17:59:42 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f195.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yallop@gmail.com) identity=pra; client-ip=209.85.216.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yallop@gmail.com designates 209.85.216.195 as permitted sender) identity=mailfrom; client-ip=209.85.216.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="yallop@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-qt0-f195.google.com) identity=helo; client-ip=209.85.216.195; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yallop@gmail.com"; x-sender="postmaster@mail-qt0-f195.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AXLOG7xRZY/fliQ8sJaD4U+KljNpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa64ZRGN2/xhgRfzUJnB7Loc0qyN4vumAjZLsc7J8ChbNscTB1ld0Y?= =?us-ascii?q?RetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1o?= =?us-ascii?q?Ora9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZwtnYZ6Kqs3gjfOpnJOM7?= =?us-ascii?q?BN2W5wJV+V2Rr74s621JVntS9ZvrQo/IhdUvOpUb4/SOl6AS4rNnF91cTvsR7b?= =?us-ascii?q?BV+e738YVX0+nR9BAgyD5xb/CMSi+hDmv/ZwjXHJdfb9Sqo5DHH7t/9m?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DBAADVbDhYhsPYVdFeDg4BAQQBAQoBA?= =?us-ascii?q?RcBAQQBAQoBAYMNAQEBAQGBeQekV5R0gggdhgQCgVsHQBMBAQEBAQEBAQEBARI?= =?us-ascii?q?BAQEICwsJHTCCMwQBFQEEghcBAQQBAg8RBBkBGx0BAwwGBQsNAgImAgIhAQERA?= =?us-ascii?q?QUBHAYTIogwAQMXnX6BMj8yi1CBbBgFAR+DDQWDVQoZJw1UgzYBAQEHAQEBARs?= =?us-ascii?q?CBhJ5ig6CSIIBgwSCXQWaHzWNMINWkDKJQIQxgkgTHoETIAKBKBMMIRGDFyCBL?= =?us-ascii?q?Ts+NAGGZ4FPAQEB?= X-IPAS-Result: =?us-ascii?q?A0DBAADVbDhYhsPYVdFeDg4BAQQBAQoBARcBAQQBAQoBAYM?= =?us-ascii?q?NAQEBAQGBeQekV5R0gggdhgQCgVsHQBMBAQEBAQEBAQEBARIBAQEICwsJHTCCM?= =?us-ascii?q?wQBFQEEghcBAQQBAg8RBBkBGx0BAwwGBQsNAgImAgIhAQERAQUBHAYTIogwAQM?= =?us-ascii?q?XnX6BMj8yi1CBbBgFAR+DDQWDVQoZJw1UgzYBAQEHAQEBARsCBhJ5ig6CSIIBg?= =?us-ascii?q?wSCXQWaHzWNMINWkDKJQIQxgkgTHoETIAKBKBMMIRGDFyCBLTs+NAGGZ4FPAQE?= =?us-ascii?q?B?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246749481" Received: from mail-qt0-f195.google.com ([209.85.216.195]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 17:59:41 +0100 Received: by mail-qt0-f195.google.com with SMTP id n6so4599088qtd.0 for ; Fri, 25 Nov 2016 08:59:41 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=jlzYjkaUbTbX0rZQNurGW0u4eaIRo41f4CnaQedSl1g=; b=BmsDEt2DCMgQr/76WYj9legwZYhhJ6d4pTRG/roV2aIKD9cMyDLCEaZAYrY0DD/bur HJsHhHi+c7Xk0hyqiPwdpmNR45tCwRNVJKIkeZ7ml+dJbYwr/gbf39aQmGi1li/7yf5m 07FPl24CM3rgO7dl3glUzOws7cVNrCtm/sXbcBKA3CYqAXafXj/Hz34kowoAHU+fmGiH CQky6skkOR9AH2W+qDcfoGZQPwrJLrqba9iW6xGxSfnkhcmgjAUpEjPjDxbe+s6XqatT MspioFGlxQXBWBMM6lZcAOfQuboQxrIZjoG0DnZOolJiCSsEwf8IyDJdbr1tjhW+iquN 0D7A== 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:content-transfer-encoding; bh=jlzYjkaUbTbX0rZQNurGW0u4eaIRo41f4CnaQedSl1g=; b=LgdbMhXo6om2+eaaEvZBC3D4A23CKybmS54Br00Pk8Q7m5BHSzwZSRjDCFbNZlb7y7 Ot0tTg3kdSFB1e7dXmruKrAZOn0yXU0sW1vE9Qj/K2/DssgoC0wzvz/L3gFwmGm25GvN EmzjWEVC8z1deTPWexsYrKjhcn9Ma931oyBvcI4iwFx+wY2/X6/ywoUE/xsXzgZLOmsX QiE7TMSPt5PLUhfVUE7FTx2jT24NoqMA8L7/faHaXsXMnAn4txnBGBITaX7MUNluqQ0o XrH4wRuAsbHHHJ0NtzAfuKbXkQ2XEPyyScsk5VBNeuAYByCZZsPJknoDGUWgajueNoc9 b5Ww== X-Gm-Message-State: AKaTC01d0SmuNmlQfp7EZjih54Y16aTp4Ha/7IWDVFeR5KSl0tdu3VRvqSMm7Hagf/J9MqDbugv1mq0gHoJYXA== X-Received: by 10.200.38.39 with SMTP id u36mr8546101qtu.31.1480093180444; Fri, 25 Nov 2016 08:59:40 -0800 (PST) MIME-Version: 1.0 Received: by 10.55.152.2 with HTTP; Fri, 25 Nov 2016 08:59:39 -0800 (PST) In-Reply-To: References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Jeremy Yallop Date: Fri, 25 Nov 2016 16:59:39 +0000 Message-ID: To: Stephen Dolan Cc: Andreas Rossberg , Gabriel Scherer , Julien Blond , David Allsopp , OCaml mailing-list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Empty polymorphic variant set On 25 November 2016 at 16:50, Stephen Dolan wr= ote: > 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. There's a small (and not enormously useful) distinction to be made here. If 'empty' is in the current module then OCaml knows that 'empty' and 'int' are incompatible, and so accepts the following program: type empty type (_,_) eql =3D Refl : ('a,'a) eql let f : (int, empty) eql -> unit =3D function _ -> . However, if 'empty' is defined in a different module ('M', say) then OCaml treats 'empty' and 'int' as compatible and so rejects the following (non-)program: type (_,_) eql =3D Refl : ('a,'a) eql let f : (int, M.empty) eql -> unit =3D function _ -> . Jeremy