[Caml-list] Empty polymorphic variant set

[Caml-list] Empty polymorphic variant set

[Julien Blond]

[-- Attachment #1: Type: text/plain, Size: 389 bytes --]

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 ?

Regards,

-- Julien Blond

[-- Attachment #2: Type: text/html, Size: 619 bytes --]

Re: [Caml-list] Empty polymorphic variant set

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 1107 bytes --]

After playing around with this for a little while, it looks to me like

    type t = []

isn't defining t as a synonym for the empty polyvariant, but rather
defining t to be an ADT with one constructor, []. In particular, note that

    type t = []
    type s = []

    let f (x : s) : t = x (* does not typecheck *)

    type r = t = [] (* parses fine, showing [] is a constructor *)

    let f [] = () (* no exhaustivity warnings, inferred type is f : r ->
unit *)

It's odd that [] is a valid constructor name, but I suppose we want it so
for lists, and might as well let other people reuse it.

On 25 November 2016 at 16:39, Julien Blond <julien.blond@gmail.com> wrote:

> 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 ?
>
> Regards,
>
> -- Julien Blond
>

[-- Attachment #2: Type: text/html, Size: 1792 bytes --]

Re: [Caml-list] Empty polymorphic variant set

[Julien Blond]

[-- Attachment #1: Type: text/plain, Size: 661 bytes --]

Forget my question :) The [] is actually interpreted as a variant
constructor, not a polymorphic variant set that must have an element at
least.

-- Julien Blond

2016-11-25 9:39 GMT+01:00 Julien Blond <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 ?
>
> Regards,
>
> -- Julien Blond
>

[-- Attachment #2: Type: text/html, Size: 1166 bytes --]

RE: [Caml-list] Empty polymorphic variant set

[David Allsopp]

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

Re: [Caml-list] Empty polymorphic variant set

[Julien Blond]

[-- Attachment #1: Type: text/plain, Size: 1740 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 2578 bytes --]

Re: [Caml-list] Empty polymorphic variant set

[Gabriel Scherer]

I would agree that OCaml lacks a convenient way to define the empty
type. (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
>
>

Re: [Caml-list] Empty polymorphic variant set

[Andreas Rossberg]

> 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

Re: [Caml-list] Empty polymorphic variant set

[Markus Mottl]

My preferred way of representing the empty type is as follows:

  type void = { void : 'a. 'a }

This allows you to do:

  type t = A | B of void

  let f = function
    | A -> "A"
    | B { void } -> void

This can come in handy for e.g. partially implementing type
definitions.  Instead of raising exceptions in branches you cannot
implement yet, you just simply return "void", which unifies with
anything.  Since there is provably no way to create a value that would
end up in that branch, this is safe.  Once you complete the argument
definition for tag B, the compiler will detect all code locations that
depend on that branch.

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



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com

Re: [Caml-list] Empty polymorphic variant set

[Gabriel Scherer]

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

Re: [Caml-list] Empty polymorphic variant set

[Yaron Minsky]

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

Re: [Caml-list] Empty polymorphic variant set

[Markus Mottl]

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.

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.

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

Re: [Caml-list] Empty polymorphic variant set

[Gabriel Scherer]

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

Re: [Caml-list] Empty polymorphic variant set

[Stephen Dolan]

[-- Attachment #1: Type: text/plain, Size: 716 bytes --]

On Fri, Nov 25, 2016 at 1:52 PM, 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?
>

I agree that that defines the empty type, but OCaml disagrees. OCaml takes
that as declaring an abstract type, just as if you'd included a module
exposing an opaque type. So, the compiler won't conclude that 'empty' is
actually an empty type (viewing it as an unknown abstract type), nor will
it refute (int, empty) eq.

Stephen

[-- Attachment #2: Type: text/html, Size: 1164 bytes --]

Re: [Caml-list] Empty polymorphic variant set

[Jeremy Yallop]

On 25 November 2016 at 16:50, Stephen Dolan <stephen.dolan@cl.cam.ac.uk> wrote:
> On Fri, Nov 25, 2016 at 1:52 PM, 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?
>
>
> I agree that that defines the empty type, but OCaml disagrees. OCaml takes
> that as declaring an abstract type, just as if you'd included a module
> exposing an opaque type. So, the compiler won't conclude that 'empty' is
> actually an empty type (viewing it as an unknown abstract type), nor will it
> refute (int, empty) eq.

There's a small (and not enormously useful) distinction to be made
here.  If 'empty' is in the current module then OCaml knows that
'empty' and 'int' are incompatible, and so accepts the following
program:

   type empty
   type (_,_) eql = Refl : ('a,'a) eql
   let f : (int, empty) eql -> unit = function _ -> .

However, if 'empty' is defined in a different module ('M', say) then
OCaml treats 'empty' and 'int' as compatible and so rejects the
following (non-)program:

   type (_,_) eql = Refl : ('a,'a) eql
   let f : (int, M.empty) eql -> unit = function _ -> .

Jeremy