5 ms·
It'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
by banachtarski 14y ago
It'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.