[Haskell-cafe] Re: Quantification in free theorems

[ajb at spamcop.net]

G'day all.

Quoting Janis Voigtlaender <voigt at tcs.inf.tu-dresden.de>:

> 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