Locally abstract type, polymorphism and function signature

Learning
2

An important point is that the meaning of type variables ('a, 'b, …) are slightly different in type signature and explicit type annotation.

Typically:

val fst: 'a * 'b -> 'a

means for all type 'a and 'b, the function fst takes a pair of 'a and 'b and returns a 'a.
Contrarily, the following function compiles:

# let not_fst: 'a * 'b -> 'a = fun (x,y) -> x + y;;
val not_fst: int * int -> int

because the explicit type annotation means: there are some types 'a and 'b such that not_fst has type 'a * 'b -> 'a. And in this case, those types 'a and 'b are actually int. If you want to express, that a function f should have the type 'a * 'b -> 'a, you need to add an explicit for all annotation:

# let fst: 'a 'b. 'a * 'b -> 'a = fun (x,y) -> x;;
val fst: 'a * 'b -> 'b

Here, the prefix 'a 'b. ... in the explicit type annotation means: for all 'a and 'b.
The important point is that this for all quantification is implicitly always here in type signature.

One way to look at this difference is that type annotation are here to help the type inference, whereas in type signature the inference is already done, so the syntax can focus on conveying the final type.

In fact locally abstract types are a good example of annotations which are needed for type inference, but never appear in type signature. Those types have mostly two use case: in local modules and in GADTs. For GADTs, there are needed to communicate that a type may be refined by pattern matching on a GADT.

For instance, your prop_eq function can be written:

let prop_eq (type n1 n2):  (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq =
  function Refl -> Refl

Here, we add a local type equation n1 nat = n2 nat on the right hand side of -> and use it to prove that
n1 s nat = n2 s nat.
Without such annotation, the typechecker would follow the normal global inference rule:

let prop_eq ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq =
  function Refl -> Refl

and deduce that 'n1 = 'n2 because Refl has type ('a,'a) eq.

Concerning the question of the difference between explicit polymorphic annotations and locally abstract types, the short version is that polymorphic annotations are needed for polymorphic recursion and locally abstract types for GADTs. Consequently, if you are defining a non-recursive function like prop_eq, you can use only a locally abstract type. However, if you are defining a recursive function on a GADT type, you probably need both. Your function are_equal is classical use case:

let rec are_equal: type n1 n2. n1 nat -> n2 nat -> (n1, n2) nat_lem = 
fun n1 n2 -> match n1, n2 with
  | Z, Z -> Left Refl
  | Z, S _ -> Right z_not_s
  | S _, Z -> Right s_not_z
  | S n1, S n2 -> propagate (are_equal n1 n2)

In the example above, type n1 n2. ... is a shorthand notation that combines an explicit polymorphic annotation with the introduction of two local abstract types n1 and n2. It is possible to split the two notion and rewrite are_equal as:

 let rec are_equal: 'n1 'n2. 'n1 nat -> 'n2 nat -> ('n1,'n2) nat_lem =
 fun (type n1) (type n2) (n1:n1 nat) (n2:n2 nat): (n1,n2) nat_lem ->
 match n1, n2 with
  | Z, Z -> Left Refl
  | Z, S _ -> Right z_not_s
  | S _, Z -> Right s_not_z
  | S n1, S n2 -> propagate (are_equal n1 n2);;

but this form is a bit of a mouthful, so most people only use the shorthand version.

6 Likes