[Haskell-cafe] Natural Transformations and fmap

[Janis Voigtländer]

Ryan Ingram wrote:
> However, the type of natural transformations comes with a free theorem, for
> example
>
>     concat :: [[a]] ->  [a]
>
> has the free theorem
>
>     forall f :: a ->  b, f strict and total, fmap f . concat = concat . fmap
> (fmap f)
>
> The strictness condition is needed; consider
>
>     broken_concat :: [[a]] ->  [a]
>     broken_concat _ = [undefined]
>     f = const ()
>
>     fmap f (broken_concat []) = fmap f [undefined] = [()]
>     broken_concat (fmap (fmap f) []) = broken_concat [] = [undefined]
>
> The 'taming selective strictness' version of the free theorem generator[1]
> allows removing the totality condition on f, but not the strictness
> condition.
>
> But in the case of concat, you can prove a stronger theorem:
>
>     forall f :: a ->  b, fmap f . concat = concat . fmap (fmap f)
>
> My suspicion is that this stronger theorem holds for all strict and total
> natural transformations, but I don't know how to go about proving that
> suspicion.  I'm a hobbyist mathematician and a professional programmer, not
> the other way around:)
>
> ...
>
> [1]http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi

There is an analogous approach to the "taming selective strictness"
version of the free theorem generator where it is general recursion that
is tamed. In that setting, you then get free theorems like that for
concat without either strictness or totality side conditions. It is
really very similar, indeed the "taming selective strictness" work takes
over and develops further the much earlier "taming general recursion"
ideas. The original source for the latter is:

http://dblp.uni-trier.de/rec/bibtex/conf/esop/LaunchburyP96

Just nobody ever bothered to implement it in a tool. (Well, actually,
such an implementation is essentially hidden inside the counterexample
generator http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi)

Best,
Janis.

-- 
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:jv at iai.uni-bonn.de