Standard syntax for preconditions, postconditions, and invariants

[Neil Mitchell]

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