[Haskell-cafe] Restricted type classes
David Menendez
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
<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/>
More information about the Haskell-Cafe
mailing list