Now, this may sound a stupid question, but I am no guru of mathematics and type theory... Could somebody point me to some documents explaining what the principal typing is and why is it useful? (Supposedly, this is some property that type inference systems should have...)

- Tom