Re: lines/unlines and "inverse"

Lars Henrik Mathiesen wrote: | lines . unlines = id | unlines . lines . unlines == unlines | words . unwords . words = words Don't be fooled by the information content of the second equation -- the first equation directly implies it: unlines . lines . unlines == {assoc (.)} unlines . (lines . unlines) == {equation 1} unlines . id == {id is unit of (.)} unlines I.e. in general, when f is g's left inverse: f . g == id Then the following equation holds automatically: g . f . g == g Regards, /Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen Chalmers University, Gothenburg, Sweden.