[Haskell-cafe] Restricted type classes

[David Menendez]

On Wed, Sep 8, 2010 at 11:17 PM, wren ng thornton <wren at freegeek.org> wrote:
> 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
<snip>
>    -- | 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.

Fascinating. I figured there might be a counter-example involving seq,
but this is pretty subtle.

In particular, would it be fair to say that in Haskell-without-seq, "E
(f a) a" and "E (f a) (f a)" are indistinguishable?

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

...at which point, it no longer has the same type as pure. But your
point is taken.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>