Is it possible to ensure a type is empty?

Learning
1

Let’s say I have a trivial GADT t:

type _ t =
| Str : string t
| Int : int t

If I have a function f that’s defined as

let f : bool t -> bool = ...

f can be implemented using

function
| _ -> failwith "unimplemented"

But if I add a new constructor Bool : bool t to t, ideally I should know that now I’m not being exhaustive, which that doesn’t guarantee.

Is it possible for me to ensure that bool t doesn’t have any constructors, similar to how I can know that I’m not exhaustively enumerating all constructors in the non-empty case?

2

You want to use a refutation case:

let f : bool t -> bool = function
| _ -> .
1 Like
3

Awesome, thanks @dbuenzli! That’s exactly what I was looking for – not sure how I missed that in the manual.