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

Luke Palmer lrpalmer at
Fri Dec 14 16:46:48 EST 2007

On Dec 14, 2007 9:18 PM, Felipe Lessa <felipe.lessa at> wrote:
> On Dec 14, 2007 6:37 PM, Benja Fallenstein <benja.fallenstein at> 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 _|_ = 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:

> 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.


More information about the Haskell-Cafe mailing list