Most maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problem

Most maths teaching emphasises this but they don't talk about it in quite the same way. Units are dealt with as units whenever you are doing real world problems around velocity, speed, physical quantities etc and you are taught not to mix units, and how units "cancel" etc each other when you deal with exponent laws. Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education. I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before. [1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.