Polymorphic functions and type inference in SML

user_19482605 0
Viewed 57

Consider this function in Standard ML.

fun times_until_zero(f, x) =
  if x = 0 then 0 
  else 1 + times_until_zero(f, f x)

REPL shows that times_until_zero has type (int -> int) * int -> int. But why isn't the type ('a -> int) * int -> int? All I can see from the function definition is that x has to be int and f has to take an argument which is at least as general as int and f has to return int. I tested it together with a function binding fun g x = 0 (so g has type 'a -> int) and times_until_zero(g, 10) returned 1 just fine.

type-inference sml
1 Answers

If times_until_zero had the type you suggest, then a caller would be allowed to do the following:

times_until_zero (string_to_int, 10)

where string_to_int : string -> int parses a string into an integer. Clearly, the call to f would not be type-correct anymore.

The subtlety here is where 'a is quantified, i.e., who gets to choose an instantiation. In the ML type system, the quantifier is always implicitly placed at the outermost position. That is, the type

('a -> int) * int -> int

actually means

forall 'a. (('a -> int) * int -> int)

Consequently, the caller of the function gets to pick a type for 'a.

For your example to be type-correct, you'd need the type

(forall 'a. ('a -> int)) * int -> int

With this the callee, i.e., your function, gets to pick a type for 'a, and can in fact pick a different one every time it calls f. On the flip-side, applying string_to_int would no longer be type-correct, since that function does not have the necessary polymorphic type.

However, types like the above with inner quantifiers (called higher-rank polymorphism) are not supported in plain ML, simply because type inference for them is not decidable in general.

user_10977800
Related