On Wed, Sep 8, 2010 at 11:17 PM, wren ng thornton <w...@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 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.
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 <d...@zednenem.com> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
