On 9/7/10 4:21 AM, Daniel Fischer wrote:
On Tuesday 07 September 2010 05:22:55, David Menendez wrote:
In fact, I think *every* appropriately-typed function satisfies that
law. Does anyone know of a counter-example?
-- | Multiply the *Hask* category by its number of objects.
data E a where
E :: a -> b -> E a
-- | Maintain all the morphisms of *Hask* in each *E*-copy of
-- it, but keep the tag for which *E*-copy we were in.
instance Functor E where
fmap f (E a b) = E (f a) b
-- | Proof that f...@e maintains identities
fmap id _|_
== _|_
== id _|_
fmap id (E a b)
== E (id a) b
== E a b
== id (E a b)
-- | Proof that f...@e maintains compositions
fmap f (fmap g _|_)
== fmap f _|_
== _|_
== fmap (f . g) _|_
fmap f (fmap g (E a b))
== fmap f (E (g a) b)
== E (f (g a)) b
== E ((f.g) a) b
== fmap (f . g) (E a b)
-- | The object part of a functor to enter *E* along the diagonal.
impure :: a -> E a
impure a = E a a
-- | Proof that impure is not p...@e
fmap f (impure a)
== fmap f (E a a)
== E (f a) a
/= E (f a) (f a)
== impure (f a)
And yet, impure has the correct type.
Of course, it is possible to define functions of type (a -> E a) which
do satisfy the law. Namely, choose any function where the second
argument to E does not depend on the parameter. But the problem is that
there are a whole bunch of them! And none of them is intrinsically any
more natural or correct than any other. Unfortunately, impure is the
most natural function in that type, but it breaks the laws.
Functors like this happen to be helpful too, not just as oddities.
They're functors for tracking the evolution of a value through a
computation (e.g., tracking the initial value passed to a function). In
this example, the existential tag is restricted by observational
equivalence to only allow us to distinguish bottom from non-bottom
initial values. But we can add context constraints on the data
constructor in order to extract more information; at the cost of
restricting impure to only working for types in those classes.
class Functor f => Pointed f where
point :: a -> f a
-- satisfying fmap f . point = point . f
notQuitePure :: Pointed f => a -> f a
notQuitePure _ = point undefined
fmap (const True) . notQuitePure = point . const True
But I don't see how to violate that law without introducing undefined on
the RHS.
You can also break the law by defining a strictness functor[*]: pure=id;
fmap=($!) ---or any newtype equivalent. It breaks the pointed law for
the same kind of reason, namely by strictifying functions that ignore
their parameters but doing so in different places.
[*] Unfortunately, that's not actually a functor, since it does not
preserve bottom-eating compositions. I.e.,
($!)(const 42 . const undefined)
/= ($!)(const 42) . ($!)(const undefined)
We only get a monotonic relationship, not an equality. I tried playing
around with it a bit, but I'm pretty sure there's no way to define any
(non-trivial, full,... i.e., interesting) functor from *Hask* into
*StrictHask* from within Haskell. The only functor that seems to work is
the CBV functor which reinterprets Haskell terms via call-by-value
semantics, which I don't think we can define from within Haskell. Of
course, defining an embedding from *StrictHask* to *Hask* is trivial.
These two points together seem like a compelling argument for
laziness-by-default in language design.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
