Types only appear in type theory in mathematics. The rest of it is based around objects built on top arbitrarily tall towers of sets which types are simply unable to capture.

The smarts in mathematics is based in the rewrite rules, not the objects they apply to. Since you do not specify what rules apply that is just a term that is already in its normal form since we have no other rules we can apply.

That you assume we are dealing with real numbers merely stems from the fact that books are too lazy to state the rules explicitly in every calculation (and with good reason) and expressions with real numbers are the most common ones that people have exposure to in the average undergraduate course.

>The smarts in mathematics is based in the rewrite rules

Can't it be argued that types are simply a way to associate a considerable amount of rewrite rules and constraints with expressions and therefore spare you the trouble of repeatedly stating them again and again ?

If the type system is rich enough that custom types encode rules just as rich, powerful, concise, etc... as native types while being interoperable with them, I would say this is much, much better than a blind rewriter who either does nothing until you provide it with a rulebook or does everything it can unless you explicitly forbid it. You can just say that that every object/expression has a rulebook attached to it instead and add meta-rules to specify how rulebooks are defined, used and extended.

In the same way that objects are just tables in disguise. Sure it's true in some way, but the impedance mismatch is huge and horrible.

There is a reason why the internals of all major cas systems use rewrite rules instead of objects with types.

As a toy test try and implement a system that simplifies an expressions of a given group to normal form for that group. Using rewrite rules you end up with a program that is dozen of lines long and even better is provably correct by hand. Using types and functions on types you end up with a monstrosity that is 10 times as long and just feels clunky. Worse even something as simple as adding a super group of which your example is a sub group requires a rewrite of the program. Using rewrite rules on the other hand merely adds a few more if/else clauses in the main program.

Types are a fetish of the programming community and are used in places where they are actively detrimental. This stems from the fact the majority of programmers do not understand the difference between types and constraint rules.

This is why we've ended up at a mixed approach. Types in Julia are used to "distinguish between things". Multiple dispatch then is a great system for defining rules that are specific to groups: `AbstractMatrix` types have non-commutative rulesets, and we then let them have different rules from `Real` and let subtyping control at a finer grain what rules apply to which pieces, and what rules apply when you combine them.