|
|
|
|
|
|
by anyfoo
1000 days ago
|
|
|
It means that the type system can prove certain properties for you. For example, in languages with dependent type systems like Agda, you can construct a sorted list type that the compiler will prove it sorted at all times, otherwise it won’t compile. Or a complex tree type that is always balanced. Or a set of only even numbers, and again it won’t compile otherwise… (Sadly, if you go that far, it isn’t generally Turing complete anymore. Though in some cases that’s a good thing.) |
|
|