5 ms·

> 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

by Peaker 11y ago

> 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/RedBlackTree.hs#L26-L37 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 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.

AnimalMuppet 11y ago
Please clarify something for me: Does that "proof" run a run time, or at compile time? If at compile time, how does it do so without running into something like the halting problem?
- mokus 11y ago
  It does run at compile time, and it doesn't run afoul of Rice's theorem (a useful generalization of the theorem about the halting problem) because it's not implementing a general decision procedure that can decide for _all_ programs whether the property holds. It's possible to solve halting-class problems for restricted subsets of programs, as well as to enlarge those subsets greatly by forcing the user to help. For example, I can trivially "solve" the halting problem for the subset of programs that contain no loops or recursion, by simply refusing to make a decision on programs that do. I can also solve it for the subset of all programs that do halt by simply running the program and reporting when it halts that it does, in fact, halt. More usefully, the type systems in Peaker's examples rely on user-provided annotations to help the compiler "see" the truth of the user's claims (or equivalently, the compilers restrict the class of programs they operate on to those programs which contain sufficient user-provided annotations). The compiler doesn't have to prove everything itself - it only has to check that the proof is valid according to the rules of the relatively simple logic of the proof system. The history of type systems has largely been a story of improving these logics and inference systems to reduce the amount of help needed from the user and enlarge the class of things that can be proven about programs. In this context, Rice's theorem amounts to saying that, no matter how complicated you make your type system, there will _always_ be programs that either (a) are valid but not accepted, or (b) are accepted but not valid.
  - AnimalMuppet 11y ago
    So is it fair to say that you are proving to the compiler that your function will return a sorted list (rather than you handing an arbitrary function to the compiler, and the compiler decides whether it returns a sorted list)?
    - mokus 11y ago
      Yes, and in general it's pretty clear as you're doing it that that's what's happening. The ML family and Haskell type systems occupy a pretty nice place on the spectrum of expressiveness in that there's not much you can add to them without losing the ability to infer unique types. As long as your types are on the same level of complexity as a Haskell or ML type, you can typically get away with minimal type annotations - a bit more than ML or Haskell would've required, but not a lot more. When you introduce more complex quantifiers such as the "exists" in these examples, in practice you have to start thinking about "what the compiler knows" and how to help it know the things you want it to. There are some systems such as Coq that use heuristics (and let you write your own new heuristics) to try to automatically find proofs, and interactive sessions in which you guide the system to the proof by suggesting tactics that move hypotheses toward goals or vice versa. This is one of the major factors that, in common speech, distinguishes between "typed languages" and "proof assistants" which otherwise are basically the same kind of thing. Even in proof assistants, though, you still need to be quite intentional about what lemmas need to be proven in order to move toward your ultimate goal, and often even in how you phrase your goals in order to improve the chances that the heuristics will find a proof. These are the kinds of things i mean by "helping" the system in my previous comment. They are very powerful tools if assurance of correctness is a high priority, but definitely not a free lunch. If you're ever interested in going down the rabbit hole, there's a pretty steep learning curve (though if you're comfortable with ML or Haskell you're already halfway up it) but an extensive and rewarding landscape of thought at the top. Unfortunately it's more of an academic or self-enrichment discipline than an industrial one these days, but if you look hard enough there are a few jobs where you can make use of these tools.
kazinator 11y ago
That would be useful if it could be applied to normal red-black trees and sorting. As in, respectively, the efficient, destructive algorithm which inserts into a tree, rendering it temporarily unbalanced and non-red-black, and then fixes it up; and an internal quicksort on an array.
- Peaker 11y ago
  Why is only destructive useful?

by Peaker 11y ago

AnimalMuppet 11y ago

Please clarify something for me: Does that "proof" run a run time, or at compile time? If at compile time, how does it do so without running into something like the halting problem?

mokus 11y ago
It does run at compile time, and it doesn't run afoul of Rice's theorem (a useful generalization of the theorem about the halting problem) because it's not implementing a general decision procedure that can decide for _all_ programs whether the property holds. It's possible to solve halting-class problems for restricted subsets of programs, as well as to enlarge those subsets greatly by forcing the user to help. For example, I can trivially "solve" the halting problem for the subset of programs that contain no loops or recursion, by simply refusing to make a decision on programs that do. I can also solve it for the subset of all programs that do halt by simply running the program and reporting when it halts that it does, in fact, halt. More usefully, the type systems in Peaker's examples rely on user-provided annotations to help the compiler "see" the truth of the user's claims (or equivalently, the compilers restrict the class of programs they operate on to those programs which contain sufficient user-provided annotations). The compiler doesn't have to prove everything itself - it only has to check that the proof is valid according to the rules of the relatively simple logic of the proof system. The history of type systems has largely been a story of improving these logics and inference systems to reduce the amount of help needed from the user and enlarge the class of things that can be proven about programs. In this context, Rice's theorem amounts to saying that, no matter how complicated you make your type system, there will _always_ be programs that either (a) are valid but not accepted, or (b) are accepted but not valid.
- AnimalMuppet 11y ago
  So is it fair to say that you are proving to the compiler that your function will return a sorted list (rather than you handing an arbitrary function to the compiler, and the compiler decides whether it returns a sorted list)?
  - mokus 11y ago
    Yes, and in general it's pretty clear as you're doing it that that's what's happening. The ML family and Haskell type systems occupy a pretty nice place on the spectrum of expressiveness in that there's not much you can add to them without losing the ability to infer unique types. As long as your types are on the same level of complexity as a Haskell or ML type, you can typically get away with minimal type annotations - a bit more than ML or Haskell would've required, but not a lot more. When you introduce more complex quantifiers such as the "exists" in these examples, in practice you have to start thinking about "what the compiler knows" and how to help it know the things you want it to. There are some systems such as Coq that use heuristics (and let you write your own new heuristics) to try to automatically find proofs, and interactive sessions in which you guide the system to the proof by suggesting tactics that move hypotheses toward goals or vice versa. This is one of the major factors that, in common speech, distinguishes between "typed languages" and "proof assistants" which otherwise are basically the same kind of thing. Even in proof assistants, though, you still need to be quite intentional about what lemmas need to be proven in order to move toward your ultimate goal, and often even in how you phrase your goals in order to improve the chances that the heuristics will find a proof. These are the kinds of things i mean by "helping" the system in my previous comment. They are very powerful tools if assurance of correctness is a high priority, but definitely not a free lunch. If you're ever interested in going down the rabbit hole, there's a pretty steep learning curve (though if you're comfortable with ML or Haskell you're already halfway up it) but an extensive and rewarding landscape of thought at the top. Unfortunately it's more of an academic or self-enrichment discipline than an industrial one these days, but if you look hard enough there are a few jobs where you can make use of these tools.

kazinator 11y ago

That would be useful if it could be applied to normal red-black trees and sorting. As in, respectively, the efficient, destructive algorithm which inserts into a tree, rendering it temporarily unbalanced and non-red-black, and then fixes it up; and an internal quicksort on an array.

Peaker 11y ago
Why is only destructive useful?