[groovy2shoes]

I understand the notation, but I don't understand the reasoning behind the Abs+App restriction (why does it have to be that way). I've been working on my own language and haven't gotten to the type inference yet, so maybe I'll finally understand once I go through it.

If the SPJ book is the one about implementing functional languages, then I've got a copy on my laptop I can peruse when I get home from work.

[gsg]

The difference between abstraction bindings and let bindings is that let variables are only ever bound to the value of a single expression, whereas the argument of a function may be bound to the value of any number of expressions.

This causes difficulties because the set of free type variables needs to be calculated in order for generalisation to produce safe type schemes, and that is tough to do for an unknown set of expressions.