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

On Dec 14, 2007 9:18 PM, Felipe Lessa wrote:

On Dec 14, 2007 6:37 PM, Benja Fallenstein 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