Hello all, ajb@spamcop.net wrote:
For this, you produce the following theorem:
g x = h (f x) => $map f . filter g = filter h . $map f
It now produces:
filter (f . g) . $map f = $map f . filter g
... which is also wrong. Consider the following: f = const False g = id Then, with the standard filter function: filter (f . g) (map f [True]) = [] /= [False] = map f (filter g [True]) Maybe it is just an accidental swapping of the arguments to (.) in your implementation. For if one would swap all such arguments above, one would get: $map f . filter (g . f) = filter g . $map f which would be correct. Regarding Lennart's suggestion: I am pretty sure that it would be easy to adapt Sascha's system to omit top level quantifiers. All that should be needed would be an extra pass prior to prettyprinting, to strip off any outermost quantifiers from the data type representing free theorems. That wouldn't really be a mix of the two systems, however, because they follow different strategies for output. This can be seen, for example, for the following type: zip :: [a] -> [b] -> [(a, b)] Here, Andrew's system now produces: (forall x y. ( f ($fst x) = $fst y && g ($snd x) = $snd y ) => h x = y) => $map h (zip xs ys) = zip ($map f xs) ($map g ys) Whereas Sascha's system produces (minus top level quantifiers): (zip x1 x2, zip (map h1 x1) (map h2 x2)) in lift_{[]}(lift_{(2)}(h1, h2)) lift_{[]}(lift_{(2)}(h1, h2)) = {([], [])} u {(x : xs, y : ys) | ((x, y) in lift_{(2)}(h1, h2)) /\ ((xs, ys) in lift_{[]}(lift_{(2)}(h1, h2)))} lift_{(2)}(h1, h2) = {((x1, x2), (y1, y2)) | (h1 x1 = y1) /\ (h2 x2 = y2)} The latter approach has advantages when it comes to producing free theorems that are faithful to the presence of _|_ and general recursion in Haskell, which is not supported by Andrew's system, as far as I can see. Also, some of Andrew's tricks for making the output look more pointfree would not work when producing the more general "relational" free theorem (prior to the specialization to functions), which is also supported in Sascha's system. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de