On Wed, Sep 8, 2010 at 11:17 PM, 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 <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@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