I recently realized that there is some sort of relation between Russellian type
ID: 650504 • Letter: I
Question
I recently realized that there is some sort of relation between Russellian type theory and type systems, as found e.g. in Haskell. Actually, some of the notation for types in Haskell seems to have precursors in type theory. But, IMHO, Russell motivation in 1908 was to avoid Russell's paradox, and I am not sure how that is related to type systems in computer science. Is Russell's paradox in one form or another something that we would have to worry about, for example, if we didn't have a good type system in a given language?
Explanation / Answer
`Type theory" in the sense of programming languages and in the sense of Russell are closely related. In fact, the modern field of dependent type theory aims to provide a constructive foundations for mathematics. Unlike set theory, most research in type theory based math is done in proof assistants like Coq, NuPRL, or Agda. As such, proofs done in these systems are not only "formalizable" but actually fully formal and machine checked. Using tactics and other proof automation techniques we try to make proving with these systems "high level" and thus resemble informal mathematics, but because everything is checked we have much better guarantees on correctness.
See here
Types in ordinary programming languages tend to be more limited, but the meta theory is the same.
Something similar to Russell's paradox is a major issue in dependent type theory. In particular, having
Type : Type
usually leads to contradiction. Coq and similar work by nesting universes
Type_0 : Type_1
but in Coq by default these numbers are implicit as they normally don't matter for the programmer.
In some systems (Agda, Idris), the type in type rule is enabled via a compile flag. It makes the logics inconsistent, but often makes exploratory programming/proving easier.
Even in more mainstream languages, Russell's paradox occasionally shows up. For example, in Haskell, an encoding of Russell's paradox combining impredicativity and open type case is possible, allowing one to build divergent terms with out recursion even at the type level. Haskell is ``inconsistent" (when interpret as a logic in the usual way) since it supports both type and value level recursion, not to mention exceptions. None the less, this result is rather interesting.