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 0C7327EE9C for ; Fri, 25 Nov 2016 17:42:15 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f196.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.216.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.216.196 as permitted sender) identity=mailfrom; client-ip=209.85.216.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@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-qt0-f196.google.com) identity=helo; client-ip=209.85.216.196; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-qt0-f196.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AAN/ZuRBFxDyooWL5ut6FUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPX6r8bcNUDSrc9gkEXOFd2CrakV0KyN6euwASQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9GiTe5b75+Nhu7oRveusQVnYdpN7o8xAbOrnZUYe?= =?us-ascii?q?pd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbY?= =?us-ascii?q?VguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLzhS?= =?us-ascii?q?wZKzA27n3Yis1ojKJavh2hoQB/w5XJa42RLfZyY7/Rcc8fSWdHWclfSjFBApik?= =?us-ascii?q?b4QRE+UBIehWr474p1QUrBu+AxSnCOfgxzJMg3P727Ax3eY8HgHcxAEvHdwOvn?= =?us-ascii?q?Taotv2KakcT/y6wqbTwDXfdvNbwyvx5JTUfh0jp/yHQLJ+cdDWyUkqDw7LiU+f?= =?us-ascii?q?qZbmPzOIzeQGrm+V7+18VeKzj24stgZ8oj21ycc2iYnJm5kVxkrB9SV+3IY1Od?= =?us-ascii?q?m4RVV0Yd6hCpRQtiWaO5FqTcMlRmFloSA3waAIt568eSgF0pUnxxjHZvyGdYiI?= =?us-ascii?q?+BPjW/yLLTd2nnJpYL2/hxeu8Uig1+3zTdO430pNripAitXNtmoC1xzU6siAUP?= =?us-ascii?q?dy4kCh2TOX2wDU9u5LO0U0la7BJ54gxL4wmJ0TvELeFSH1gEX7lLGaelkg9+Sy?= =?us-ascii?q?6OnqYq/qqoGBO4J1kA3yL6Ajl825DO8lKAYBRXKb9v651LD7/U32XrFKjvoun6?= =?us-ascii?q?ncqp/aJMAbqregAw9Jzoov8hi/Ayqi3dkZh3UHI1VFeBWIj4jtJV7COuz3DfC6?= =?us-ascii?q?g1i0kTdrwe7JPqH5D5nTMnTOlK3tcLV95kJG1gY/0NFS64hJBrwFIf//Qkrxu8?= =?us-ascii?q?bZDh89PQy02eHnCNBl24MbQ22PGKyZML7JsVOS4+IvJPWMZJMRuDvmJPgl4uTh?= =?us-ascii?q?jX49mVMHYaap2p4XZGiiHvt6O0WZfWbsgtAZHGgWpAU+SejqhESGUT5SfHayQ7?= =?us-ascii?q?kx5io7CYKjFYfMXJqhgL2H3CehH51ZfHpKCl6WESSgS4LRav4WbyTaB85niT8V?= =?us-ascii?q?HeywTo4nzhK/nA3zzbd8MvDZ9zFevpXmgotb/erWwDQ77z9pFIy41H2RSykgm2?= =?us-ascii?q?oSRCItmqV4vVB54liG2Kl8xfdfEIoAtLtyTg4mOMuEnKRBANfoV1eEI46E?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CNAABLaThYhsTYVdFUCh0GDBgBAQQBA?= =?us-ascii?q?QoBAYMNAQEBAQE9OoECB40+lxmCN5I9gggdC4V5AoFbBz8UAQEBAQEBAQEBAQE?= =?us-ascii?q?SAQEBCAsLCR0wgjMaghwBAQQBAg8RBBkBFAcSCwEDDAYFCwMKAgIJGgMCAiEBA?= =?us-ascii?q?REBBQEKAREGExIIAQeIMAEDFw6dYIEyPzKLUIFsGAUBH4MNBYNWChknAwpUgzY?= =?us-ascii?q?BAQEBAQEEAQEBAQEBARgCBhJ5hTOEW4JIgVkogwSCXQWGNlIMiFmKMjWBdoRSh?= =?us-ascii?q?h9Jg1aCCTiNcYlAhDGCSBMegRMegSxAEYMmEQuBeyA0AYg2AQEB?= X-IPAS-Result: =?us-ascii?q?A0CNAABLaThYhsTYVdFUCh0GDBgBAQQBAQoBAYMNAQEBAQE?= =?us-ascii?q?9OoECB40+lxmCN5I9gggdC4V5AoFbBz8UAQEBAQEBAQEBAQESAQEBCAsLCR0wg?= =?us-ascii?q?jMaghwBAQQBAg8RBBkBFAcSCwEDDAYFCwMKAgIJGgMCAiEBAREBBQEKAREGExI?= =?us-ascii?q?IAQeIMAEDFw6dYIEyPzKLUIFsGAUBH4MNBYNWChknAwpUgzYBAQEBAQEEAQEBA?= =?us-ascii?q?QEBARgCBhJ5hTOEW4JIgVkogwSCXQWGNlIMiFmKMjWBdoRShh9Jg1aCCTiNcYl?= =?us-ascii?q?AhDGCSBMegRMegSxAEYMmEQuBeyA0AYg2AQEB?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="201737830" Received: from mail-qt0-f196.google.com ([209.85.216.196]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 17:42:13 +0100 Received: by mail-qt0-f196.google.com with SMTP id n34so4546205qtb.3 for ; Fri, 25 Nov 2016 08:42:13 -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=IG7jg5T7nN3YnylMngNlaS9/KMTjAGiYAIctIfHtA9Y=; b=AX5qZfMsf0XBdYJZnsbuN97ord14zr7cN4srt+f+WgSG8fVxogy74A9GmjW4EhfkFo mtDrCV5wQtXzQpHOvV5XdlPxxLtHaBWEJOUv95KNRqqn9mlM2atXJwYZ+MdzSBDkcMzD kzOuwuKRi/fDxKYbBEz2VbiB7WElMOLEikVy65yg+NJbXNMhMd/XvGcYcy40XddJ+Y0O CXVhET9nzw5k6rX1HQagbdI8MpR4LdMuaJthn1RxnUaR+AF8Zvzr3/bb5oSZYtTHAKg9 EJFv+bsfbo3NPS/82TX0dbXNGUXjQSuAQALq0Dzsbznxi16kPRv2p3o4zmzpw3qaCFnl /JWg== 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=IG7jg5T7nN3YnylMngNlaS9/KMTjAGiYAIctIfHtA9Y=; b=Nkhd5T+qYVjKbNLrMlWjVfjK4Lk0BkWB+yHNUtyjtEK3yUWE9rX61qKLIEddaWsuVf 9keXjwBk8RCzggOFo6cYtkc+gxIWMqq1aJ52o+iuBCld1lh7NT7eZ5rhm3hbRzGTcl9o oZH58fNw6Zw/S4tMu1cU4H0k+3h+zF14TM9Qk9svJ8WVkgoqMHSIl6kw7s0yg1Op+ysq fUwx1HtVV7Vbn3FUOMAp8eBK2AfflhwLivZL8942Lh8gxTE4D+CEG97D60zlzMoh0Ouw QYW1uqoAQpj9Dr+rJiLBv2VY2zVj35DnlmKGwLPzYZdXpTxFyXTKyDqna6dg6St1zN4p 3xXA== X-Gm-Message-State: AKaTC01952V+8uim++yyFNLNgk+8my+qVWpxU2OnBSZGYsfuIPwHjKWNhL/9I7UGG7fYWPacIkkqzVDJbvKMjA== X-Received: by 10.200.40.204 with SMTP id j12mr7863703qtj.284.1480092132171; Fri, 25 Nov 2016 08:42:12 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.129.98 with HTTP; Fri, 25 Nov 2016 08:42:11 -0800 (PST) In-Reply-To: References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Markus Mottl Date: Fri, 25 Nov 2016 11:42:11 -0500 Message-ID: To: Yaron Minsky Cc: Gabriel Scherer , Andreas Rossberg , 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 Interesting, somehow it had escaped my attention that match case elimination also applies to ordinary sum types if they have GADT arguments. I thought that this was only supported for GADTs. In that case the "nothing" approach, though requiring an explicit type annotation, might be an even neater solution. I wonder whether the type checker could be made to identify such match case elimination opportunities with the previously mentioned "empty" and "void" type definitions, too, which are obviously unpopulated. On Fri, Nov 25, 2016 at 10:59 AM, Yaron Minsky wro= te: > For what it's worth, Core_kernel's Nothing.t type is an impossible > type in Gabriel's sense. It effectively uses this pattern: > > module Equal =3D struct > type (_,_) t =3D Equal : ('a,'a) t > end > > type nothing =3D (unit,int) Equal.t > > let f (x:(unit,nothing) result) =3D > match x with > | Ok () -> () > > On Fri, Nov 25, 2016 at 10:46 AM, Gabriel Scherer > wrote: >>> Isn=E2=80=99t [an abstract type definition] a sufficiently convenient w= ay to define an empty type? >> >> It is not, because this is treated as a type whose definition is >> unknown, rather that as a type that is known to have no inhabitant. >> This is of course the only possible interpretation when (type empty) >> occurs in a signature/declaration; but I think that having abstract >> definitions be interpreted essentially as abstract declarations is >> good design -- although I'm not completely sure how close exactly the >> type-checker considers them today. >> >> I also believe that this kind of declarations is used to define types >> populated by the FFI -- with values coming from C -- which justifies >> this stricter interpretation. >> >> I forgot to point out, in my message above, that the (Error _ -> .) >> case expresses intent, but is not necessary as the type-checker (in >> recent OCaml versions) understands that the pattern-matching without >> this case is exhaustive. One way to notice the difference is to try >> with Andreas' definition, which the type-checker complains about: >> >> # type empty;; >> # let extract : ('a, empty) result -> 'a =3D function Ok x -> x;; >> Warning 8: this pattern-matching is not exhaustive. >> Here is an example of a case that is not matched: >> Error _ >> val extract : ('a, empty) result -> 'a =3D >> >> On Fri, Nov 25, 2016 at 8:52 AM, 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? >>> >>> /Andreas >>> >>>> (It used to be possible using the revised syntax, which uses >>>> braces to delimit (non-polymorphic) variant definitions, but this was >>>> ruled out by sanity checks introduced in OCaml 4.02). >>>> >>>> One way is to use GADTs to create an impossible type: >>>> >>>> type 'a onlybool =3D Bool : bool onlybool >>>> type empty =3D int onlybool >>>> >>>> let extract : ('a, empty) result -> 'a =3D function Ok x -> x >>>> >>>> Since 4.03 (April 2016), it is possible to explicitly write a >>>> so-called "refutation case", of the form " -> .", to say that >>>> a given case cannot happen -- it is an error if the type-checker >>>> cannot verify it: >>>> >>>> https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec241 >>>> >>>> let extract : ('a, empty) result -> 'a =3D function >>>> | Ok x -> x >>>> | Error _ -> . >>>> >>>> I would support the idea of having a built-in "empty" type to >>>> represent a variant type with no constructor -- but then I am probably >>>> biased in favor of the empty type. >>>> >>>> >>>> On Fri, Nov 25, 2016 at 8:01 AM, Julien Blond = wrote: >>>>> Yes, i knew the variant constructor but, somehow i didn't realize i w= as >>>>> precisely using it for my mind was focused on the polymorphic variant= list >>>>> :) >>>>> >>>>> In fact, i wondered if a generic result type like this >>>>> >>>>> type ('a, 'b) result =3D Ok of 'a | Error of 'b >>>>> >>>>> that we can see in several library could be used to specify a "safe" = result >>>>> which could have type something like ('a, []) result. One could encod= e 'b as >>>>> some error list at type level but it needs some complicated type mana= gement >>>>> and i'm targeting OCaml beginners for which i just want them to be ca= reful >>>>> about non nominal results. >>>>> >>>>> >>>>> 2016-11-25 12:22 GMT+01:00 David Allsopp : >>>>>> >>>>>> Julien Blond wrote: >>>>>>> 2016-11-25 9:39 GMT+01:00 Julien Blond : >>>>>>> Hi, >>>>>>> Let's try something : >>>>>>> $ ocaml >>>>>>> OCaml version 4.03.0 >>>>>>> >>>>>>> # let _ : [] list =3D [];; >>>>>>> Characters 9-10: >>>>>>> let _ : [] list =3D [];; >>>>>>> Error: Syntax error >>>>>>> # type empty =3D [];; >>>>>>> type empty =3D [] >>>>>>> # let _ : empty list =3D [];; >>>>>>> - : empty list =3D [] >>>>>>> # >>>>>>> >>>>>>> Does anyone know if there is a reason to forbid the empty polymorph= ic >>>>>>> variant >>>>>>> set in type expressions or if it's a bug ? >>>>>> >>>>>> As you've observed, [] is a variant constructor since 4.03.0 - see G= PR#234 >>>>>> (https://github.com/ocaml/ocaml/pull/234). The GPR contains referenc= es and >>>>>> comments as to the motivation for this. >>>>>> >>>>>> What's your desired use for the type of the non-extensible empty >>>>>> polymorphic variant? >>>>>> >>>>>> Possibly related, you can define a general type for a list of polymo= rphic >>>>>> variants: >>>>>> >>>>>> let (empty : [> ] list) =3D [] >>>>>> >>>>>> or >>>>>> >>>>>> let (length : [> ] list -> int) =3D List.length;; >>>>>> length [`Foo; `Bar];; >>>>>> length [42];; >>>>>> >>>>>> if that's what you were after? >>>>>> >>>>>> >>>>>> David >>>>> >>>>> >>>> >>>> -- >>>> Caml-list mailing list. Subscription management and archives: >>>> https://sympa.inria.fr/sympa/arc/caml-list >>>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >>>> Bug reports: http://caml.inria.fr/bin/caml-bugs >>> >> >> -- >> Caml-list mailing list. Subscription management and archives: >> https://sympa.inria.fr/sympa/arc/caml-list >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >> Bug reports: http://caml.inria.fr/bin/caml-bugs > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com