Empty polymorphic variant type use case

Learning
1

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 mainly asking the question because I know there is an interesting use case in Coq for example, where propositional falseness is represented as an empty type, and a match clause on such a value does not typecheck. However, I have no clue if such interesting cases can occur in OCaml.

Do you have any ideas or pointers to interesting documents on the topic?
Thanks in advance.

2 Likes
2

It’s sometimes useful if you’re implementing a generic interface and you don’t need something in your implementation. e.g.

module Disk_db : DB with type error = io_error
module Memory_db : DB with type error = empty

Then anyone using Memory_db specifically knows they don’t have to worry about handling errors.

3 Likes
3

To add to @talex5’s example, the exhaustiveness checker understands empty types. For instance, the following function is total, and emits no exhaustivity warning when compiled:

let handle_error : (string, empty) result -> string =
  fun (Ok x) -> x

Again, useful for satisfying a generic interface that permits some inhabited error but doesn’t require it. It’s also possible to assert that a pattern is unreachable using refutation cases. For your own example of a function that cannot be applied:

let f : empty -> bool = function _ -> .
4 Likes