Frank Christoph:
> > I think he means the application term associated with second-order lambda
> > calculus' "big lambda," usually written "M [T]" or just "M T" where M is a
> > value term and T is a type term, e.g., "(/\X.\x.x) Int 3".
>
> Should be: "(/\X.\x:X.x) Int 3". (Doesn't make much sense if you don't say
> what type variable your abstracting...!)
That's exactly right. Sorry if I was being over-terse in my original.
Fergus is of course correct that you can write any type application
as a partial type spec too, if the syntax is thusly extended. However,
I think the type-ap style would in many cases still be somewhat more
concise, so it's not clear to me that the two are redundant -- or that
if they are, which is superior...
Cheers,
Alex.