Is it possible to program and check invariants in Haskell?
haskell, invariants, theorem-proving, types
Solution
Well, the answer is yes and no. There's no way to just write an invariant separate from a type and check it. There was an implementation of this in a research fork of Haskell called ESC/Haskell, however: http://lambda-the-ultimate.org/node/1689
You do have various other options. For one, you can use asserts: http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html
Then with the appropriate flag, you can turn off these asserts for production.
More generally, you can encode the invariants in your types. I was going to add more here, but dons beat me to the punchlines.
One more example is this very nice encoding of red-black trees: http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/
Problem
When I write an algorithm I usually write down invariants in comments. For example, one function might return an ordered list, and the other one expect that a list would be ordered. I'm aware that theorem provers exists, but I have no experience using them. I also believe that smart compiler [sic!] can make use of them to optimize the program. So, is it possible to write down invariants and make compiler check them?