let id = fn x -> x in (id 1, id true)

the function bound to id is given the type

forall a. a -> a

The values in the tuple expression are then type checked using instances of this type scheme, allowing the two uses of id to have different type instantiations.

The way I have seen this implemented in the past is by variants of the W algorithm. This algorithm uses unification to resolve two types to get a most general type of which the two types are an instance.

in id id

—-> In empty type environment fn x -> let y = x in y

—-> We generate a fresh type variable representing the type of x

——> In type environment x:b1, let y = x in y

——–> In type environment x:b1, x

——–< Return no substitution and type b1 for the expression

——> We generalize the result type, b1, for x, in an environment containing x. This generalization doesn’t effect

——> b1 in this case as this type is bound further out.

——–> In the type environment x:b1, y:b1 we process y

——–< Return no substitution and type b1

——< We return no substitution and the type b1

—-< We return no substitution and type b1 -> b1

–< We now know that id has type b1 -> b1. Because this is a let binding though, we generalise this

–< to forall b1. b1 -> b1. Hence uses of id inside the let body are going to allow separate instantiations.

—-> In type environment id: forall b1. b1 -> b1 process id id

——> In type environment forall b1. b1-> b1 process id

——< We instantiate the schema with new type variables and return no substitution and b2 -> b2

——> In type environment forall b1. b1-> b1 process id

——< We instantiate the schema with new type variables and return no substitution and b3 -> b3

—-> The applications causes a new type variable b4 to be generated for the result type of (id id)

—-> and we need to unify (b2-> b2) and (b3 -> b3) -> b4

—-> This gives substitions b2 = b3 -> b3 and b4 = b3 -> b3 and the result type is b4, which is transformed

—-> to b3 -> b3

–> The final type of the expression is b3 -> b3.

A = B reflects that A and B should be unified at a later stage of the type inferencing.

A <= B reflects that A should be a generic instance of B.

To handle the let bound polymorphism, there is a third constraint type,

A <{M}= B which reflects that the variables M should remain monomorphic during this unification.

–> let id = fn x -> let y = x in y in id id

—-> fn x -> let y = x in y in id id

——> let y = x in y

——–> x

——–< Generate a new type variable, b1, and return the environment x:b1 and type b1

——–> y

——–< Generate a new type variable, b2, and return the environment y:b2 and type b2

——< Return the environment x:b2 and generate the constaints b2 <{b1}= b1

—-< Introduce a fresh type variable b3 for the result type

—-< Generate constraints b2=b3

—-< and return type b3->b2 and an empty enivronment

–> Continue the body of the let

—-> Process (id id)

——> Process id

——< Return a fresh type variable b5 and environment id:b5

——> Process id

——< Return a fresh type variable b6 and environment id:b6

—-< Add constraints b5 = b6 -> b7 for a fresh b7, and result type b7 in type environment id:b5 id:b6

–< Result type is b7 and constraints are b5 <{}= b3 -> b2 and b6 <{}= b3 -> b2

b2 <{b1}= b1 forces b2=b1 and then the key is that b5 <{}= b3->b2 can only be solved after the constraint b2=b3 has been processed, showing that b5 <{}= b1->b1 ie that b5 has the polymorphic type

forall b1. b1 -> b1.