3 ms·
Types do not need to have a one-to-one correspondence with runtime data structures and indeed in many type systems often do not. In the limit, a type does not n
by dwohnitmok 6y ago
Types do not need to have a one-to-one correspondence with runtime data structures and indeed in many type systems often do not. In the limit, a type does not need to have any runtime representation at all (this is more than just generic erasure or phantom type parameters, you can have an entire type signature that has absolutely no runtime representation of any of its parts).
There is not really a fundamental difference between types and static analysis.
- jacinabox 6y agoA predicate is a computer program that accepts an input and returns "yes/no." A type system could be an arbitrary predicate which returns "well typed/not well typed" when given a term. But obviously there must be some difference between types and predicates, such as extensionality -- the type of an expression can be decided by examining the code alone.
- dwohnitmok 6y agoAre you responding to my assertion that there's no fundamental difference between type systems and static analysis? If so, if we just change "well typed/not well typed" to "acceptable/not acceptable" I think you've pretty much just described static analysis.