[Ccing to haskell-cafe; please direct any replies there instead of haskell]
G'day all.
First of all, once again well done to Sascha on a great tool.
Just a few comments.
Quoting Janis Voigtlaender <[EMAIL PROTECTED]>:
- support for type classes
(e.g., enter "elem" and note the generated respects-restrictions)
This is a great feature, and it'll be even better when constructor
classes are done.
Some of these respects-restrictions arent as useful as they might be,
because they don't take into account easily-predictable invariants.
For example, the type:
(Eq a) => [a] -> [a]
generates the following restriction:
g respects Eq if
forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y)
forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y)
Thats correct, but redundant, because (x == y) = (g x == g y) if and only
if (x /= y) = (g x /= g y). Crucially, you can work this out from the
definition of Eq, because (/=) has a default implementation defined in
terms of (==) alone.
The type (Monoid a) => [a] -> a gives:
forall t1,t2 in TYPES(Monoid), g :: t1 -> t2, g
respects Monoid.
forall x :: [t1]. g (f x) = f (map g x)
The class restriction occurring therein is defined as follows:
g respects Monoid if
g mempty = mempty
forall x :: t1.
forall y :: t1. g (mappend x y) = mappend (g x) (g y)
forall (x, y) in lift{[]}(g). g (mconcat x) = mconcat y
Again, mconcat is redundant. Even more curiously, though, map
appears in the theorem, but lift{[]} appears in the class restriction.
Cheers,
Andrew Bromage
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
