2020-06-05
One day I was reading the wikipedia page on type systems (see here) and came across the quote:
any sound, decidable type system must be incomplete
I tried to read the source for that line (see here), but I couldn't understand it. I thought, surely that can't always be true? Aren't there some super simple type systems are sound, decidable, and complete? What does it mean for a type system to be sound, decidable or complete?
Let our type checker be M which takes a program w and returns true or false
M is sound if: for every program w, if M(w) is true, w will not have any run time type errors
M is complete if: for ever program w, if w would have no run time type errors, M(w) returns true
M is decidable if: for every input i, M(i) halts and returns true or false.
A trivial M that is sound and decidable, but not complete:
def M(w):
return false
A trivial M that is complete and decidable, but not sound:
def M(w):
return true
A trivial M that is sound and complete, but not decidable:
def M(w):
Run w
return true if there were no type errors while running w, false otherwise
But just because I came up with these examples, doesn't mean there isn't some sound, complete, and decidable M, right? Couldn't there be some super simple type system, that only has booleans, that we could create a sound, complete, and decidable type checker for?
Another issue I have is with our definitions of sound and complete. They're a little under specified: what is a "run time type error"? Not all run time errors are type errors, example: dividing by zero. What counts as a run time type error?
With all these questions, I want some answers. Also sometimes when I'm reading type system computer scienc-y adjacent things I come accross lambda calculus notation which I don't understand at all. I'd like to learn the basics of type theory at least. Also what is Curry Howard Correspondence? it sounds neat, programs as proofs? Also what are Hindley-Milner type systems? I've come accross those when reading about type inference and couldn't really understand its wikipedia page.
After some searching I came across Types and Programming Languages by Benjamin C. Pierce. I'll start reading this and see if it helps
On my earlier question about what counts as a "run time type error":
The bad behaviors that can be eliminated by the type system in a given lan- guage are often called run-time type errors. It is important to keep in mind that this set of behaviors is a per-language choice: although there is substan- tial overlap between the behaviors considered to be run-time type errors in different languages, in principle each type system comes with a definition of the behaviors it aims to prevent. The safety (or soundness) of each type system must be judged with respect to its own set of run-time errors. --Types and Programming Languages, Benjamin C. Pierce, page 3
literally in the introduction.
If the set of run time type errors is not locked down, couldn't I just make a type system, and say that the set of run time type errors is the empty set? then my type checker can just always return true, like the trivial example for sound and decidable above, since run time type errors never occur (there aren't any). In which case my type checker is complete.
There must be some context that wikipedia quote was assuming without stating. Or maybe the source it was quoting specified some earlier context about what type systems it was talking about.
My new question: Is there some level like: once your type system encodes such and such level of information your type checker can no longer be sound, complete, and decidable? If there is no exact level like this, are there some desirable common features of type systems that cause type checkers for those systems to not be sound, complete and decidable?