Re: [Caml-list] Empty polymorphic variant set

[Andreas Rossberg <rossberg@mpi-sws.org>]

> 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