Empty polymorphic variant type?

Learning
1

Is there an empty polymorphic variant type? Since the syntax [>] means a polymorphic variant that can have any constructors, it would seem natural for [<] to mean a polymorphic variant that can have no constructors (hence is necessarily empty), but it doesn’t seem to be accepted. The syntax [] for an “exact” empty polymorphic variant would conflict with empty lists, but I don’t see a problem with [<].

One reason I think this would be useful is that it would be a subtype of all other polymorphic variant types.

2

https://ocaml.org/manual/emptyvariants.html

3

I know about empty variants. I’m asking about empty polymorphic variants. Despite its name, the other question seems to be only about empty ordinary variants.

4

Empty types would be strictly superior replacement for empty polymorphic types, if empty types were considered as a subtype of any type as suggested in Feature request: Make empty types subtype of any other type · Issue #9459 · ocaml/ocaml · GitHub .

Note also that empty polymorphic variants are supported by the compiler, there is just no syntax for them, partially because they are mostly useless. However, it is perfectly possible to define an empty polymorphic variant ppx. For instance, this test is the compiler testsuite: ocaml/typecore_empty_polyvariant_error.ml at trunk · ocaml/ocaml · GitHub tests an error path that only happens with empty polymorphic variants.

5

Considering ordinary empty types as a subtype of any type is wrong to me; I’m glad that isn’t the case. But since polymorphic variant types already have subtyping relations, I think it would make sense for them to include an empty version.

6

I had the same question and opened a feature wish to support [ | ] as the empty polymorphic variant type. If there is positive feedback I may open a Pull Request.

7

I have just discovered that there do exist polymorphic variant types that are semantically empty even if they are not syntactically empty, such as

type empty = [ `Empty of empty ]

This type has a constructor, but due to the recursion it is not possible to actually construct an element of it, and we can prove that it satisfies the eliminator of the empty type:

let rec abort : type a. empty -> a = function (`Empty e) -> abort e

This doesn’t achieve the general goal of having one polymorphic variant type that is a subtype of every other such. But I think if you have control over the other polymorphic variant types you’re using, you should be able to add the constructor `Empty of empty to all of them, causing them to contain empty as a subtype without adding any actual elements to them. (Although that would require adding an extra `Empty e → abort e clause to any match on them.)

8

It’s actually possible to write:

let rec empty : empty = `Empty empty

which without the annotation gets type [> `Empty of 'a ] as 'a, so it isn’t really an empty type.

9

It’s easy enough to adapt that approach to use actually empty types, though, e.g. with a empty variant

type nothing = |
type empty = [`Empty of nothing ]
let abort : type a. empty -> a = function `Empty _ -> .

or a polymorphic record field:

type nothing = { abort: 'a. 'a }
type empty = [`Empty of nothing ]
let abort : type a. empty -> a = function `Empty { abort } -> abort

or an equality GADT with incompatible types:

type empty = [`Empty of ([`A], [`B]) Type.eq ]
let abort : type a. empty -> a = function `Empty _ -> .
10

Thank you! You’re right, those modifications work. And for completeness, here is a definition, using that approach, of a family of finite types of all cardinalities that are related by subtyping:

type empty = |
type zero = [ `Empty of empty ]
type 'a suc = [ `Zero | `Suc of 'a | `Empty of empty ]

Then zero < zero suc < zero suc suc < …

11

That’s because in a turing complete language (with full recursion) any type is inhabited, see for instance How many values does a boolean have?, especially the paragraph about Haskell and bottom which is similar to the solution of @viritrilbia. Bottom is the denotation of non terminating computation.

In OCaml, you can inhabit the type empty like this:

type empty = |
let rec make_empty () = (make_empty () : empty)

In other words, in @yallop solution the production-introduction of a bottom value leads to non termination (make_empty ()), whereas in @viritrilbia that’s the use-elimination of such a value that lead to non termination (abort empty) : they are dual point of view.

12

That was my first reaction too, but I think there’s a difference: your make_empty is a function whose return type is empty, but if you actually call it, it never returns. If you try to define let x = make_empty () then it will compile, but if it will blow up if you run it. Whereas @amongonz 's empty will actually return: it’s a cyclic data structure, not a divergent computation.

13

For sure, because OCaml is a call-by-value language. If you look at the blog article I linked, in Haskell, which is a call-by-name language, you could write this equivalent OCaml code:

let rec empty : 'a. a = empty

and that’s the use-elimination of empty that leads to a divergent computation, as in your code example: try abort empty with your implementation and you will have a divergent computation. @yallop and your Haskellish solution are dual : in one case the divergence is in the introduction principle, in the other it’s in the elimination one.

14

I think this one works, too:

module rec Empty :
sig
  type t
  val abort : t -> 'a
end = Empty
15

Apparently the following also works:

  module Empty : sig
    type t = private [ `B of t ]
  end = struct
    type t = [ `B of t ]
  end

Who knew there were so many ways to define an empty type!

16

This is not a empty type, since the module could construct

let rec x = `B x

If you want to test that you are defining a provably empty type, you can ask the typechecker directly with an unreachable clause. For instance, this compiles fine:

type empty = |
type t = [ `E of empty ]
let really_empty (x:t) = match x with `E _ -> .

Contrarily, this code

module Empty : sig
  type t = private [ `B of t ]
end = struct
  type t = [ `B of t ]
  let rec x = `B x
end
let not_empty (x:Empty.t) = match (x:> [`B of Empty.t]) with `B _ -> .

fails with

Error: This match case could not be refuted.
Here is an example of a value that would reach it: `B _

17

But outside the module it behaves like an empty type, because the module as defined doesn’t export such a thing.