Ryan Ingram wrote:
However, the type of natural transformations comes with a free theorem, for exampleconcat :: [[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:[email protected] _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
