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 5A1C47EE9C for ; Fri, 25 Nov 2016 14:53:04 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rossberg@mpi-sws.org; spf=Pass smtp.mailfrom=rossberg@mpi-sws.org; spf=None smtp.helo=postmaster@hera.mpi-klsb.mpg.de Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rossberg@mpi-sws.org designates 139.19.1.49 as permitted sender) identity=mailfrom; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; 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@hera.mpi-klsb.mpg.de) identity=helo; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@hera.mpi-klsb.mpg.de"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AeV6sxxOpJicwxi4edhsl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0IvTzrarrMEGX3/hxlliBBdydsKMfzbGM+P26EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT6zbL9oIhi6swrdu8kIjYB/Nqs/1xzFr2dSde?= =?us-ascii?q?9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLY?= =?us-ascii?q?TQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVQTlgz?= =?us-ascii?q?kbOTEn7G7Xi9RwjKNFrxKnuxx/2JPfbIWMOPZjYq/RYdYWSGxGUchMSixBGZu8?= =?us-ascii?q?YJUTAOodM+hYqIz9qEEPrRu4GAKgAOzixztNinLwwKY00fkuERve0QI9EN0BrH?= =?us-ascii?q?Tao9f7OqkdUu61wrfGwzLYYvNKwDf97ZTEchA9rfyOW797bMrfyVMoFwPAllid?= =?us-ascii?q?tYrlMC6P1usTqWeb9PdrW/6oi248sAF+uSagxt0jioLUgY8V0FfE9T5iwIkuO9?= =?us-ascii?q?K4UkF7bMWhEJtItiGWLpB2Q805Q21yvyY60LIGtIe9cSMXxponwBvfZOaGc4iO?= =?us-ascii?q?+h/jVeCRIS15hH1/Yr6/iQyy/VCvyu39Ssm00EtKoTFfntbQsXAN0gTf68idRf?= =?us-ascii?q?t9+Ueh3iyD2BzU6uFBJ00/iKnVK4Y5z7ItmJcetV7PEjLylUnskaOabEop9+yu?= =?us-ascii?q?5u/6eLvpvIWcOJVxigzmMqQhhMi/AeMgPwgOQWeb4/6z2Kfm/U3hQbVGl/42kq?= =?us-ascii?q?3CsJ/BP8gbo7a5AwBP3ok+9RmzFzam0NIGknkbNF9JZRyKgozzN13TJP30F+qz?= =?us-ascii?q?j06jnTpv3/zGO6fuApTJLnjNirfherN95lZGyAo01tBf/IlbBa8bIPL8QULxsc?= =?us-ascii?q?TYDh4gPwyvzefnE89x1oQEWWKAGqOZKr/dsUeU5uIzJOmBfJMatyz4K/gh/vLu?= =?us-ascii?q?iX45mUQBfaSyxpsWaHW4Hux8LEmDYHrshM0BEWYQsQYkQuzqkg7KbTkGSH+4Ra?= =?us-ascii?q?Mx4nkAA4KrF4rZDtSiibab3Sq/WIZdZm1cB0qkHnLhdoHCUPAJPnG8OMhkxxUC?= =?us-ascii?q?WaKsQpRp7xa1rwX30bUvevDT4TYSuIjs/N1t5qjIigp08iZ7WZfOm1qRRn15yz?= =?us-ascii?q?tbDwQ927py9Akgk1o=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AuAABaQThYmDEBE4teRwEBBAEBCgEBg?= =?us-ascii?q?w0BAQEBAXeBAqRdgjeFO40CgggdC4V5AoF1QBMBAQEBAQEBAQEBARIBAQEBAQg?= =?us-ascii?q?LCwcdMIIzGoIbAQEBAwEBAiAEGQEBLAsBBAsLGAICCRoDAgIhJAERBhMSCIg5A?= =?us-ascii?q?w8IBAqqVWeBbD2DDAEBBYQfAwqECgEBAQEBAQEDAQEBAQEBARgIgQuHMAiCVoJ?= =?us-ascii?q?IggGCTDgtgjCHDQyTCzWGSIZohheHQoYviUCEHhOEDB8BgUkhDgEBgRgBgh+Ba?= =?us-ascii?q?XEBiDYBAQE?= X-IPAS-Result: =?us-ascii?q?A0AuAABaQThYmDEBE4teRwEBBAEBCgEBgw0BAQEBAXeBAqR?= =?us-ascii?q?dgjeFO40CgggdC4V5AoF1QBMBAQEBAQEBAQEBARIBAQEBAQgLCwcdMIIzGoIbA?= =?us-ascii?q?QEBAwEBAiAEGQEBLAsBBAsLGAICCRoDAgIhJAERBhMSCIg5Aw8IBAqqVWeBbD2?= =?us-ascii?q?DDAEBBYQfAwqECgEBAQEBAQEDAQEBAQEBARgIgQuHMAiCVoJIggGCTDgtgjCHD?= =?us-ascii?q?QyTCzWGSIZohheHQoYviUCEHhOEDB8BgUkhDgEBgRgBgh+BaXEBiDYBAQE?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="201713233" Received: from hera.mpi-klsb.mpg.de ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 25 Nov 2016 14:53:03 +0100 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sws.org; s=mail200803; h=To:References:Message-Id:Content-Transfer-Encoding:Cc:Date:In-Reply-To:From:Content-Type:Mime-Version:Subject; bh=WeRQ6Ih35YPXS1lYicJammMOtLHhwhzEBjLZI0b8Y8w=; b=LQI8cevv+xyItiW0w4K56K+JDjihe7PHf4ECdPi34RHgpmleHwxpyObB46dQ1VWdM0VpHm2oRiVZuXhroPC5qB+OhSlLMAnL10mTqulm6CrKrDUDJt5mt0iWjypz42m+Y5gMkg1DC844Xop95HbsDh+l3nn4R5OaJCMqAX/dITQ=; Received: from srv-00-125.mpi-klsb.mpg.de ([139.19.1.28]:36240 helo=maniac.mpi-klsb.mpg.de) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtps (TLS1.2:DHE_RSA_AES_128_CBC_SHA1:128) (Exim 4.80) id 1cAGvv-0006tT-Hn; Fri, 25 Nov 2016 14:53:00 +0100 Received: from 109.125.107.239.dynamic.cablesurf.de ([109.125.107.239]:50699 helo=macbook-air-3.fritz.box) by maniac.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:256) (Exim 4.80) id 1cAGvu-00005o-PK; Fri, 25 Nov 2016 14:52:54 +0100 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: text/plain; charset=utf-8 From: Andreas Rossberg In-Reply-To: Date: Fri, 25 Nov 2016 14:52:52 +0100 Cc: Julien Blond , David Allsopp , OCaml mailing-list Content-Transfer-Encoding: quoted-printable Message-Id: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> References: To: Gabriel Scherer X-Mailer: Apple Mail (2.3124) X-MPI-Local-Sender: true Subject: Re: [Caml-list] Empty polymorphic variant set > On Nov 25, 2016, at 14:46 , Gabriel Scherer w= rote: >=20 > 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). >=20 > One way is to use GADTs to create an impossible type: >=20 > type 'a onlybool =3D Bool : bool onlybool > type empty =3D int onlybool >=20 > let extract : ('a, empty) result -> 'a =3D function Ok x -> x >=20 > 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: >=20 > https://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec241 >=20 > let extract : ('a, empty) result -> 'a =3D function > | Ok x -> x > | Error _ -> . >=20 > 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. >=20 >=20 > On Fri, Nov 25, 2016 at 8:01 AM, Julien Blond wr= ote: >> 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 li= st >> :) >>=20 >> In fact, i wondered if a generic result type like this >>=20 >> type ('a, 'b) result =3D Ok of 'a | Error of 'b >>=20 >> that we can see in several library could be used to specify a "safe" res= ult >> 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 managem= ent >> and i'm targeting OCaml beginners for which i just want them to be caref= ul >> about non nominal results. >>=20 >>=20 >> 2016-11-25 12:22 GMT+01:00 David Allsopp : >>>=20 >>> Julien Blond wrote: >>>> 2016-11-25 9:39 GMT+01:00 Julien Blond : >>>> Hi, >>>> Let's try something : >>>> $ ocaml >>>> OCaml version 4.03.0 >>>>=20 >>>> # 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 [] >>>> # >>>>=20 >>>> Does anyone know if there is a reason to forbid the empty polymorphic >>>> variant >>>> set in type expressions or if it's a bug ? >>>=20 >>> 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. >>>=20 >>> What's your desired use for the type of the non-extensible empty >>> polymorphic variant? >>>=20 >>> Possibly related, you can define a general type for a list of polymorph= ic >>> variants: >>>=20 >>> let (empty : [> ] list) =3D [] >>>=20 >>> or >>>=20 >>> let (length : [> ] list -> int) =3D List.length;; >>> length [`Foo; `Bar];; >>> length [42];; >>>=20 >>> if that's what you were after? >>>=20 >>>=20 >>> David >>=20 >>=20 >=20 > --=20 > 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