Jonathan Cast wrote: > On 16 Dec 2007, at 3:21 AM, Dominic Steinitz wrote: > >>>> Do you have a counter-example of (.) not being function composition in >>>> the categorical sense? >>> >>> Let bot be the function defined by >>> >>> bot :: alpha -> beta >>> bot = bot >>> >>> By definition, >>> >>> (.) = \ f -> \ g -> \ x -> f (g x) >>> >>> Then >>> >>> bot . id >>> = ((\ f -> \ g -> \ x -> f (g x)) bot) id >>> = (\ g -> \ x -> bot (g x)) id >>> = \ x -> bot (g x) >> >> I didn't follow the reduction here. Shouldn't id replace g everywhere? > > Yes, sorry. > >> This would give >> >> = \x -> bot x >> >> and by eta reduction > > This is the point --- by the existence of seq, eta reduction is unsound > in Haskell. >
Am I correct in assuming that if my program doesn't contain seq then I can reason using eta reduction? >> >> Why is seq introduced? > > Waiting for computers to get fast enough to run Haskell got old. > I'm guessing you were not being entirely serious here but I think that's a good answer. > Oh, you mean here? Equality (=) for pickier Haskellers always means > Leibnitz' equality: > > Given x, y :: alpha > > x = y if and only if for all functions f :: alpha -> (), f x = f y > > f ranges over all functions definable in Haskell, (for some version of > the standard), and since Haskell 98 defined seq, the domain of f > includes (`seq` ()). So since bot and (\ x -> bot x) give different > results when handed to (`seq` ()), they must be different. > > The `equational reasoning' taught in functional programming courses is > unsound, for this reason. It manages to work as long as everything > terminates, but if you want to get picky you can find flaws in it (and > you need to get picky to justify extensions to things like infinite lists). > Reasoning as though you were in a category with a bottom should be ok as long as seq isn't present? I'm recalling a paper by Freyd on CPO categories which I can't lay my hands on at the moment or find via a search engine. I suspect Haskell (without seq) is pretty close to a CPO category. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
