Locally abstract types

[mimoo]

(* an example with type variables that produces a bug *)
let map (x: 'a * 'a) (f:'a -> 'b) : ('b * 'b) =
    let x1, x2 = x in   
    (f x1, x2)

gives

val map : 'b * 'b -> ('b -> 'b) -> 'b * 'b = <fun>

whereas it should be (f x1, f x2)

keeping type abstracts prevents unification, which would have had the compiler yell at us:

let map (type a b) (x: a * a) (f:a -> b) : (b * b) =
    let x1, x2 = x in   
    (f x1, x2)

gives us: Error: This expression has type a but an expression was expected of type b

Also, it's useful for GADTs (see GADT section)

[mimoo]

the other syntax is also useful, as noted by the manual it allows functions to be generic:

let rec f : type t1 t2. t1 * t2 list -> t1 = …

or does it really make the function generic? I remember reading that you should use records to make argument of functions generic.

As in:

type ('a, 'b) generic_fn = { f : 'a -> 'b }

let fn (f : (_, _) generic_fn) = ...

but I'm not sure where this is useful, I can already write this:

utop # let fn ( f : 'a -> 'b ) ( a : 'a ) = f a;;
val fn : ('a -> 'b) -> 'a -> 'b = <fun>

[mimoo]

I guess that doesn't work for functions like Fn.id or acting on containers. For example:

let concat (l1 : 'a list) (l2 : 'a list) : 'a list = ...

I wouldn't be able to apply it to something like this:

let (a : (int list * int list)) (b : (string list * string list)) ~(f : 'a list -> 'a list -> 'a list) = ...

because it would need 'a to be int at first, but then to be string later