No, it's about proving something about your program. Types are theorems about programs. If a compiler type checks (well if it is a sound type system) that your

No, it's about proving something about your program. Types are theorems about programs. If a compiler type checks (well if it is a sound type system) that your function returns an non-zero integer, it proves that it can only return non-zero integers. And you can write that kind of constraint in types. Types can be very expressive! You can even check that all variables are within scope in a lambda expression by using an appropriate encoding (de Brujin indexes users integers instead of variable names) for the expression. Typically you provide hints or even proofs for the compiler; they mix with something called proof assistants. Scala looks hacky at it. If you want cleaner examples, look at the Coq, agda, epigram and idris languages.