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 E22307EE9C for ; Fri, 25 Nov 2016 18:12:53 +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-f175.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.175; 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.175 as permitted sender) identity=mailfrom; client-ip=209.85.223.175; 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-f175.google.com) identity=helo; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f175.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ANLkOSRxFDLFmDSXXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0egXIJqq85mqBkHD//Il1AaPBtSArakewLuK++C4ACpbvsbH6ChDOLV3FDY7yu?= =?us-ascii?q?wu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9?= =?us-ascii?q?Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnCRysrhjK/uwRnZdmYvI0wwHKv2AOfu?= =?us-ascii?q?NK2WdAKleanhK67cC1qs1N6SNV7t0o/dRBXKGyRK84QKZVFnxyPGk//szmsV/Y?= =?us-ascii?q?RguC/HYGemoTmxtMRQPC6UepDd/KriLmu78li2GhNsrsQOVxAGz64g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BKAAB5cDhYf6/fVdFEEAocAQEEAQEKA?= =?us-ascii?q?QEXAQEEAQEKAQGCfw4BAQEBAXdyEAeNPpcZgjeSPYIIHQ2FdwKBXQc/FAEBAQE?= =?us-ascii?q?BAQEBAQEBEgEBCQsLCRsygjMEARUBBIIWAQEBAgEBAQIPEQQZARQHEgsBAwELB?= =?us-ascii?q?gULDQICCRoDAgIhAQERAQUBCgERBhMIAQkIAQeIMAEDDwgOLp1NgTI/MotQgWw?= =?us-ascii?q?YBQEfgw0Fg1UKGScDClSDNgEBAQEBAQQBAQEBAQEBARcCBhJ5hTOEW4JIQ4EWK?= =?us-ascii?q?IMEgl0FhjZSDIhZijI1gXaEUoYfSYNWggk4jXGJQIQxgkgTHoETHoEsQBGDFw8?= =?us-ascii?q?cgXsgNAGGZ4FPAQEB?= X-IPAS-Result: =?us-ascii?q?A0BKAAB5cDhYf6/fVdFEEAocAQEEAQEKAQEXAQEEAQEKAQG?= =?us-ascii?q?Cfw4BAQEBAXdyEAeNPpcZgjeSPYIIHQ2FdwKBXQc/FAEBAQEBAQEBAQEBEgEBC?= =?us-ascii?q?QsLCRsygjMEARUBBIIWAQEBAgEBAQIPEQQZARQHEgsBAwELBgULDQICCRoDAgI?= =?us-ascii?q?hAQERAQUBCgERBhMIAQkIAQeIMAEDDwgOLp1NgTI/MotQgWwYBQEfgw0Fg1UKG?= =?us-ascii?q?ScDClSDNgEBAQEBAQQBAQEBAQEBARcCBhJ5hTOEW4JIQ4EWKIMEgl0FhjZSDIh?= =?us-ascii?q?ZijI1gXaEUoYfSYNWggk4jXGJQIQxgkgTHoETHoEsQBGDFw8cgXsgNAGGZ4FPA?= =?us-ascii?q?QEB?= X-IronPort-AV: E=Sophos;i="5.31,547,1473112800"; d="scan'208";a="246751245" Received: from mail-io0-f175.google.com ([209.85.223.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Nov 2016 18:11:58 +0100 Received: by mail-io0-f175.google.com with SMTP id x94so133893001ioi.3 for ; Fri, 25 Nov 2016 09:11:58 -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=QG56ZTqkQunYxOGthFEVeBsNl4yEuEl0vX3mAoLHXpY=; b=x4pezDd5v+V8O7SgsKKPQpsZNftdiq8lJi2SKMS2SG8GRAM9Vr0eGBkRB7e2FJyuN0 n+2sz3Pd96GLFq6zL1k5j/ZqmUHkGLyAFVwkh5Jv2hHLBIyGN5HN40gYlpjwH9vNcLus vXC4GzxyVaZNQpOKhKx0nbNUpiLQvvwjUECCZU3pOp1FPYqNdlG4RUivLq74hTJrYFdN Kt7L4pIcrIil6/5skUsAmaRj8OWLHaNpKX5nR3MbhjnhWi9leTWWJ9a/Vdxkao2nFTZ9 k0ncgQ8FCL4tmOvaciTyKji3GsBjbKiumn0oPS21a746bJ5LbAH7EDdFtDl0ifPCBxtz pTKQ== 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=QG56ZTqkQunYxOGthFEVeBsNl4yEuEl0vX3mAoLHXpY=; b=BPD+eYAZdTNiGtDYjXR+ilCJokWDK0WdaIhFZiZlgBWrXRsBEpZYgvu0Q/KYJGyqqX E802yK6Z3jE5IyQiOf3+KFtU6r0Gti4atNGHloX+H+Apb5IxEb4id563erNOXX8ldzBb YT3VyfFhfwIwOyZUcVe8BP6oqEltV136IP9xvlIiWsVLAnPrNKXzUsYUpPcDR97iQzdZ FSF6Zs5/RjR63Ewkhpy0eoMHFHad9vZstnB98cpSJC4IzIeCeTLaM2q4UFU+2/dWCDW6 0grZy4niWq82PAp0sdQsDWDBZPsdaNxavhuGYXOeKw3xwL7/HOpxVYZslxETaLWgCRQw fm7w== X-Gm-Message-State: AKaTC01aC/2FCxdNvLqPoFnCgPSDoFzG8gZHbmgSRLjAdS1OWDuYo/3NG/I8n3ITt0f8EDr9YUD9fvZxP25ZOg== X-Received: by 10.107.2.210 with SMTP id 201mr7429075ioc.67.1480093917094; Fri, 25 Nov 2016 09:11:57 -0800 (PST) MIME-Version: 1.0 Received: by 10.79.18.131 with HTTP; Fri, 25 Nov 2016 09:11:16 -0800 (PST) In-Reply-To: References: <3AD797C1-47D8-4521-9CEF-03D12CDF6867@mpi-sws.org> From: Gabriel Scherer Date: Fri, 25 Nov 2016 12:11:16 -0500 Message-ID: To: Markus Mottl Cc: Yaron Minsky , 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 On Fri, Nov 25, 2016 at 11:42 AM, Markus Mottl wro= te: > 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. It used to be the case that the only way to get the type-checker to reason on which constructors of a GADT can or cannot happen from type information was to have one of the constructors of this GADT to occur explicitly in the pattern-matching. The code above would thus have beeen warned as non-exhaustive as the type-checker could not "see" that the missing case, namely _, was in fact equivalent to (Error _), and that there was no possible constructor to fill that last wildcard. (Doing a case-analysis on the possible patterns a "_" could be decomposed into is called "exploding" the wildcard.) Jacques Garrigue gave at talk at the 2015 ML workshop on the question of: how much wildcard should we explode when analyzing pattern-matchings? GADTs and exhaustiveness: looking for the impossible Jacques Garrigue and Jacques Le Normand 2015 http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-imposs= ible.pdf https://youtu.be/vyZ4Bvogil4 If we explode wildcards as long as the type says we can, we can non-terminate on recursive types. If we explode wildcard too much, the performance of type-checking can suffer a lot. If we don't explode enough, we are unable to check exhaustiveness effectively. Jacques and Jacques' idea was to let people write pattern to say "this case cannot happen", and that would serve two roles at once: indicate author's intent in tricky case (an aspect of language design whose importance cannot be understated), and also serve as "exploding hints" for the type-checker, who would explode as deeply as those refutation patterns directed it to -- plus one more, if I remember correctly. This is highly similar to Agda's "absurd patterns". The rest of the discussion, including a lengthy but ultimately fairly satisfying syntax bike-shedding session, can be found on Mantis: https://caml.inria.fr/mantis/view.php?id=3D6437 > 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. I think we don't want to be in the business of arbitrary proof search for emptyness or inhabitation. For GADTs there are well-understood notion of equations, (in)compatible types that naturally lead to the type-checker detecting some cases as impossible -- so these "elimination opportunities" are intrisic to GADTs as a feature. Adding heuristics to detect other notions of non-inhabitation sounds risky. Do we have strong use-cases for this? > On Fri, Nov 25, 2016 at 10:59 AM, Yaron Minsky w= rote: >> 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 = 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 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 typ= e? >>>> >>>> /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 varian= t 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 enco= de 'b as >>>>>> some error list at type level but it needs some complicated type man= agement >>>>>> and i'm targeting OCaml beginners for which i just want them to be c= areful >>>>>> 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 polymorp= hic >>>>>>>> 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 referen= ces 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 polym= orphic >>>>>>> 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 > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com