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 B06E07EE9C for ; Fri, 25 Nov 2016 17:00:18 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yminsky@janestreet.com; spf=Pass smtp.mailfrom=yminsky@janestreet.com; spf=None smtp.helo=postmaster@mxout1.mail.janestreet.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yminsky@janestreet.com) identity=pra; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yminsky@janestreet.com designates 38.105.200.78 as permitted sender) identity=mailfrom; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.78; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Af2gszhZ0MItpeo/PJWf6Ad//LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZpci6bnLW6fgltlLVR4KTs6sC0LuN9fu6EjxYqdbZ6TZZL8wKD0dEwe?= =?us-ascii?q?wt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYn?= =?us-ascii?q?br+tQt2ap42N2uuz45zeZRlTzHr4OOsqbUaAlhjKrsQdnadlL68wzFOJ/ioJKK?= =?us-ascii?q?xqwjZHLFiJnhv4rvy7/JN5/j4Y7/0o/dRBXKG8ZK84QKZVFhwpNmk04IvgshyV?= =?us-ascii?q?HiWV4X5JY2wMlRwAJgnD9xLrFsPgtyr8rels8CuTO8DtUao5VCjk5KBuHky7wB?= =?us-ascii?q?wbPiI0pTmEwvd7i7hW9Vf8/hE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BKAADBXjhYfU7IaSZeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAXeBAgeNPpcZgjeFO40CgggdC4V5AoFaBz8UAQEBAQE?= =?us-ascii?q?BAQEBAQESAQEJFglNgjMEARUFghcBAQQBAg8RBBkBASwLAQ8LCw0CAgkaAwICI?= =?us-ascii?q?QESAQUBCgERBhMSCAiIMQMXAwudToEyPzKKaWeBbD2DDAEBBYQgAwqECgEBAQE?= =?us-ascii?q?BAQEBAQEBAQEBAQEBAQEWCBJ5hTOEW4JIggGDBIJdhw0MiFmKMjWGSIYfSYNWg?= =?us-ascii?q?gk4jXGJQIQxgkgTHoETHoEsEwwhEQKDFYImVAGGZ4FPAQEB?= X-IPAS-Result: =?us-ascii?q?A0BKAADBXjhYfU7IaSZeHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAXeBAgeNPpcZgjeFO40CgggdC4V5AoFaBz8UAQEBAQEBAQEBAQESAQEJF?= =?us-ascii?q?glNgjMEARUFghcBAQQBAg8RBBkBASwLAQ8LCw0CAgkaAwICIQESAQUBCgERBhM?= =?us-ascii?q?SCAiIMQMXAwudToEyPzKKaWeBbD2DDAEBBYQgAwqECgEBAQEBAQEBAQEBAQEBA?= =?us-ascii?q?QEBAQEWCBJ5hTOEW4JIggGDBIJdhw0MiFmKMjWGSIYfSYNWggk4jXGJQIQxgkg?= =?us-ascii?q?THoETHoEsEwwhEQKDFYImVAGGZ4FPAQEB?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246740130" Received: from mxout1.mail.janestreet.com ([38.105.200.78]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 25 Nov 2016 17:00:17 +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 1cAIvA-00064f-GC for caml-list@inria.fr; Fri, 25 Nov 2016 11:00:16 -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 BYOGAQ-AAAEcB-OF; 2016-11-25 11:00:16.452322-05:00 Received: from mail-ua0-f197.google.com ([209.85.217.197]) by mxgoog1.mail.janestreet.com with esmtps (UNKNOWN:AES128-GCM-SHA256:128) (Exim 4.72) (envelope-from ) id 1cAIvA-0004BM-C0 for caml-list@inria.fr; Fri, 25 Nov 2016 11:00:16 -0500 Received: by mail-ua0-f197.google.com with SMTP id b35so75868716uaa.1 for ; Fri, 25 Nov 2016 08:00:16 -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:content-transfer-encoding; bh=cAvpylDZZejjd9l8lew2Eztfm/OP6gMNBECuQyzdlzM=; b=S1wQYvwwUdcsSigPML2O1+tYGZDoWQzcPPs4ZNftsNeCP6s2N35VCneWDbQIid4FC+ GdOxd/J0j/CtOMV7uKro5WYekEu7oLaKOws6ISSqODt5Oila17J5jLGPAA2sHt/lJS6i wBb0mQ2noT/1RMauq8R+C6v/rXoPnGcRZlLgc= 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=cAvpylDZZejjd9l8lew2Eztfm/OP6gMNBECuQyzdlzM=; b=Ns18jN/QxzB3H0ofP+scTxFRWZb8p+DHc+HjExv6KQBwnx29qxypnClD2TpD/OVChG wDyk7Fmkv1+hXCFTv/DaDxKgpNquZm/ICWZGTV9vnloNTPSp5VscJd5bVsLMKZwc474x n3ALbuu7ZC+Md43j6WJI2TR44OqCM9p5Ajtj/leGH3WQEfIvpmZl4XPGMXGTbFRabwi8 aCI05uBYgLVT58/D/f6l4pGrqnEz1m7KGUW67f42lrzkctaYfyVNsQAhdZygCuu00t6c HgkaoBJBqpWK7oJQ4hIHD/k03CMsrD7q8hyXcbpbm4bNM+nbuGtmFB25IAxy+EXnCWjO pQhA== X-Gm-Message-State: AKaTC03VZoKMv8BP+CVXfOX2pxKGVPyjeQbaqvOR+kHWLI7iB6qOrvaRcP6qkudv5el0I1Vc6q0lZ3iHLbNU2NvxfJziwEwCgjFnFnl6zWSRDax9jctgaQOC5OuHGW9+45OVINH9RP4eaJiDKizL X-Received: by 10.176.64.234 with SMTP id i97mr5233246uad.7.1480089615802; Fri, 25 Nov 2016 08:00:15 -0800 (PST) X-Received: by 10.176.64.234 with SMTP id i97mr5233231uad.7.1480089615471; Fri, 25 Nov 2016 08:00:15 -0800 (PST) MIME-Version: 1.0 Received: by 10.31.202.71 with HTTP; Fri, 25 Nov 2016 07:59:54 -0800 (PST) In-Reply-To: References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From:Yaron Minsky Date: Fri, 25 Nov 2016 10:59:54 -0500 Message-ID: To:Gabriel Scherer Cc:Andreas Rossberg , Julien Blond , David Allsopp , OCaml mailing-list Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-JS-Processed-by: mailcore Subject: Re: [Caml-list] Empty polymorphic variant set 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 wa= y 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 was >>>> 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" r= esult >>>> which could have type something like ('a, []) result. One could encode= 'b as >>>> some error list at type level but it needs some complicated type manag= ement >>>> and i'm targeting OCaml beginners for which i just want them to be car= eful >>>> 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 polymorphic >>>>>> variant >>>>>> set in type expressions or if it's a bug ? >>>>> >>>>> As you've observed, [] is a variant constructor since 4.03.0 - see GP= R#234 >>>>> (https://github.com/ocaml/ocaml/pull/234). The GPR contains reference= s 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 polymor= phic >>>>> 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