[Haskell-cafe] Natural Transformations and fmap

Janis Voigtländer jv at informatik.uni-bonn.de
Sat Jan 28 13:55:52 CET 2012

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:


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)


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

More information about the Haskell-Cafe mailing list