On 10/19/06, Neil Mitchell
Hi
reverse @ ensure { reverse (reverse xs) == xs }
Question, does "reverse [1..]" meet, or not meet this invariant?
This is a good point. You can only do sensible conditions on functions if appropriate termination constraints are met.
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?
This invariant holds at the time you build the RBNode. It's effectively a precondition on the RBNode "function".
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.
I agree that Haskell' will not have this, if only under the "must
already be implemented" requirement for major features. However, it
seems that Haskell' is a good way to get people thinking about future
improvements, and I'd hate to stifle that.
--
Taral