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
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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
And what is the type of f here?
I think this doesn't typecheck.
Cheers, Jochem
--
Jochem Berndsen | joc...@functor.nl | jochem@牛在田里.com
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.)
> 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
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
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.)
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.
> 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
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
> 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
Hmm. Not quite a proff as we want to use: For all f g fmap (f . g) =
fmap f . fmap g. So we need to operate on arbitrary f and g. Also in
first line conclusion is used - at this stage we don't know if h . p =
p . q -> fmap h . fmap p = fmap q . fmap g.
Especially that (A->B) functions is |A|^|B| (and in haskell |A| >= 1, |
B| >= 1). Now imagine that (in pseudocode[1]):
rho :: (A -> B) -> A -> B
rho f | f is A -> A = id
| f is Integral -> Integral = (+1) . fromIntegral
| otherise = f
then
instance Functor Foo where
fmap f (Something a) = Something $ rho f a
then
fmap id = id
but
if f = (+1) . fromIntegral :: Integer -> Int
g = (-1) . fromIntegral :: Int -> Integer
then
fmap (f . g) = fmap id
but
fmap f . fmap g = fmap (+2)
Regards
[1] It can nearly be written in Haskell+Rules but rules does not have
precedence.
Quoting Derek Elkins <derek.a...@gmail.com>:
> 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
No, the first line is the "free theorem" -- i.e. the parametericity
theorem -- for the type. It holds for any Haskell value with this
type, coming essentially from the fact that downcasts are not possible
in Haskell. You can play with free theorems here:
http://linux.tcs.inf.tu-dresden.de/~voigt/ft/. See Wadler's paper
"Theorem's for free!" for more about them.
> Especially that (A->B) functions is |A|^|B| (and in haskell |A| >= 1, |
> B| >= 1). Now imagine that (in pseudocode[1]):
> rho :: (A -> B) -> A -> B
> rho f | f is A -> A = id
> � � �| f is Integral -> Integral = (+1) . fromIntegral
> � � �| otherise = f
Haskell's inability to write this function is exactly where free
theorems come from.
Luke
This was published as an aside in a paper a long time back, but I forget
where.
-Edward Kmett
This looks relevant:
Janis Voigtländer.
Free Theorems Involving Type Constructor Classes.
http://wwwtcs.inf.tu-dresden.de/~voigt/icfp09.pdf
Regards,
Heinrich Apfelmus
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
Oops. Yeah, sorry, it's been ... late and stuff...
Steffen