Re: [Haskell-cafe] Questions about the Functor class and it's use in "Data types à la carte"
lrpalmer at gmail.com
Fri Dec 14 16:46:48 EST 2007
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,
> 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,
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