Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Dominic Steinitz wrote: Roberto Zunino wrote: This is the point: eta does not hold if seq exists. undefined `seq` 1 == undefined (\x - undefined x) `seq` 1 == 1 Ok I've never used seq and I've never used unsavePerformIO. Provided my program doesn't contain these then can I assume that eta reduction holds and that (.) is categorical composition? Yes, provided that you do not use seq and all its related stuff, e.g. ($!), foldl', bang patterns, data Foo a = Foo !a, ... Also, note that you still can define and use seq restricted to many useful types: seqInt :: Int - a - a seqInt 0 x = x seqInt _ x = x IIRC, you can also have a quite general seqData :: Data a = a - b - b The (.) does not form a category argument should be something like: id . undefined == (\x - id (undefined x)) /= undefined where the last inequation is due to the presence of seq. That is, without seq, there is no way to distinguish between undefined and (const undefined), so you could use a semantic domain where they coincide. In that case, eta does hold. It would be a pretty odd semantic domain where 1 == undefined. Or perhaps, I should say not a very useful one. in the new domain, you do not have 1 == undefined (which are still different) but merely undefined == (\x - undefined) Regards, Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Excellent! This has all been very helpful. Thanks a lot everybody! :-) -Corey On 12/14/07, Benja Fallenstein [EMAIL PROTECTED] wrote: Hi Corey, On Dec 14, 2007 8:44 PM, Corey O'Connor [EMAIL PROTECTED] wrote: The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor? Recall the definition of functor. From Wikipedia: A functor F from C to D is a mapping that * associates to each object X in C an object F(X) in D, * associates to each morphism f:X - Y in C a morphism F(f):F(X) - F(Y) in D such that the following two properties hold: * F(idX) = idF(X) for every object X in C * F(g . f) = F(g) . F(f) for all morphisms f:X - Y and g:Y - Z. http://en.wikipedia.org/wiki/Functor We consider C = D = the category of types. Note that any type constructor is a mapping from types to types -- thus it associates to each object (type) X an object (type) F(X). Declaring a type constructor to be an instance of Functor means that you have to provide 'fmap :: (a - b) - (f a - f b) -- that is, a mapping that associates to each morphism (function) fn :: a - b a morphism fmap fn :: f a - f b. Making sure that the two laws are fulfilled is the responsibility of the programmer writing the instance of Functor. (I.e., you're not supposed to do this: instance Functor Val where fmap f (Val x) = Val (x+1).) Hope this helps with seeing the correspondence? :-) - Benja -- -Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
keep in mind that Haskell composition (.) is not really composition in the category-theoretic sense, because it adds extra laziness. Use this Do you have a counter-example of (.) not being function composition in the categorical sense? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
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? This would give = \x - bot x and by eta reduction = bot which /= bot since (seq bot () = bot) but (seq (\ x - M) () = ()) regardless of what expression we substitute for M. Why is seq introduced? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Yitzchak Gale wrote: When using seq and _|_ in the context of categories, keep in mind that Haskell composition (.) is not really composition in the category-theoretic sense, because it adds extra laziness. Use this instead: (.!) f g x = f `seq` g `seq` f (g x) id .! undefined == \x - undefined /= undefined Probably you meant (.!) f g = f `seq` g `seq` (f . g) Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Dominic Steinitz wrote: This would give = \x - bot x and by eta reduction This is the point: eta does not hold if seq exists. undefined `seq` 1 == undefined (\x - undefined x) `seq` 1 == 1 The (.) does not form a category argument should be something like: id . undefined == (\x - id (undefined x)) /= undefined where the last inequation is due to the presence of seq. That is, without seq, there is no way to distinguish between undefined and (const undefined), so you could use a semantic domain where they coincide. In that case, eta does hold. Regards, Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
I wrote: (.!) f g x = f `seq` g `seq` f (g x) Roberto Zunino wrote: id .! undefined == \x - undefined /= undefined Probably you meant (.!) f g = f `seq` g `seq` (f . g) Yes, thank you. -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Roberto Zunino writes: without seq, there is no way to distinguish between undefined and (const undefined), no way to distinguish is perhaps too strong. They have slightly different types. Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Roberto Zunino wrote: Dominic Steinitz wrote: This would give = \x - bot x and by eta reduction This is the point: eta does not hold if seq exists. undefined `seq` 1 == undefined (\x - undefined x) `seq` 1 == 1 Ok I've never used seq and I've never used unsavePerformIO. Provided my program doesn't contain these then can I assume that eta reduction holds and that (.) is categorical composition? The (.) does not form a category argument should be something like: id . undefined == (\x - id (undefined x)) /= undefined where the last inequation is due to the presence of seq. That is, without seq, there is no way to distinguish between undefined and (const undefined), so you could use a semantic domain where they coincide. In that case, eta does hold. It would be a pretty odd semantic domain where 1 == undefined. Or perhaps, I should say not a very useful one. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Ah, good old seq. How I loathe it. Seriously, though, good catch. I always forget about seq when I'm doing stuff like this. When using seq and _|_ in the context of categories, keep in mind that Haskell composition (.) is not really composition in the category-theoretic sense, because it adds extra laziness. Use this instead: (.!) f g x = f `seq` g `seq` f (g x) -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
I'm working through the interesting paper Data type à la carte and am confused by the Functor instance for Val. I think this stems from some confusion of mine regarding the Functor class in general. The Functor instance I'm confused about is: instance Functor Val where fmap f (Val x ) = Val x where Val is defined as: data Val e = Val Int Is this the only valid Functor instance for the Val type? Even though I'd, naively, expect the Functor instance to look like: instance Functor Val where fmap f (Val x) = Val (f x) I suspect that would not work out due to the type of the Val constructor. Is this correct? The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor? Any help would be, of course, greatly appreciated. -Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 14, 2007 11:44 AM, Corey O'Connor [EMAIL PROTECTED] wrote: I'm working through the interesting paper Data type à la carte and am confused by the Functor instance for Val. I think this stems from some confusion of mine regarding the Functor class in general. I'll try to explain, but I might not be very clear :). The Functor instance I'm confused about is: instance Functor Val where fmap f (Val x ) = Val x where Val is defined as: data Val e = Val Int Is this the only valid Functor instance for the Val type? Even though I'd, naively, expect the Functor instance to look like: instance Functor Val where fmap f (Val x) = Val (f x) Yes, I think people often expect this, because they're used to the idea that fmap applies a function to all the terminal elements in a data structure. For example, if you map a function across a list or tree, you expect the function to be applied to each value or node, not the branches themselves, and to preserve the structure of the tree or list. This is not the case when you use functors as you are in your email (I think sometimes called syntactic functors, for traversing abstract syntax trees); In this case, you are only pushing the function into all recursive subterms of a data structure, which the function then operates on. So, consider this data structure: data Val e = Add e e | Val Int instance Functor Val where fmap f (Val x) = Val x fmap f (Add x y) = Add (f x) (f y) Notice that it is not (fmap f x) and (fmap f y). You only push the function one level deeper, not all the way down (the catamorphism takes care of fmap-ing the function all the way down). I suspect that would not work out due to the type of the Val constructor. Is this correct? Correct, the types wouldn't work. Try it and see :) The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor? I could try to answer this one, but I would just confuse both of us, heh. Hope I was helpful! Any help would be, of course, greatly appreciated. -Corey O'Connor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Hi Corey, On Dec 14, 2007 8:44 PM, Corey O'Connor [EMAIL PROTECTED] wrote: The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor? Recall the definition of functor. From Wikipedia: A functor F from C to D is a mapping that * associates to each object X in C an object F(X) in D, * associates to each morphism f:X - Y in C a morphism F(f):F(X) - F(Y) in D such that the following two properties hold: * F(idX) = idF(X) for every object X in C * F(g . f) = F(g) . F(f) for all morphisms f:X - Y and g:Y - Z. http://en.wikipedia.org/wiki/Functor We consider C = D = the category of types. Note that any type constructor is a mapping from types to types -- thus it associates to each object (type) X an object (type) F(X). Declaring a type constructor to be an instance of Functor means that you have to provide 'fmap :: (a - b) - (f a - f b) -- that is, a mapping that associates to each morphism (function) fn :: a - b a morphism fmap fn :: f a - f b. Making sure that the two laws are fulfilled is the responsibility of the programmer writing the instance of Functor. (I.e., you're not supposed to do this: instance Functor Val where fmap f (Val x) = Val (x+1).) Hope this helps with seeing the correspondence? :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 14, 2007 6:37 PM, Benja Fallenstein [EMAIL PROTECTED] wrote: such that the following two properties hold: * F(idX) = idF(X) for every object X in C * F(g . f) = F(g) . F(f) for all morphisms f:X - Y and g:Y - Z. Should we write instance Functor Val where fmap = undefined Would those properties be satisfied? Of course, fmap (g . f) == _|_ == fmap g . fmap f, but fmap id x == _|_ =/= x == id x. As my understanding of the relationship between bottoms and non-bottoms isn't that great, could anyone tell me if the above instance is sound (i.e. satisfy the expected properties)? If it is not, the implementation fmap f = id is really the only one sound, right? Thanks! -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 15, 2007 12:00 AM, David Menendez [EMAIL PROTECTED] wrote: These can (and, if Val is a newtype, will) be compiled to the same code, but they don't have the same type. In particular, there is no way to unify a - a with f a - f b for any f. Thanks for noticing that! I hadn't seen before that the two Val constructors in fmap f (Val x) = Val x were of different types. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On 12/14/07, David Menendez [EMAIL PROTECTED] wrote: And yes, I'm pretty sure that's the only possible implementation for that type which satisfies the functor laws. Lets just prove it, then; I'm pretty sure it comes pretty easily from the free theorem for the type of fmap. data Val a = Val Int fmap :: (a - b) - (Val a - Val b) which must satisfy the law fmap id1 = id2 with id1 :: forall a. a - a id2 :: forall a. Val a - Val a Now, first note that since we cannot make any choices based on the type of f, there's no way for f to be relevant to the result of fmap; we have no way to get something of type a besides _|_ to pass to f, and no use for things of type b. Therefore, since the choice of f can't affect the implementation of fmap, we are given the only possible implementation directly from the Functor law: fmap _ ~= id or, to avoid the type error mentioned previously, fmap _ (Val x) = (Val x) -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 15, 2007 3:44 AM, Benja Fallenstein [EMAIL PROTECTED] wrote: Hmmm. Something about that ticks off my don't play fast and loose with bottom detector. I should add that I do think you're correct if you ignore the existence of bottom, and I'm pretty sure that you're correct if you allow bottom but consider seq to be only slightly better than unsafePerformIO. But I couldn't turn your proof sketch into something that would completely convince me, myself :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 14, 2007 9:44 PM, Benja Fallenstein [EMAIL PROTECTED] wrote: data Val a = Val Int instance Functor Val where fmap f (Val x) = f `seq` Val x Ah, good old seq. How I loathe it. Seriously, though, good catch. I always forget about seq when I'm doing stuff like this. -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
