On 10/19/06, Neil Mitchell <[EMAIL PROTECTED]> wrote:
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 <[EMAIL PROTECTED]> "You can't prove anything." -- Gödel's Incompetence Theorem _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
