Re: [Caml-list] Empty polymorphic variant set

[Jeremy Yallop <yallop@gmail.com>]

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