5 ms·

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 impl

by 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.

by mokus 11y ago

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.