What's the F# type inference approach to generics?

Question

I'm trying to understand rules around type inference as I'd like to incorporate it into my own language, and in that spirit I've been playing around with F#'s type inference, and the following struck me as odd.

This compiles, and id is 'a -> 'a, which (if I am not mistaken), means that every invocation is using a "fresh" type.

let id x = x

let id1 = id 1
let id2 = id "two"

But when using an operator, it seems to be that the first invocation determines the signature for that function going forward.

Here, mul is reported as being int -> int -> int

let mul x y = x * y

let mul1 = mul 1 2
let mul2 = mul 1.1 2.2 // fails here

If I reorder them, then mul is float -> float -> float:

let mul x y = x * y

let mul2 = mul 1.1 2.2
let mul1 = mul 1 2 // fails here

Could you explain (in preferably non-academical) terms what the rules are and perhaps how it works from the perspective of the type checking implementation? Does it walk over the functions to check their types every time they are referenced? Or is there some other approach?

Answer 1

First note that this will not happen if we declare mul as an inline function:

let inline mul x y = x * y

let mul1 = mul 1 2  // works
let mul2 = mul 1.1 2.2 // also works

Here the inferred type of mul will be as follows:

x: ^a -> y: ^b ->  ^c
    when ( ^a or  ^b) : (static member ( * ) :  ^a *  ^b ->  ^c)

This type means that the parameters x and y can have any type (doesn't even have to be the same type) as long as at least one of them has a static member named * that takes arguments of the same types as x and y. The return type of mul will be the same as that of the * member.

So why don't you get the same behavior when mul isn't inline? Because member constraints (i.e. type constraints that say that a type must have specific members) are only allowed on inline functions - that's also why the type variables have a ^ in front instead of the usual ': to signify that we're dealing with a different, less limited kind of type variable.

So why does this limitation on non-inline functions exist? Because of what .NET supports. Type constraints like "T implements the interface I" are expressible in .NET bytecode and thus allowed in all functions. Type constraints like "T must have a specific member named X with type U" are not expressible and therefore not allowed on ordinary functions. Since inline functions don't have a corresponding method in the generated .NET bytecode, there is no need for their type to be expressible in .NET bytecode and therefore the limitations don't apply to them.