Hi
reverse @ ensure { reverse (reverse xs) == xs }
Question, does "reverse [1..]" meet, or not meet this invariant? What is the type signature for reverse? What about "reverse [(+),(-)]" ? Is anything going to be said about the semantics of the invariants? Or are we just reserving a little piece of syntax that no one else is going to trample on?
invariant RedBlackTree a where RBNode False _ l _ r ==> redDepth l == redDepth r
Where does this invariant hold? At all points in time? After a call has executed? Only between module boundaries? I'd be wary about taking too much time to specify the syntax of this kind of thing, and skipping the issue of semantics entirely :) Also, you might want to look at the programatica project, which I think has had invariants in their code for years. I'm not sure if the syntax is the same or not. That said, I think that embedding invariants/pre/postconditions in the code is very useful, I just don't think that Haskell' is a good target for this - there is a big design space that no one has yet explored. Thanks Neil