Generalized Abstract Data Types

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 *)

let two = eval (App (App (Add, Int 1), Int 1))
 ==>  val two : int = 2

Unless you are familiar with the precedence of operators in type expressions, the above definition of term is likely to confuse you. With extra parentheses it is:

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

First we parse the definition of term and then of eval.

I think that “type z.” should be read as “for some type z ...”. More exactly we should say that for each instance of a value of this type, there is a type called z such that ... . Perhaps we need another BNF rule such as:
“typexpr ::= type ident . typexpr”. The scope of the ident is just the typexpr. The defining occurrence of ident is the one in “ident.” and the applied occurrences are all in typexpr.

One can usually, but not always turn “ident : typexpr” into just “ident” but not here. I do not claim to understand when the compiler infers types.

I have a prior notion of a well defined set of values and that type theory merely says what sets of these prior values there are that the compiler and programmer must reason about. It is true that most language defining documents usually introduce the values as a byproduct of defining the type and thus seem to suggest that the value is parasitic on the type. This, I think, is a pedagogical style that may be usually good, but not fundamental. This values-first stance reveals questions such as when two types are the same. In the set context it would seem that two types are the same just in case they encompass the same values.

Of course I have not asked a crisp question here. Some computing theories see floating 2 as the same value as fixed 2. There are languages of both persuasions that I like.

I am not objecting to OCaml or even its documentation; I am trying to understand the ideas behind OCaml with and without GADTs. Concretely I am trying to understand what the compiler does.

I note an incongruity in the syntax. Before GADT ‘->’ occurred only to the left of value expressions. The first ‘->’ in the example occurs to the left of type expressions. Similarly the asterisk, in a type context, denotes a Cartesian product. Here it authorizes the ‘(f,x)’ in ‘App(f,x) -> (eval f) (eval x)’. The asterisk suggests a tuple of values but this is not about tuples. I see a drift here towards making types first class values. This may be good but it is hazardous.

“eval : type a. a term -> a” is the 2nd option for a let-binding and “type a. a term -> a” is thus a typexpr. “” “”