[Haskell-cafe] Restricted type classes

[wren ng thornton]

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 
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