# How to statically type polymorphic lambdas using hindley milner style type inference

I am playing with a simple implicitly typed functional language and have implemented type checking using a Hindley Milner style system. In order to guide code generation, I want to tag each term with its type during type inference.

Of course my language uses lambda expressions and the implicit typing should enable nice polymorphic use of those lambdas. Unfortunately, this goal clashes with the static type tagging as each lambda can be tagged only once which specializes it for a particular set of argument and closure types. It is also not possible to statically copy lambdas on each use, as this requires dynamic knowledge.

I thought about dynamically copying and tagging lambdas at runtime but this would involve quite some work and possibly overhead. Is there a standard solution for this kind of problem?

Update 1 The following example might help to clarify my point.

add := func (a, b) begin a + b end


The lambda add has polymorphic type (T1, T1) -> T1 and during type checking add is first instantiated to (Int, Int) -> Int and then to (Str, Str) -> Str, everything fine so far. But, during compilation, I want to have the tree representing add to be annotated with conrete types. Unfortunately, add is a single tree and that tree is either tagged with the first or the second type instantiation.

I could create copies of the add tree for each application but it seems to me that this is only possible at runtime, when the actual target of a call is available. On the other hand, maybe I could somehow let bind copies of the lambda for each instantiation and mangle the type variant into the name? That would entail updating references and I'm not sure whether this is actually possible in general? What about lambda return values, conditionals and so forth?

Update 2 I still feel like I did not describe my problem sufficiently. My language is really rather simple and I would like to stick with a simple typing solution. I found an article series that exactly details my problem and even explores the approaches that I envisioned: type spacialization per application and selecting specialized trees using a structured ler naming scheme.

• Type inference algorithms for HM style systems normally deduce polymorphic types for let-bound variables, whether they are lambdas or not. If you want to make it for lambdas in general (or in some circumstances), you could transform the expressions so all lambdas are let-bound before type inference. – Alexey Romanov Mar 9 at 9:33
• What is the type of +? It looks like you are already facing the exact same problem with +, as add is just a wrapper around it. – Andrej Bauer Mar 10 at 11:08
• +(a, b) is a predefined function that is overloaded for int, float, string etc. – Johannes Luong Mar 10 at 20:48

You should use a polymorphic lambda calculus, e.g. System F for representing typed terms. Then, when you generalize a let binding, you also insert lambdas which abstract over types, and when you check a function application, you also insert type applications as needed. This is precisely what GHC Haskell does, and is the standard solution.

Now, your concrete example does not fit into pure H-M inference, because you seem to be using an overloaded + operation. Unless + is implemented for every type or fails at runtime for some types, (T1, T1) -> T1 is not a valid polymorphic type for add.

For a pure H-M example program, elaborating to System F would look something like the following, with input:

id := func a begin a end
a  := id 'hello'
b  := id 100


And output:

id := Func A (func (a : A) begin a end)
a  := id [String] 'hello'
b  := id [Int] 100


Where I use Func A to mean a lambda binding a type (corresponding to big lambda in System F), and id [String] to mean applying the polymorphic id to a String type. The point of type lambdas and applications is to have an explicit internal representation of polymorphic functions.