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.