Re: [Caml-list] Empty polymorphic variant set

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

> 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
>