[Haskell-cafe] Re: Quantification in free theorems

[Janis Voigtlaender]

Hello all,

[EMAIL PROTECTED] 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:[EMAIL PROTECTED]

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: Quantification in free theorems

[ajb]

G'day all.

Quoting Janis Voigtlaender [EMAIL PROTECTED]:

 Maybe it is just an accidental swapping of the arguments to (.) in your
 implementation.

That was it, yes.  Thanks for debugging my code for me. :-)

(For those keeping score, it was actually the incorrect unzipping of
a zipper data structure.  If only I could scrap my boilerplate...)

 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.

In my case, the approach taken was to pass a Bool around the pretty
printer which says whether or not to include quantifiers.  (It's okay
to strip quantifiers off the right-hand side of an implication if it's
okay to strip quantifiers off the implication itself.)

 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.

That's correct.  Once again, different design criteria apply.  IRC has
anti-flooding rules which encourage brevity rather than full-featuredness.

Cheers,
Andrew Bromage
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe