The limits of Hindley-Milner

The simplest thing in the world. Concatenate two pairs of lists component-wise:

# fun (a, x) (b, y) -> (a @ b, x @ y) ;;
- : 'a list * 'b list -> 'a list * 'b list -> 'a list * 'b list = <fun>

Why, let's abstract out the concatenation part and call it thread, so that it lifts a binary function to operate on pairs component-wise:

# let thread f (a, x) (b, y) = (f a b, f x y) ;;
val thread : ('a -> 'b -> 'c) -> 'a * 'a -> 'b * 'b -> 'c * 'c = <fun>

Aaaaaargh! Hindley-Milner doesn't let f to have different types in different application sites, so it forces both components of each pair to be equal. I'd wish at least for thread to have the type

val thread : ('a . 'a -> 'a -> 'a) -> 'a * 'b -> 'a * 'b -> 'a * 'b

Is there any way to do this with polymorphic records?


Alain Frisch said...

Yes, polymorphic record fields give you such first-class polymorphism:

type binop = { apply: 'a. 'a -> 'a -> 'a }

let thread f (a, x) (b, y) = (f.apply a b, f.apply x y)

Matías Giovannini said...


I tried that, but I stumbled trying to actually build such a binop. I understand that the type of the label apply means "this is a value that, for all 'a, takes an 'a and an 'a and returns an 'a". As far as I can see parametricity dictates that the type is empty. It is here where I think, what am I missing?

Alain Frisch said...

I thought that by

val thread : ('a . 'a -> 'a -> 'a) -> 'a * 'b -> 'a * 'b -> 'a * 'b

you actually meant that the first argument had to be polymorphic.

Parametricity does not imply that the type binop is empty. Pure and total functions in this type are (fun x y -> x), (fun x y -> y). But in OCaml, you have many more functions, like min, max, (fun x y -> if Random.int 2 = 0 then x else y), etc...

But it seems that what you really want is a way to pass a "function" that has two unrelated types (like (int list -> int list -> int list) and (string -> string -> string), but not necessarily (int -> int -> int)). What about using a pair of functions?


let thread (f, g) (a, x) (b, y) = (f a b, g x y)

ssp said...

Hello, it seems no way to do what you want. I'm not able to find original discussion, but some results are summarised at