# Empty polymorphic variant type?

**URL:** <https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467>\
**Category:** Learning\
**Created:** [September 10, 2021, 5:21pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467 "2021-09-10T17:21:12Z")\
**Posts on this page:** 17\
**Page:** 1

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [September 10, 2021, 5:21pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/1 "2021-09-10T17:21:12Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![orbitz](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/orbitz/32/110_2.png) [@orbitz](https://discuss.ocaml.org/u/orbitz)\
**Post date:** [September 10, 2021, 8:43pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/2 "2021-09-10T20:43:53Z")

</div>

[https://ocaml.org/manual/emptyvariants.html](https://ocaml.org/manual/emptyvariants.html)

> [@Empty polymorphic variant type use case](https://discuss.ocaml.org/t/empty-polymorphic-variant-type-use-case/8371):
>
> Hello. I was wondering with some of my colleagues what the use case could be for an empty polymorphic variant type, apart from making some type that is empty at first but meant to be extended afterwards in other modules. type empty = | Second question: the previous declaration typechecks, but why can one match on a value in this empty type, if the compiler knows there are no constructors available? let f : empty -\> bool = fun x -\> match x with \_ -\> true (\* should not typecheck? \*) I am mai…

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [September 10, 2021, 8:58pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/3 "2021-09-10T20:58:26Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [September 10, 2021, 10:04pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/4 "2021-09-10T22:04:08Z")

</div>

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](https://github.com/ocaml/ocaml/issues/9459) .

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](https://github.com/ocaml/ocaml/blob/trunk/testsuite/tests/typing-misc/typecore_empty_polyvariant_error.ml#L12) tests an error path that only happens with empty polymorphic variants.

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [September 11, 2021, 4:35pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/5 "2021-09-11T16:35:30Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\
**Post date:** [October 10, 2021, 1:15pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/6 "2021-10-10T13:15:20Z")

</div>

I had the same question and opened [a feature wish](https://github.com/ocaml/ocaml/issues/10687) to support `[|]` as the empty polymorphic variant type. If there is positive feedback I may open a Pull Request.

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [April 20, 2026, 6:57am UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/7 "2026-04-20T06:57:59Z")

</div>

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

```ocaml
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:

```ocaml
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.)

---

<div class="post-metadata">

**Author:** ![amongonz](https://avatars.discourse-cdn.com/v4/letter/a/a88e4f/32.png) [@amongonz](https://discuss.ocaml.org/u/amongonz)\
**Post date:** [April 20, 2026, 7:39am UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/8 "2026-04-20T07:39:21Z")

</div>

It’s actually possible to write:

```ocaml
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.

---

<div class="post-metadata">

**Author:** ![yallop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yallop/32/517_2.png) [@yallop](https://discuss.ocaml.org/u/yallop)\
**Post date:** [April 20, 2026, 8:25am UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/9 "2026-04-20T08:25:38Z")

</div>

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

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

```

or a polymorphic record field:

```auto
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:

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

```

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [April 20, 2026, 4:58pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/10 "2026-04-20T16:58:45Z")

</div>

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:

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

```

Then `zero` \< `zero suc` \< `zero suc suc` \< …

---

<div class="post-metadata">

**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\
**Post date:** [April 20, 2026, 8:30pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/11 "2026-04-20T20:30:09Z")

</div>

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?](https://danilafe.com/blog/boolean_values/), 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:

```ocaml
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.

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [April 20, 2026, 8:54pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/12 "2026-04-20T20:54:40Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![kantian](https://avatars.discourse-cdn.com/v4/letter/k/4bbf92/32.png) [@kantian](https://discuss.ocaml.org/u/kantian)\
**Post date:** [April 20, 2026, 10:20pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/13 "2026-04-20T22:20:28Z")

</div>

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:

```ocaml
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.

---

<div class="post-metadata">

**Author:** ![yallop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yallop/32/517_2.png) [@yallop](https://discuss.ocaml.org/u/yallop)\
**Post date:** [April 20, 2026, 10:46pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/14 "2026-04-20T22:46:14Z")

</div>

I think this one works, too:

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

```

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [April 21, 2026, 1:12am UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/15 "2026-04-21T01:12:56Z")

</div>

Apparently the following also works:

```ocaml
  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!

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [April 21, 2026, 8:10am UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/16 "2026-04-21T08:10:51Z")

</div>

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

```ocaml
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:

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

```

Contrarily, this code

```ocaml
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 \_

---

<div class="post-metadata">

**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\
**Post date:** [April 21, 2026, 4:02pm UTC](https://discuss.ocaml.org/t/empty-polymorphic-variant-type/8467/17 "2026-04-21T16:02:14Z")

</div>

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