> Ralf: can you supply other examples?
Sure thing. A while ago I implemented several popular priority queue
structures. Being tired of proving them correct I worked out a simple
method of checking their correctness (or rather: the absence of errors)
at run-time. The idea is to cross-check a new implementation with a
trusted old implementation.
> newtype ControlBy q p a = Control (q a, p a)
>
> instance (PriorityQueue q a, PriorityQueue p a, Show (p a))
> => PriorityQueue (ControlBy q p) a where
> empty = Control (empty, empty)
> single a = Control (single a, single a)
> meld (Control (q1, p1)) (Control (q2, p2))
> = Control (meld q1 q2, meld p1 p2)
> splitMin (Control (q, p)) = case (splitMin q, splitMin p) of
> (Null, Null) -> Null
> (Null, Cons _ _) -> error (show p ++ ": priority queue is not empty")
> (Cons _ _, Null) -> error (show p ++ ": priority queue is empty")
> (Cons a q', Cons b p')
> | a == b -> Cons a (Control (q', p'))
> | otherwise -> error (show p ++ ": wrong minimum")
To be able to print the faulty queue a context of the form `Show (p a)'
is required. [I would guess that this is a common idiom.] I `solved' the
problem by introducing a class Dump q which was basically a higher-order
copy of Show.
> One possible choice would be to insist that the context of
> an instance decl constrained only proper sub-expressions of
> the type on the RHS. Alex's example would be fine then, but
> perhaps others might not?
This does not help here.
Cheers, Ralf
