On 13 October 2015 at 07:15, Ben Millwood <bmillwood@janestreet.com> wrote:
> I'll advance on others' advice by pointing out that if you say:
>
> type never = private [`never]
>
> then you neither "use up" a constructor name nor is it possible to write an
> expression with type never.
A nit: there are lots of *expressions* of type 'never', such as
'(assert false: never)'. However, there are no (closed) *values* of
type 'never'.
> Unfortunately, the compiler still doesn't realise that, so it
> doesn't help you for pattern-matching.
The gadt-warnings branch, which is described here:
GADTs and exhaustiveness: looking for the impossible
Jacques Garrigue's and Jacques Le Normand
ACM SIGPLAN Workshop on ML, September 2015
http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf
includes better supports for "empty" types. For example, here's a
definition of an empty type 'wrong':
type 'a is_true = T: [`True] is_true
type wrong = [`False] is_true
and here's a function definition which omits a case that you can
deduce is unmatchable when you know that 'wrong' is empty:
let f : wrong option -> unit = fun None -> ()
The current OCaml compiler (4.02.3) issues a warning for 'f':
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Some _
In contrast, the compiler in the gadt-warnings branch compiles 'f'
without complaint (and generates more efficient code, since there's no
need to inspect the argument).
Jeremy.