Dear all,

Thanks a lot for your help. Things are much clearer now.

Abdallah

2015-10-13 20:45 GMT+11:00 Jeremy Yallop <yallop@gmail.com>:

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