wren ng thornton wren at freegeek.org
Wed Sep 8 23:17:43 EDT 2010

```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 fmap at E maintains identities
fmap id _|_
== _|_
== id _|_

fmap id (E a b)
== E (id a) b
== E a b
== id (E a b)

-- | Proof that fmap at 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 pure at 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
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