On 10/19/06, Neil Mitchell <ndmitchell@gmail.com> 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 <taralx@gmail.com> "You can't prove anything." -- Gödel's Incompetence Theorem