Synopsis

This page gives information on the original implementation of GADTs in OCaml, now merged in trunk.

    svn checkout http://caml.inria.fr/svn/ocaml/trunk

Examples are in the subdirectory

  testsuite/tests/typing-gadts

which you can access directly at the following URL

  http://caml.inria.fr/cgi-bin/viewvc.cgi/ocaml/trunk/testsuite/tests/typing-gadts/

Status

About the implementation

The two following documents give some insights on the implementation and its theoretical background.

Example code

Intuition

To gain some intuition, we must first understand what I refer to as a newtype. In the expression:

fun (type s) -> e

the type s is a newtype, and is treated like a type constructor in e. The type s can take on other types, but only within a branch. For example, in the expression: 

let eval (type s) (x:s t) : s =
   match x with
   | IntLit x -> x
   | BoolLit x -> x

then the newtype s will have type int in the branch 

and bool in the branch 

Constructor level existential types

In the Exp example, we could define a type:

type anyt = Anyt : 'a t -> anyt

let eval_anyt (Anyt x) =
  try
    eval x ; 
    print_endline "evaluation succeeded"
  with _ -> 
    print_endline "evaluation failed"

Syntax extensions

Summary

Type parameters

type (_,_) t = u

type ('a,'b) t = u

type _ t = int

type 'a t = int

type +_ t = Foo : 'a t -> 'a t

Constructors

Mixing polymorphic recursion and newtypes

type _ t = 
     | IntLit : int -> int t
     | BoolLit : bool -> bool t

let eval : 'a . 'a t -> 'a = 
    fun (type s) (x : s t) -> 
          ((match x with
             | IntLit x -> x 
             | BoolLit x -> x) : s)

let eval : type a . a t -> a = function
   | IntLit x -> x
   | BoolLit x -> x

let rec f (type s) (x : s) = f x (* this does not type check *)

Here we try to call f with an argument of new type s. If we do not know that f is polymorphic in its argument, we get a type error.

Exhaustiveness check

Exhaustiveness check is done, to a great extent, by trying many possibilities. For example:

type _ t = 
    | BoolLit : bool -> bool t
    | IntLit : int -> int t

let same_type : type s . s t * s t -> bool = function
  | BoolLit _, BoolLit _ -> true
  | IntLit _, IntLit _ -> true

would pass the exhaustiveness check. However:

type _ t = 
  | BoolLit : bool -> bool t
  | IntLit : int -> int t
  | Impossible : float t -> float t

let same_type : type s . s t * s t -> bool = function
  | BoolLit _, BoolLit _ -> true
  | IntLit _, IntLit _ -> true

would not, even though it is impossible to construct a value with the Impossible constructor.

Sometimes, there isn't enough information to tell two types apart and this can effect exhaustiveness checking. For example:

module M : sig type t type u end = struct
  type t = int
  type u = bool
end

type _ t = 
  | BoolLit : M.u -> M.u t
  | IntLit : M.t -> M.t t

let same_type : type s . s t * s t -> bool = function
  | BoolLit _, BoolLit _ -> true
  | IntLit _, IntLit _ -> true

Unused match cases

Duplicate variants

type _ t = A : int t

let foo =
  function A -> () | A -> ()

Redundant underscore

Variance

Type constructors with GADT data constructors can be variant in all their type parameters which cannot introduce new equations.

For example, the following is correct:     

To see why this is the case, consider the following example (taken from Jacques Garrigue):

type -'a t = C : < m : int > -> < m : int > t

type eval : type a . a t -> a = fun (C x) -> x

let a = C (object method m = 5 end)

let b = (a :> < m : int ; n : bool > t)

let c = eval b

Limitations

Polymorphic variants

Patterns containing polymorphic variant patterns are not handled as GADTs. 
This is because propagating type information in patterns is required for GADTs, but might change types inferred for polymorphic variant patterns.

For example, the following code is not allowed:

Generation order

Within a pattern, constraints are generated, and can only be used, from left to right in tuples and in label definition order for records. For example:

would type but the function:

would not. The reason is that patterns are checked in this order during runtime so that check' might compare integers with booleans.

Note: for record patterns, left to right must be understood according to the definition order.

Propagation

let rec baz : type s . s t -> s =
  fun (type z) ->
  function
    IntLit x -> x
  | BoolLit y -> y

so you need to add the annotation:

let rec baz : type s . s t -> s =
  fun (type z) ->
  ((function
      IntLit x -> x
    | BoolLit y -> y) : s t -> s)

or, equivalently:

let rec baz : type s z . s t -> s =
  function
    IntLit x -> x
  | BoolLit y -> y

Exhaustiveness check

The exhaustiveness check is not complete. However, this is not new to O'Caml. Consider:

type a = {field : 'a. 'a list}

let foo = function {field = []} -> ()

This function is exhaustive, but it is flagged as being non-exhaustive. 

With GADTs, the problem becomes a little more severe. Consider:

type _ u = Int : int u | Bool : bool u
type _ v = VInt : int v

let foo =
  function Int, VInt -> ()

Even though foo is exhaustive it is flagged as being non-exhaustive. As a general rule, when matching on a tuple, the exhaustiveness check is more effective if you keep your wildcard patterns ( _ ) at the right most position in the tuple. 

Contact