Understanding the type error: "expected signature Int*Int->Int but got Int*Int->Int"

Question

The comments on Steve Yegge's post about server-side Javascript started discussing the merits of type systems in languages and this comment describes:

... examples from H-M style systems where you can get things like:

expected signature Int*Int->Int but got Int*Int->Int

Can you give an example of a function definition (or two?) and a function call that would produce that error? That looks like it might be quite hard to debug in a large-ish program.

Also, might I have seen a similar error in Miranda? (I have not used it in 15 years and so my memory of it is vague)

Answer 1

I'd take Yegge's (and Ola Bini's) opinions on static typing with a grain of salt. If you appreciate what static typing gives you, you'll learn how the type system of the programming language you choose works.

IIRC, ML uses the '*' syntax for tuples. <type> * <type> is a tuple type with two elements. So, (1, 2) would have int * int type.

Both Haskell and ML use -> for functions. In ML, int * int -> int would be the type of a function that takes a tuple of int and int and maps it to an int.

One of the reasons you might see an error that looks vaguely like the one Ola quoted when coming to ML from a different language, is if you try and pass arguments using parentheses and commas, like one would in C or Pascal, to a function that takes two parameters.

The trouble is, functional languages generally model functions of more than one parameter as functions returning functions; all functions only take a single argument. If the function should take two arguments, it instead takes an argument and returns a function of a single argument, which returns the final result, and so on. To make all this legible, function application is done simply by conjunction (i.e. placing the expressions beside one another).

So, a simple function in ML (note: I'm using F# as my ML) might look a bit like:

let f x y = x + y;;

It has type:

val f : int -> int -> int

(A function taking an integer and returning a function which itself takes an integer and returns an integer.)

However, if you naively call it with a tuple:

f(1, 2)

... you'll get an error, because you passed an int*int to something expecting an int.

I expect that this is the "problem" Ola was trying to cast aspersions at. I don't think the problem is as bad as he thinks, though; certainly, it's far worse in C++ templates.

Answer 2

It's possible that this was in reference to a badly-written compiler which failed to insert parentheses to disambiguate error messages. Specifically, the function expected a tuple of int and returned an int, but you passed a tuple of int and a function from int to int. More concretely (in ML):

fun f g = g (1, 2);

f (42, fn x => x * 2)

This will produce a type error similar to the following:

Expected type int * int -> int, got type int * (int -> int)

If the parentheses are omitted, this error can be annoyingly ambiguous.

It's worth noting that this problem is far from being specific to Hindley-Milner. In fact, I can't think of any weird type errors which are specific to H-M. At least, none like the example given. I suspect that Ola was just blowing smoke.

Answer 3

Since many functional language allow you to rebind type names in the same way you can rebind variables, it's actually quite easy to end up with an error like this, especially if you use somewhat generic names for your types (e.g., t) in different modules. Here's a simple example in OCaml:

# let f x = x + 1;;
val f : int -> int = <fun>
# type int = Foo of string;;
type int = Foo of string
# f (Foo "hello");;
This expression has type int but is here used with type int

What I've done here is rebind the type identifier int to a new type that is incompatible with the built-in int type. With a little bit more effort, we can get more-or-less the same error as above:

# let f g x y = g(x,y) + x + y;;
val f : (int * int -> int) -> int -> int -> int = <fun>
# type int = Foo of int;;
type int = Foo of int
# let h (Foo a, Foo b) = (Foo a);;
val h : int * int -> int = <fun>
# f h;;
This expression has type int * int -> int but is here used with type
  int * int -> int