Jon Pretty

Interesting how ructc uses "ty" while scalac uses "tpe".

… and Isabelle uses "typ"

Embrace the backticks. We should use "`type`"!

why am I not surprised that this is coming from you

Maybe because I've been saying for years, a) features exist so they can be used, and b) arbitrary choices (e.g. choice of abbreviation) are not intuitive, while taking the uniquely obvious option, even if it's slightly inconvenient, is.

How many times and across how many people are you willing to multiple that "slightly inconvenient" before you consider the alternative (teaching newcomers that "tpe" means "type") a better trade-off?

The trade-off is on the learning curve, for the benefit of the uninitiated and to the detriment of the experienced. Everyone has the cost of learning that tpe = type, but only the subset who use it extensively feel the cost of typing the backticks.

I will offer that by the time you encounter tpe its naming is the least of your problems.