Questions about GADT examples

Learning
1

I read the example in GADT, and have some questions about the code;

 type _ term =
   | Int : int -> int term
   | Add : (int -> int -> int) term
   | App : ('b -> 'a) term * 'b term -> 'a term

 let rec eval : type a. a term -> a = function
   | Int n    -> n                 (* a = int *)
   | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
   | App(f,x) -> (eval f) (eval x)
           (* eval called at types (b->a) and b for fresh b *)

what’s the meaning of type a.a term in the eval function?

1 Like
2

It is a polymorphic locally abstract type. To infer the type parameter of the GADT in the eval function, you need a locally abstract type. Because eval is recursive (it calls itself) it must be a polymorphic locally abstract type so that the type will be separately inferred on each recursive call.

Polymorphic locally abstract types use the dot notation you have seen. You will also see it used with first class modules. The explanation in the manual is here: OCaml - Language extensions

3

Thanks, so type a is a local abstract type, and this function will accept input which type is a term, is my understanding is correct?

4

As final result our function will have normal polymorphic type 'a term -> 'a. But we can’t do straightforward type inference as we usually do for normal algebraic datatypes — in general case there is not the most general type for functions with GADTs.

  1. We remember that we finally want to get normal forall-quantified polymorphism (in ideal case)
  2. We pick an arbitrary type from this forall-quantified collection of types.
  3. This type is kind of fixed for typing this concrete function body, that’s why it doesn’t have an apostrophe and is called local.
  4. It was picked arbitrarily, so we don’t know it’s implementation, that’s why it’s called abstract.

AFAIR, Haskell doesn’t have local abstract types, they write normal standard polymorphic signatures. Maybe it’s because they use another algorithm for type inference of GADTs, maybe some other reason exists. I think more experienced members of our community can provide exact answer why OCaml has concept of “locally abstract types”, and other languages don’t use these words.

5

My knowledge of ocaml’s type system is incomplete but as I have understood locally abstract types, they give a local name to a deduced type which can be referred to in the body of the function concerned. From that point of view they are quite useful.

For some reason which I have not fully delved into but is presumably connected with how GADTs are implemented, locally abstract types are also required for dealing with GADTs polymorphically: you will notice that the return type of eval is polymorphic. Even though in your example the type parameter of term is necessarily limited to those supplied by the variant cases, as mentioned by @Kadaku eval's signature is 'a term -> 'a, that is to say the type variable 'a is universally quantified. Why that happens I am not sure: the result is desirable and necessary, and I just accept it.