Re: [Haskell-cafe] lawless instances of Functor
Brent Yorgey wrote: > On Mon, Jan 04, 2010 at 11:49:33PM +0100, Steffen Schuldenzucker wrote: >> [...] > > As others have pointed out, this doesn't typecheck; but what it DOES > show is that if we had a type class > > class Endofunctor a where > efmap :: (a -> a) -> f a -> f a > > then it would be possible to write an instance for which efmap id = id > but efmap (f . g) /= efmap f . efmap g. The difference is that with > the normal Functor class, once you have applied your function f :: a > -> b to get a b, you can't do anything else with it, since you don't > know what b is. With the Endofunctor class, once you have applied f > :: a -> a, you CAN do something with the result: namely, apply f > again. Oops. Yeah, sorry, it's been ... late and stuff... Steffen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Mon, Jan 4, 2010 at 3:01 PM, Derek Elkins wrote: > So without doing funky stuff involving bottoms and/or seq, I believe > that fmap id = id implies the other functor law (in this case, not in > the case of the general categorical notion of functor.) So lets play with bottoms and/or seq. > data X a = X a > instance Functor X where > fmap f x = f `seq` case x of X a -> f a fmap id x = id `seq` case x of X a -> X (id a) = case x of X a -> X a = id x fmap (const () . undefined) x = fmap (\a -> const () (undefined a)) x = fmap (\a -> ()) x = case x of X a -> X () (fmap (const ()) . fmap undefined) x = fmap (const ()) (fmap undefined x) = const () `seq` case (fmap undefined x) of X a -> X () = case (fmap undefined x) of X a -> X ()) = case (undefined `seq` case x of X a -> X (undefined a)) of X a -> X () = case undefined of X a -> X () = undefined ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
Given fmap id = id, fmap (f . g) = fmap f . fmap g follows from the free theorem for fmap. This was published as an aside in a paper a long time back, but I forget where. -Edward Kmett On Mon, Jan 4, 2010 at 5:14 PM, Paul Brauner wrote: > Hi, > > I'm trying to get a deep feeling of Functors (and then pointed Functors, > Applicative Functors, etc.). To this end, I try to find lawless > instances of Functor that satisfy one law but not the other. > > I've found one instance that satisfies fmap (f.g) = fmap f . fmap g > but not fmap id = id: > > data Foo a = A | B > > instance Functor Foo where > fmap f A = B > fmap f B = B > > -- violates law 1 > fmap id A = B > > -- respects law 2 > fmap (f . g) A = (fmap f . fmap g) A = B > fmap (f . g) B = (fmap f . fmap g) B = B > > But I can't come up with an example that satifies law 1 and not law 2. > I'm beginning to think this isn't possible but I didn't read anything > saying so, neither do I manage to prove it. > > I'm sure someone knows :) > > Paul > ___ > 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] lawless instances of Functor
G'day all. Quoting Derek Elkins : Ignoring bottoms the free theorem for fmap can be written: If h . p = q . g then fmap h . fmap p = fmap q . fmap g Setting p = id gives h . id = h = q . g && fmap h . fmap id = fmap q . fmap g Using fmap id = id and h = q . g we get, fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g Dan Piponi points out: When I play with http://haskell.as9x.info/ft.html I get examples that look more like: If fmap' has the same signature as the usual fmap for a type and h . p = q . g then fmap h . fmap' p = fmap' q . fmap g From which it follows that if fmap' id = id then fmap' is fmap. The free theorem for: fmap' :: forall a b. (a -> b) -> F a -> F b assumes that F is already a Functor. That is, it shows that if there exists a valid fmap instance for F, then for any other function fmap' with the same signature as fmap, fmap' id = id implies fmap' = fmap. So if you want to invent a data type and fmap instance which satisfies law 1 but not law 2, then it needs to be a data type for which no valid fmap instance is possible *at all*. So it doesn't rule out the possibility completely, but it narrows down the search space considerably. Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Mon, Jan 4, 2010 at 4:15 PM, Paul Brauner wrote: > I wonder why this isn't some "classic" category theory result (maybe it is ?) It doesn't hold in category theory in general. Haskell (or at least a certain subset) is special - many things that just *look* category theoretical turn out to actually *be* category theoretical. That's quite a strong statement. So, for example, functions that have the type signature of a natural transformation are in fact natural transformations (which tells you non-trivial facts about the function). And you've found that things that are only half-defined functors are actually full-blown functors (subject to someone providing a rigorous proof of this...). This is useful. If you're using QuickCheck to convince yourself you've implemented a functor correctly, you only need to test it on id. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
Thanks. I was wondering if the free theorem of fmap entailed that implication, but I'm not used enough to decipher the output of the tool, neither am I able to generate it by hand. However, if this holds (law1 => law2), I wonder why this isn't some "classic" category theory result (maybe it is ?). I don't know much about category theory, but it seems to me that functors are pretty central to it. Maybe i'm confusing haskell's notion of Functor and category theory functors. Paul On Tue, Jan 05, 2010 at 08:01:46AM +0900, Derek Elkins wrote: > On Tue, Jan 5, 2010 at 7:14 AM, Paul Brauner wrote: > > Hi, > > > > I'm trying to get a deep feeling of Functors (and then pointed Functors, > > Applicative Functors, etc.). To this end, I try to find lawless > > instances of Functor that satisfy one law but not the other. > > > > I've found one instance that satisfies fmap (f.g) = fmap f . fmap g > > but not fmap id = id: > > > > data Foo a = A | B > > > > instance Functor Foo where > > fmap f A = B > > fmap f B = B > > > > -- violates law 1 > > fmap id A = B > > > > -- respects law 2 > > fmap (f . g) A = (fmap f . fmap g) A = B > > fmap (f . g) B = (fmap f . fmap g) B = B > > > > But I can't come up with an example that satifies law 1 and not law 2. > > I'm beginning to think this isn't possible but I didn't read anything > > saying so, neither do I manage to prove it. > > > > I'm sure someone knows :) > > Ignoring bottoms the free theorem for fmap can be written: > > If h . p = q . g then fmap h . fmap p = fmap q . fmap g > Setting p = id gives > h . id = h = q . g && fmap h . fmap id = fmap q . fmap g > Using fmap id = id and h = q . g we get, > fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g > > So without doing funky stuff involving bottoms and/or seq, I believe > that fmap id = id implies the other functor law (in this case, not in > the case of the general categorical notion of functor.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Mon, Jan 4, 2010 at 3:26 PM, Derek Elkins wrote: > Yes, I have the same problem...Basically, I'm > pretty sure the construction of that free theorem doesn't rely on any > of the actual details... For a long time I've thought such a higher order free theorem must exist, and I've mentioned it to a few people, and searched hard for a paper on it, but I haven't seen an actual statement and proof. > At this point, though, I haven't put > much effort into proving that the free theorem holds uniformly Well I encourage you to as I've a hunch the correctly generalised theorem will be quite pretty. I'd have a go but the style of proof for these sorts of things is outside of my domain of confidence/experience. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Tue, Jan 5, 2010 at 8:22 AM, Brent Yorgey wrote: > On Mon, Jan 04, 2010 at 11:49:33PM +0100, Steffen Schuldenzucker wrote: >> >> data Foo a = Foo a >> >> instance Functor Foo where >> fmap f (Foo x) = Foo . f . f $ x >> >> Then: >> >> fmap id (Foo x) == Foo . id . id $ x == Foo x >> >> fmap (f . g) (Foo x) == Foo . f . g . f . g $ x >> fmap f . fmap g $ (Foo x) == Foo . f . f . g . g $ x >> >> Now consider Foo Int and >> >> fmap ((+1) . (*3)) (Foo x) == Foo $ (x * 3 + 1) * 3 + 1 >> == Foo $ x * 9 + 4 >> fmap (+1) . fmap (*3) $ (Foo x) == Foo $ x * 3 * 3 + 1 + 1 >> == Foo $ x * 9 + 2 > > As others have pointed out, this doesn't typecheck; but what it DOES > show is that if we had a type class > > class Endofunctor a where > efmap :: (a -> a) -> f a -> f a As an aside, for clarity, this class does NOT correspond to the categorical notion of "endofunctor." I don't think any such identification was Brent's intent, I just want to avoid potential confusion. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Tue, Jan 5, 2010 at 8:15 AM, Dan Piponi wrote: > On Mon, Jan 4, 2010 at 3:01 PM, Derek Elkins wrote: > >> Ignoring bottoms the free theorem for fmap can be written: >> >> If h . p = q . g then fmap h . fmap p = fmap q . fmap g > > When I play with http://haskell.as9x.info/ft.html I get examples that > look more like: > > If fmap' has the same signature as the usual fmap for a type > > and h . p = q . g > > then fmap h . fmap' p = fmap' q . fmap g > > From which it follows that if fmap' id = id then fmap' is fmap. It should not be necessary to prove this as fmap has the appropriate type to be fmap' and therefore fmap' can simply be set to fmap. > But I don't know how to prove that uniformly for all types, just the > ones I generated free theorems for. Yes, I have the same problem. I generated a few examples using pretty much that site and generalized, but I haven't proven the general statement, though I'm pretty confident that it holds. Basically, I'm pretty sure the construction of that free theorem doesn't rely on any of the actual details of the type constructor and probably by using a higher-order notion of free theorem this could be formalized and then used to prove the above result. At this point, though, I haven't put much effort into proving that the free theorem holds uniformly (enough.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Mon, Jan 04, 2010 at 11:49:33PM +0100, Steffen Schuldenzucker wrote: > > data Foo a = Foo a > > instance Functor Foo where > fmap f (Foo x) = Foo . f . f $ x > > Then: > > fmap id (Foo x) == Foo . id . id $ x == Foo x > > fmap (f . g) (Foo x) == Foo . f . g . f . g $ x > fmap f . fmap g $ (Foo x) == Foo . f . f . g . g $ x > > Now consider Foo Int and > > fmap ((+1) . (*3)) (Foo x) == Foo $ (x * 3 + 1) * 3 + 1 > == Foo $ x * 9 + 4 > fmap (+1) . fmap (*3) $ (Foo x) == Foo $ x * 3 * 3 + 1 + 1 > == Foo $ x * 9 + 2 As others have pointed out, this doesn't typecheck; but what it DOES show is that if we had a type class class Endofunctor a where efmap :: (a -> a) -> f a -> f a then it would be possible to write an instance for which efmap id = id but efmap (f . g) /= efmap f . efmap g. The difference is that with the normal Functor class, once you have applied your function f :: a -> b to get a b, you can't do anything else with it, since you don't know what b is. With the Endofunctor class, once you have applied f :: a -> a, you CAN do something with the result: namely, apply f again. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Mon, Jan 4, 2010 at 3:01 PM, Derek Elkins wrote: > Ignoring bottoms the free theorem for fmap can be written: > > If h . p = q . g then fmap h . fmap p = fmap q . fmap g When I play with http://haskell.as9x.info/ft.html I get examples that look more like: If fmap' has the same signature as the usual fmap for a type and h . p = q . g then fmap h . fmap' p = fmap' q . fmap g >From which it follows that if fmap' id = id then fmap' is fmap. But I don't know how to prove that uniformly for all types, just the ones I generated free theorems for. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Tue, Jan 5, 2010 at 7:14 AM, Paul Brauner wrote: > Hi, > > I'm trying to get a deep feeling of Functors (and then pointed Functors, > Applicative Functors, etc.). To this end, I try to find lawless > instances of Functor that satisfy one law but not the other. > > I've found one instance that satisfies fmap (f.g) = fmap f . fmap g > but not fmap id = id: > > data Foo a = A | B > > instance Functor Foo where > fmap f A = B > fmap f B = B > > -- violates law 1 > fmap id A = B > > -- respects law 2 > fmap (f . g) A = (fmap f . fmap g) A = B > fmap (f . g) B = (fmap f . fmap g) B = B > > But I can't come up with an example that satifies law 1 and not law 2. > I'm beginning to think this isn't possible but I didn't read anything > saying so, neither do I manage to prove it. > > I'm sure someone knows :) Ignoring bottoms the free theorem for fmap can be written: If h . p = q . g then fmap h . fmap p = fmap q . fmap g Setting p = id gives h . id = h = q . g && fmap h . fmap id = fmap q . fmap g Using fmap id = id and h = q . g we get, fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g So without doing funky stuff involving bottoms and/or seq, I believe that fmap id = id implies the other functor law (in this case, not in the case of the general categorical notion of functor.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
Steffen Schuldenzucker wrote: > data Foo a = Foo a > > instance Functor Foo where > fmap f (Foo x) = Foo . f . f $ x I think this doesn't typecheck. Cheers, Jochem -- Jochem Berndsen | joc...@functor.nl | joc...@牛在田里.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
On Tue, Jan 5, 2010 at 7:49 AM, Steffen Schuldenzucker wrote: > Hi Paul, > > Paul Brauner wrote: >> Hi, >> >> I'm trying to get a deep feeling of Functors (and then pointed Functors, >> Applicative Functors, etc.). To this end, I try to find lawless >> instances of Functor that satisfy one law but not the other. >> >> I've found one instance that satisfies fmap (f.g) = fmap f . fmap g >> but not fmap id = id: >> [...] >> But I can't come up with an example that satifies law 1 and not law 2. >> I'm beginning to think this isn't possible but I didn't read anything >> saying so, neither do I manage to prove it. >> >> I'm sure someone knows :) > > data Foo a = Foo a > > instance Functor Foo where > fmap f (Foo x) = Foo . f . f $ x And what is the type of f here? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
Hi Paul, Paul Brauner wrote: > Hi, > > I'm trying to get a deep feeling of Functors (and then pointed Functors, > Applicative Functors, etc.). To this end, I try to find lawless > instances of Functor that satisfy one law but not the other. > > I've found one instance that satisfies fmap (f.g) = fmap f . fmap g > but not fmap id = id: > [...] > But I can't come up with an example that satifies law 1 and not law 2. > I'm beginning to think this isn't possible but I didn't read anything > saying so, neither do I manage to prove it. > > I'm sure someone knows :) data Foo a = Foo a instance Functor Foo where fmap f (Foo x) = Foo . f . f $ x Then: fmap id (Foo x) == Foo . id . id $ x == Foo x fmap (f . g) (Foo x) == Foo . f . g . f . g $ x fmap f . fmap g $ (Foo x) == Foo . f . f . g . g $ x Now consider Foo Int and fmap ((+1) . (*3)) (Foo x) == Foo $ (x * 3 + 1) * 3 + 1 == Foo $ x * 9 + 4 fmap (+1) . fmap (*3) $ (Foo x) == Foo $ x * 3 * 3 + 1 + 1 == Foo $ x * 9 + 2 -- Steffen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lawless instances of Functor
Hi, I'm trying to get a deep feeling of Functors (and then pointed Functors, Applicative Functors, etc.). To this end, I try to find lawless instances of Functor that satisfy one law but not the other. I've found one instance that satisfies fmap (f.g) = fmap f . fmap g but not fmap id = id: data Foo a = A | B instance Functor Foo where fmap f A = B fmap f B = B -- violates law 1 fmap id A = B -- respects law 2 fmap (f . g) A = (fmap f . fmap g) A = B fmap (f . g) B = (fmap f . fmap g) B = B But I can't come up with an example that satifies law 1 and not law 2. I'm beginning to think this isn't possible but I didn't read anything saying so, neither do I manage to prove it. I'm sure someone knows :) Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
