GADT pattern matching

I’ve been playing around with GADTs lately and was wondering if anybody could point me in the right direction for learning how to type this so it would compile, if it’s possible, or if I’m overly complicating things.

I have seen a few other answers to GADT pattern matching here but this seems to be a little different.

I’ve seen this type of thing done to represent a type with no possible values:

module Nothing = {
  type t =
    | Nothing(t);
};

So I wanted to use it to lock down this Exit.t type so I could have a type of Exit.t('a, Nothing.t) to represent the Success case, capturing the fact that there is no recoverable Failure value.

module Exit = {
  type t('a, 'e) =
    | Success('a): t('a, Nothing.t)
    | Failure('e): t(Nothing.t, 'e);

This seemed to be okay, until I tried to write a flatMap function for it.

  let flatMap: ('a => t('a1, 'e), t('a, 'e)) => t('a1, 'e) = (f, exit) =>
    switch (exit) {
    | Success(a) => f(a)
    | Failure(_) as e => e
    };
};

As is, it is inferring type Exit.t to always be Exit.t(Nothing.t, Nothing.t) which, I kind of understand since the type in the Failure case would set the first type to Nothing and the Success case would set the second type to Nothing.

I've tried the one thing I know, making some of those types local using type a. I've tried type a a1 e and type a e leaving 'a1 but I just don't seem to be able to capture the idea.

Solution

(I am using the OCaml syntax below, since the question is also tagged "ocaml", but the same should hold for Reason.)

First, your type Nothing.t is not empty. The cyclic value Nothing (Nothing (Nothing (...))) is a valid inhabitant. If you really want the type to be empty, do not put any constructor.

Second, as you guessed, in flat_map, your Failure branch forces 'a1 to be instantiated with Nothing.t. There is no way around that; it is not a deficiency of the compiler, just the only way to interpret this code.

Third, you are making things a bit too complicated, as Exit.t does not have to be a GADT in the first place, to achieve your goals.

Below is a simpler example that shows that, if Nothing.t is actually empty, then the compiler correctly allows irrelevant branches.

type nothing = |
type ('a, 'b) result =
  | Success of 'a
  | Failure of 'b
let only_success (x : ('a, nothing) result) : 'a =
  match x with
  | Success v -> v
  | Failure _ -> . (* this branch can be removed, as it is correctly inferred *)