5 ms·
From the article: "Definition. A type is a statement of the invariants of some expressions." To the author, a type is any mathematical statement that can be pr
by smadge 8y ago
From the article: "Definition. A type is a statement of the invariants of some expressions."
To the author, a type is any mathematical statement that can be proven about the code. This definition is so general that, yes, every computer language is typed, as we can prove things about programs in that language. For example: when provided with an integer as input this program produces as integer as output, this program will terminate, this program returns a sorted list of digits, this program will never divide by zero, this program recognizes sentences from this language, etc.
- roenxi 8y agoOn the one hand, I doubt the author was out to stir up criticism on HN. On the other, that definition is skirting quite close to defining everything in the known universe as typed - I suspect there is a hair splitting argument about whether the fundamentals of physics can be defined as a 'symbol' in an 'expression'. With that sort of starting point, it is no longer clear what the value of things being typed is. If everything has a type, what use is it to point out that a thing is typed? The results become too trivial to be worth discussing. A little further down this rabbit hole and we'll have discovered that mathematics encapsulates universal laws!
- smadge 8y agoI think the main point of the article is to shift type systems from being necessarily a part of the language itself to something that can exist outside the language and used to analyze it. For instance I once wrote a program which would infer types on a subset of Python and identify simple type errors without running it. That said there are languages which are more amendable to type checking. For example type checking a Ruby program which dynamically adds methods to a class.