4 ms·
I don't know my way around Type theory, but I have done a fair bit of Mathematics and Programming. Mathematics is largely based on set theory, so every element
by heinrichhartman 9y ago
I don't know my way around Type theory, but I have done a fair bit of Mathematics and Programming.
Mathematics is largely based on set theory, so every element has a set it belongs to, and every function has a source-set (domain) and a target-set (co-domain). Mathematicians are very careful to always qualify the encompassing sets, domains and co-domains. You would always write:
* Let x \in X be a point in Space.
* Let f:A->B be a fuction with ceratin properties.
This is even more pronounced in Category theory, which invaded algebra and geometry quite heavily. Where the only thing you know about a function is it's domain, codomain and how it composes.
So, yes. Mathematics on a practical level is _very_ type aware.
And it also prevents you from doing stupid stuff: f:A->B, g:A->C, can't be composed, so f(g(x)) is a "type error".
- Drup 9y agoWhile Mathematics is type aware, Mathematicians often aren't. They mix things that are "not the same object, but almost, I swear", and constantly write ill-typed expressions. This is generally on purpose, to avoid making explicit things that are obvious, but as someone developing and using statically typed languages, reading Math papers is often quite frustrating.