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 EDCAE7EE9C for ; Fri, 25 Nov 2016 16:42:29 +0100 (CET) Authentication-Results: mail2-smtp-roc.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-qk0-f170.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.220.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.220.170 as permitted sender) identity=mailfrom; client-ip=209.85.220.170; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qk0-f170.google.com) identity=helo; client-ip=209.85.220.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-qk0-f170.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A8XVTExVxp/1CdllhqUxvfhxrUOHV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZheBt8tkgFKBZ4jH8fUM07OQ6PG7Hzdaqsnd+DBaKdoXCE9D0Z?= =?us-ascii?q?1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f//6mI9pbSewRFgiamKfM3dU3u7FbnjdQNmYZpNoo2zxLIpDMIJ7?= =?us-ascii?q?UXlitUIge6mRrm686rtKRk6D9atuguv5paVr7hdakiQpRdFDVjKH8uosrxuk+Q?= =?us-ascii?q?YxGI4y45W38VjwEAJg/Z8BWyCpL4qCjnrax43zWGOeX5SLk1XXKp6KI9G0ygsz?= =?us-ascii?q?sOKzNsqDKfscd3lq8O5U/4qg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CHAAAoWzhYhqrcVdFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAT06gQIHjT6XGYI3kj2CCB0LhXkCgVoHPxQBAQEBAQE?= =?us-ascii?q?BAQEBARIBAQEICwsJHTCCMwQBFQWCFwEBBAECDxEEGQEUBxILAQMMBgULDQICC?= =?us-ascii?q?RoDAgIhAQERAQUBCgERBhMSCAiIMAEDFw6dT4EyPzKLUIFsGAUBH4MNBYNWChk?= =?us-ascii?q?nAwpUgzYBAQEBAQEEAQEBAQEBARgCBhJ5hTOEW4JIggGDBIJdBYcIDIhZijI1g?= =?us-ascii?q?XaEUoZog1aCQY1xiUCEMYJIEx6BEx6BLEARgxcPEQuBeyA0AYZngU8BAQE?= X-IPAS-Result: =?us-ascii?q?A0CHAAAoWzhYhqrcVdFeHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAT06gQIHjT6XGYI3kj2CCB0LhXkCgVoHPxQBAQEBAQEBAQEBARIBAQEIC?= =?us-ascii?q?wsJHTCCMwQBFQWCFwEBBAECDxEEGQEUBxILAQMMBgULDQICCRoDAgIhAQERAQU?= =?us-ascii?q?BCgERBhMSCAiIMAEDFw6dT4EyPzKLUIFsGAUBH4MNBYNWChknAwpUgzYBAQEBA?= =?us-ascii?q?QEEAQEBAQEBARgCBhJ5hTOEW4JIggGDBIJdBYcIDIhZijI1gXaEUoZog1aCQY1?= =?us-ascii?q?xiUCEMYJIEx6BEx6BLEARgxcPEQuBeyA0AYZngU8BAQE?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246736992" Received: from mail-qk0-f170.google.com ([209.85.220.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 16:42:28 +0100 Received: by mail-qk0-f170.google.com with SMTP id n21so81536055qka.3 for ; Fri, 25 Nov 2016 07:42:28 -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=1EMJcaOfPDehZsjeQxTvMNYrAbpnjAZ4sfRJV3/2FLY=; b=EMMf2ocItE26O25lZJBCfobXaFnU7FtG9NZZjdpxu6Mv4E8SJXt/miSZrbY45Q+bBX NMvITPQTIPYP8z9Zi8FP8htaOeK+lU79pKSvvfdQEyLN64zRAHgwt/D4hZXEm8B9mIhx LwC3SRk+zwqQ/b3R3Th7kt01AFCt9Z9DVhPn80rM5rio6cAT3m9rbIssfLoJbYDmVq6o xo0M62rIVAiOo6MmJFsvY/Lc2+v1LAgDH+biAmp1nmLzd+Ci/E8Kwjq8du4+VSWb/R0h vp2il7yga3B53znmZMMiKsvCxhVfyypOYERK8NBGvHD4DqacsLnuxLbIGz4mlILA4xOn g57w== 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=1EMJcaOfPDehZsjeQxTvMNYrAbpnjAZ4sfRJV3/2FLY=; b=iiB/+dyc2CU++k7U9eIT7eZZYqG/flqt0YCA/60GWwMYPwYBThB+WlJQcozdP6N64d AavWvAEGGJ3hd2gMHph6+7kwiElfukDmCf/eGH4cMBuyi+mlkFgM30oHDvwHSkDFdU0b nQYa59o6pZE4iQRKKoS/Ey47zh9My8nUdp2L0KRerPXTjsV4qXYku5Cy2ecIfOjVBnfb M48C2aAk08QSA9E8j3gtwvl0ecAZq0K3kGKSN4xJhWNYPNi9l+PwqEGugaRuxkYpRFdm +u0DMFvDhnsQER/JuBpTw8Gsf4hy9Zd6khV3jHYlXM4IBlXPZderGSIkC3hciVbhP3op My9g== X-Gm-Message-State: AKaTC03tXdHh4mpIHZH9DQUKQCGm0EvN+ARSDRhStTcQs32NPoK5qnlO3zL2lq278POk1FFX2rrUv61Jro+h0A== X-Received: by 10.55.3.2 with SMTP id 2mr8362250qkd.65.1480088547931; Fri, 25 Nov 2016 07:42:27 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.129.98 with HTTP; Fri, 25 Nov 2016 07:42:27 -0800 (PST) In-Reply-To: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Markus Mottl Date: Fri, 25 Nov 2016 10:42:27 -0500 Message-ID: To: Andreas Rossberg Cc: 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 My preferred way of representing the empty type is as follows: type void =3D { void : 'a. 'a } This allows you to do: type t =3D A | B of void let f =3D function | A -> "A" | B { void } -> void This can come in handy for e.g. partially implementing type definitions. Instead of raising exceptions in branches you cannot implement yet, you just simply return "void", which unifies with anything. Since there is provably no way to create a value that would end up in that branch, this is safe. Once you complete the argument definition for tag B, the compiler will detect all code locations that depend on that branch. 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 > > > -- > 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