[Haskell-cafe] Re: Quantification in free theorems

[Janis Voigtlaender]

Hello all,

ajb at 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 at tcs.inf.tu-dresden.de