Re: [Caml-list] Empty polymorphic variant set

[Gabriel Scherer <gabriel.scherer@gmail.com>]

On Fri, Nov 25, 2016 at 11:42 AM, Markus Mottl <markus.mottl@gmail.com> wrote:
> 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-impossible.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=6437

> 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 <yminsky@janestreet.com> wrote:
>> 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 = struct
>>   type (_,_) t = Equal : ('a,'a) t
>> end
>>
>> type nothing = (unit,int) Equal.t
>>
>> let f (x:(unit,nothing) result) =
>>   match x with
>>   | Ok () -> ()
>>
>> On Fri, Nov 25, 2016 at 10:46 AM, Gabriel Scherer
>> <gabriel.scherer@gmail.com> wrote:
>>>> Isn’t [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 = 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 = <fun>
>>>
>>> On Fri, Nov 25, 2016 at 8:52 AM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
>>>>
>>>>> On Nov 25, 2016, at 14:46 , Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
>>>>>
>>>>> I would agree that OCaml lacks a convenient way to define the empty
>>>>> type.
>>>>
>>>> Isn’t
>>>>
>>>>   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 = Bool : bool onlybool
>>>>>  type empty = int onlybool
>>>>>
>>>>>  let extract : ('a, empty) result -> 'a = function Ok x -> x
>>>>>
>>>>> Since 4.03 (April 2016), it is possible to explicitly write a
>>>>> so-called "refutation case", of the form "<pattern> -> .", 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 = 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 <julien.blond@gmail.com> 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 = 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 encode 'b as
>>>>>> some error list at type level but it needs some complicated type management
>>>>>> and i'm targeting OCaml beginners for which i just want them to be careful
>>>>>> about non nominal results.
>>>>>>
>>>>>>
>>>>>> 2016-11-25 12:22 GMT+01:00 David Allsopp <dra-news@metastack.com>:
>>>>>>>
>>>>>>> Julien Blond wrote:
>>>>>>>> 2016-11-25 9:39 GMT+01:00 Julien Blond <mailto:julien.blond@gmail.com>:
>>>>>>>> Hi,
>>>>>>>> Let's try something :
>>>>>>>> $ ocaml
>>>>>>>>        OCaml version 4.03.0
>>>>>>>>
>>>>>>>> # let _ : [] list = [];;
>>>>>>>> Characters 9-10:
>>>>>>>> let _ : [] list = [];;
>>>>>>>> Error: Syntax error
>>>>>>>> # type empty = [];;
>>>>>>>> type empty = []
>>>>>>>> # let _ : empty list = [];;
>>>>>>>> - : empty list = []
>>>>>>>> #
>>>>>>>>
>>>>>>>> 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 polymorphic
>>>>>>> variants:
>>>>>>>
>>>>>>> let (empty : [> ] list) = []
>>>>>>>
>>>>>>> or
>>>>>>>
>>>>>>> let (length : [> ] list -> int) = 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