PEPeaker·Dec 22, 2015
> We do not know a whole lot about code just because it has type checked. It may feel like you do, but that's just a feeling.
You can know a whole lot because it type-checked. What exactly you know depends on how you leveraged the type system.
For example, if you define a red black tree as is defined here:
https://github.com/yairchu/red-black-tree/blob/master/RedBla...
You know code will never generate trees that break the red/black invariants. The tree is guaranteed to be balanced by the type checking process.
> The name of the function might be `sort`, but it could actually fail to sort items, in spite of type checking
Unless you use a dependently-typed language.
Consider this `sort` definition:
sort : (in:List n a) -> (out:SortedList n a, IsPermutation in out)
"List n a" is a list of length "n" of values of type "a".
"SortedList n
Read the rest
a" is a sorted list of length "n" of values of type "a". "IsPermutation a b" is a proof that a is a permutation of b (returned from sort).
Here's how you can define a type like SortedList:
type SortedList n a =
exists min. SortedList' min n a
data SortedList' min n a where
Empty : SortedList' min 0 a
Cons : LessOrEq x y -> (x:a) -> SortedList' y n a -> SortedList' x (1+n) a
SortedList thus embeds a proof alongside each element that it is less than or equal to the lower-bound of the remaining list (i.e: the next element).
Type-checking this guarantees that `sort` does the right thing, modulo resource-use/performance (or termination, depending on your type checker).
Resource use (bounding) can also be type-checked, but requires leveraging the type system even more.
These guarantees aren't free -- you have to write the types for them, and you have to prove them by instantiating values of these types. But you can opt in or out of each of these guarantees -- leverage the type system as much as you want.
With dynamic typing, you just don't have this tool at your disposal at all. No flexibility to guarantee anything. You're forced to opt out completely.