[Haskell-cafe] Restricted type classes
dave at zednenem.com
Thu Sep 9 01:04:59 EDT 2010
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
> -- | 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>
More information about the Haskell-Cafe