[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 <voigt@tcs.inf.tu-dresden.de>:
- 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