Standard syntax for preconditions, postconditions, and invariants

[Taral]

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