Matching incompatible GADT constructors

Learning
1

Is it possible for this match to typecheck when constructors seem to be incompatible?

type 'a t =
  | I: int -> int t
  | S: string -> string t

let () =
  let i = I 42 in
  match i with
  | I n -> Printf.printf "int: %d\n" n
  | S t -> Printf.printf "string: %s\n" t (* error *)

The typechecker tries (and fails) to unify type parameters:

Error: This pattern matches values of type string t
but a pattern was expected which matches values of type int t
Type string is not compatible with type int

I’d like to do this, too, but I guess it’s related:

let get = function
  | I n -> n
  | S t -> t

Thanks!

2

As a general rule, only abstract types can be refined by matching on GADT-constructors. When defining function operating on GADTs, it is therefore often necessary to use locally abstract types:

let get (type a): a t -> a = function
  | I n -> n
  | S s -> s

( If the function is recursive and , the locally abstract notation may need to be combined with the explicit polymorphic notation yielding let get: type a. a t -> a=… .)

However, on your first example, the problem is that your second case is simply impossible: since i has for type int t, the only possible case when matching on i is Int _. Consequently, your example can be rewritten as

let () =
  let i = I 42 in
  match i with
  | I n -> Printf.printf "int: %d\n" n

And this pattern matching is exhaustive. If you don’t feel reassured or if for some extremely imperious reasons you are not using the exhaustiveness check for pattern matching, it is possible to complete the pattern with a refutation case:

let () =
  let i = I 42 in
  match i with
  | I n -> Printf.printf "int: %d\n" n
  | _ -> .

Here the dot . on the right hand side of the case indicates that the pattern on the left hand side should not be reachable and the type-checker will check that it is impossible to produce a value that matches this pattern.

4 Likes
3

Thank you! I’d only heard about forall but it still looks like magic to me, I’m used to think the compiler always gets the most general type for an expression…

My first example didn’t make a lot of sense since it was monomorphic. Of course, if true then I 42 else S "fourty-two" won’t typecheck (int ≠ string), but is it possible to ever get an 'a t from it (I’m just curious)?

4

It’s indirectly possible by using what is usually called an existential wrapper, where the type variable is hidden inside a GADT (here, any):

type _ t =
  | B : bool -> bool t
  | S : string -> string t

type any = Any : 'a t -> any

With that you can express something which is close to your if example:

if true then Any (I 3) else Any (S "foo")

Note that when you pattern match on an any you get an 'a t where the type 'a is unknown and must not escape. The type checker will reject programs that don’t meet the non-escape condition with an error message (that is frequently not as helpful as you would like). Sometimes it isn’t obvious how to fix the problem, which is part of why programming with GADTs can get ‘interesting’.

5

Thanks! I guess 'a can’t escape since it isn’t available at runtime…

As octachron said (I would’ve asked, otherwise), it works with a recursive function, too, so I guess my issue is completey solved!

type 'a t =
  | I: int -> int t
  | S: string -> string t
  | O: 'a t option -> 'a option t

let rec get: type a. a t -> a = function
  | I n -> n
  | S t -> t
  | O None -> None
  | O (Some x) -> Some (get x)

… but I thought forall and type did the same thing. And the former doesn’t work. Why?

6

forall and type are indeed different. type binds a locally abstract type variable (the kind that can have a different type for each GADT constructor that you match against), and forall requires a type variable to be polymorphic.

For this definition of get, you need both (which is what the type a. ... syntax gives you). The reason you need forall is because this function exhibits polymorphic recursion, where a recursive function is used at a different type within its definition. Because of limitations of type inference, annotations are required for this to type check.

An existential variable can escape quite easily: an simple example of a program which is rejected for this reason is let test eq (Any x) (Any y) = eq x y.

7

This property “usually holds” in OCaml. Formally we say that the language has “principal types”, there exists most general types that the inference engine can look for. This works well for the core fragments of OCaml (or other ML languages), but this property crumbles in presence of more advanced type-system features (GADTs, or polymorphic record fields for example); typically we still have principal types but only with respect to a specification¹ that requires extra annotations in some places.

¹: scientific aside: “having principal types” is a property of a type system; you can make it very strong by making this type system very implicit, or fairly weak by forcing programs using this type system to have explicit and ad-hoc/arbitrary specifications. This idea that it is relative to a type system that may or may not be as “declarative” as you expect is key to compare and evaluate some of the more recent/advanced literature on type inference – to read the fine prints. “Has principal types” by itself does not necessarily mean that the type system is nice, if the reference system is very algorithmic in nature.

1 Like