From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 2145E7EE9C for ; Fri, 25 Nov 2016 16:47:22 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f196.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.196 as permitted sender) identity=mailfrom; client-ip=209.85.223.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-io0-f196.google.com) identity=helo; client-ip=209.85.223.196; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f196.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AFTf50hwvlb6l71DXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0e4UIJqq85mqBkHD//Il1AaPBtSArakewLWK++C4ACpbvsbH6ChDOLV3FDY7yu?= =?us-ascii?q?wu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9?= =?us-ascii?q?Dq3PF4XTl8W60fyps92WOl0QxWmLWq5pNBi9sSnWs8AXh8MidvdwmVP1pS5hfe?= =?us-ascii?q?hMyGpzbWiUhA32692/tMp59D9Lsf87+OZFSaS/ZLsjC7tCA2J1HXoy4ZjEvBPZ?= =?us-ascii?q?TAaLrkAXUmgMnwAAVwfM5gv7U5O3qSD6u/BwwgGVOMT3SfY/XjH0vPQjcwPhlC?= =?us-ascii?q?pSb21xy2rQkMElyf8CrQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ATAQBuXDhYYsTfVdFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAR9YgQIHjT6XGYI3kj2CCCiFeQKBWgc/FAEBAQEBAQE?= =?us-ascii?q?BAQEBBRgLDAYdMoIzBAEVBYIWAQEBAwESEQQZARsSCwEDAQsGBQsNAgIJGgMCA?= =?us-ascii?q?iEBAREBBQEKAREGExIICIgwAQMPCA6dUYEyPzKLUIFsGAUBH4MNBYNXChknAwp?= =?us-ascii?q?UgzYBAQEBAQEEAQEBAQEBARgCBhJ5hTOEW4JIggGDBIJdBYcIDIhZijI1gXaEU?= =?us-ascii?q?oYfSYNWggk4jXGJQIQxgkgTHoETHoEsQBGDF4ImIDQBhmeBTwEBAQ?= X-IPAS-Result: =?us-ascii?q?A0ATAQBuXDhYYsTfVdFeHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAR9YgQIHjT6XGYI3kj2CCCiFeQKBWgc/FAEBAQEBAQEBAQEBBRgLDAYdM?= =?us-ascii?q?oIzBAEVBYIWAQEBAwESEQQZARsSCwEDAQsGBQsNAgIJGgMCAiEBAREBBQEKARE?= =?us-ascii?q?GExIICIgwAQMPCA6dUYEyPzKLUIFsGAUBH4MNBYNXChknAwpUgzYBAQEBAQEEA?= =?us-ascii?q?QEBAQEBARgCBhJ5hTOEW4JIggGDBIJdBYcIDIhZijI1gXaEUoYfSYNWggk4jXG?= =?us-ascii?q?JQIQxgkgTHoETHoEsQBGDF4ImIDQBhmeBTwEBAQ?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246738104" Received: from mail-io0-f196.google.com ([209.85.223.196]) by mail2-smtp-roc.national.inria.fr with ESMTP; 25 Nov 2016 16:47:21 +0100 Received: by mail-io0-f196.google.com with SMTP id r94so10134787ioe.1 for ; Fri, 25 Nov 2016 07:47:21 -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=wSTegEeh/QchfME3wpU4bou0z/Yaar801NC6JNkFQg0=; b=kg2uynV6qqAX4bQKi52NZdA2L2Dspt3bpGkfi/Nhy4BC2kdphUZ/xVFwhY2Qrx8e6j t+1JgLiI5FcFTLY7DLIPV1ceITb7pJvAadrveuGoQswtaJPrRyTP5AndU6pRnetLp9MT J5+EI0/6Jnr/Zf7OF4Pvb6ErBnOOHUqyr0uFuXWa7rjHHR7zspPZc8ZAMztP06WRHC7F JlLZx0rarauocWGyizGCevFokozYFmDUgu0mSk1gBwIEFz1zKJ6GCd79PTz9FvkcBKmW eA0XgX5bpevORLpXswIpqhL9KFRADxcem/q+Uzh7F2xIHvxCVhOVRbh7sPdGZ1nMS/qV t2Bw== 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=wSTegEeh/QchfME3wpU4bou0z/Yaar801NC6JNkFQg0=; b=NcYCtERuRrw7dkH+HFsnmSG4hR/HxypQNgbOxjyTN3BDF3PFcnICyrkhXj0Q04pQmQ C7qLjrIoX3UJUiEYklBhM5d+XSPU/fK6VinVL0KcTsXEytQ6cq3eCkkxpyZwgWlfa/c6 Ecar+CixvgAoIqbY7ReRNxneH0NYI8UxaRcz2bCoQnkZ4AgxQSZYJD8lHm+ysSOy5dNW 84j/5G7SjPtLOAIml8848u1PP4wyIa+m2w/B07YJGUiAQilwbnOclb+ob0hZHYM8n4WM qOJvtuWify8yQgsyqRcyfXJZotFiIDbhNbwBNTTzkeoEzPd8qTLrKY482mO0jI3SLXGB 4qgw== X-Gm-Message-State: AKaTC02LfeIQZzKy4B86S09pDnD2P9j5RsP0t7EiYoU4nIcaF1vxNqjR40coT/QMf5t5Fmu8xSGkXgLOh6AoKg== X-Received: by 10.36.22.212 with SMTP id a203mr7592731ita.3.1480088840358; Fri, 25 Nov 2016 07:47:20 -0800 (PST) MIME-Version: 1.0 Received: by 10.79.18.131 with HTTP; Fri, 25 Nov 2016 07:46:39 -0800 (PST) In-Reply-To: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Gabriel Scherer Date: Fri, 25 Nov 2016 10:46:39 -0500 Message-ID: To: Andreas Rossberg Cc: 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 > Isn=E2=80=99t [an abstract type definition] a sufficiently convenient way= 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 wr= ote: > >> 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 w= rote: >>> 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 l= ist >>> :) >>> >>> 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" re= sult >>> 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 manage= ment >>> and i'm targeting OCaml beginners for which i just want them to be care= ful >>> 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 GPR= #234 >>>> (https://github.com/ocaml/ocaml/pull/234). The GPR contains references= 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 polymorp= hic >>>> 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 >