Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"

[Luke Palmer]

On Dec 14, 2007 9:18 PM, Felipe Lessa <felipe.lessa at gmail.com> wrote:
> On Dec 14, 2007 6:37 PM, Benja Fallenstein <benja.fallenstein at gmail.com> wrote:
> > such that the following two properties hold:
> >
> >     * F(idX) = idF(X) for every object X in C
> >     * F(g . f) = F(g) . F(f) for all morphisms f:X -> Y and g:Y -> Z."
>
> Should we write
>
> instance Functor Val where
>   fmap = undefined
>
> Would those properties be satisfied? Of course,
>
> fmap (g . f) == _|_ == fmap g . fmap f,
>
> but
>
> fmap id x == _|_ =/= x == id x.

Right, so here is a proof that this instance is not sound.


> As my understanding of the relationship between bottoms and
> non-bottoms isn't that great,

My understanding is that the difference between bottom and non-bottom, other
than their just being two different values, is that bottom is used in the
definition of "definedness" in the denotational semantics; eg. for all functions
f:

    f _|_ = a implies f x = a for all x

Concretely, you are not allowed to pattern match against bottom, that's all.

This is a great article for understanding bottom:
http://en.wikibooks.org/wiki/Haskell/Denotational_semantics

> could anyone tell me if the above
> instance is sound (i.e. satisfy the expected properties)? If it is
> not, the implementation "fmap f = id" is really the only one sound,
> right?

I think so, given that we cannot use dynamic typing on arbitrary values
and don't have dependent types. If we could/did, the following pseudocode
would also be valid:

    fmap (f :: Int -> Int) (Val x) = Val (f x)
    fmap (f :: otherwise)  (Val x) = Val x

I'd love to see a proof that fmap f = id is the only sound implementation
in Haskell, but I don't really know what proofs like that look like so
I'm having trouble constructing one.

Luke