3 ms·
That doesn't seem to be any sort of refutation of the given complaint. Sure, Terrence Tao is a great mathematician, and he may trying to do something that type
by gliese1337 14y ago
That doesn't seem to be any sort of refutation of the given complaint. Sure, Terrence Tao is a great mathematician, and he may trying to do something that type theorists haven't done yet, and we can reasonably give him the benefit of the doubt and assume that, even though he didn't mention it, he may well be familiar with type theory and left out reference to it on purpose.
Nevertheless, for some audience, in which I am included, the connection to type theory seems blatantly obvious and it would've been a better article for us had it been presented in that light.
- banachtarski 14y agoIt's not the same as type theory because the relationships between physical units are actually tied by real mathematical operations. A float and a string do not combine in any sensible way (aside from type-casting, which is entirely different). This suggests that type theory as you are familiar with isn't as connected as you might think.
- gliese1337 14y agoSure they do- by "multiplication" to form an instance of an algebraic product type (float,string).
- evincarofautumn 14y agoThere are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notions of exponentiation, division, subtraction, complement, union, and intersection. There is little formal reason why an algebra of types shouldn’t include even more interesting operations.