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

On Dec 15, 2007 12:00 AM, David Menendez wrote:

These can (and, if Val is a newtype, will) be compiled to the same code, but they don't have the same type. In particular, there is no way to unify "a -> a" with "f a -> f b" for any f.

Thanks for noticing that! I hadn't seen before that the two Val constructors in fmap f (Val x) = Val x were of different types. Cheers, -- Felipe.

On Dec 15, 2007 3:15 AM, Ryan Ingram wrote:

On 12/14/07, David Menendez wrote:

...

And yes, I'm pretty sure that's the only possible implementation for that type which satisfies the functor laws.

Lets just prove it, then; I'm pretty sure it comes pretty easily from the free theorem for the type of fmap.

...

Now, first note that since we cannot make any choices based on the type of f, there's no way for f to be relevant to the result of fmap; we have no way to get something of type "a" besides _|_ to pass to f, and no use for things of type "b".

Hmmm. Something about that ticks off my "don't play fast and loose with bottom" detector. data Val a = Val Int instance Functor Val where fmap f (Val x) = f `seq` Val x :-) - Benja

On Dec 14, 2007 9:44 PM, Benja Fallenstein wrote:

data Val a = Val Int

instance Functor Val where fmap f (Val x) = f `seq` Val x

Ah, good old seq. How I loathe it. Seriously, though, good catch. I always forget about seq when I'm doing stuff like this. -- Dave Menendez http://www.eyrie.org/~zednenem/

Yitzchak Gale wrote:

When using seq and _|_ in the context of categories, keep in mind that Haskell "composition" (.) is not really composition in the category-theoretic sense, because it adds extra laziness. Use this instead:

(.!) f g x = f `seq` g `seq` f (g x)

id .! undefined == \x -> undefined /= undefined Probably you meant (.!) f g = f `seq` g `seq` (f . g) Zun.

keep in mind that Haskell "composition" (.) is not really composition in the category-theoretic sense, because it adds extra laziness. Use this

Do you have a counter-example of (.) not being function composition in the categorical sense?

...

Do you have a counter-example of (.) not being function composition in the categorical sense?

Let bot be the function defined by

bot :: alpha -> beta bot = bot

By definition,

(.) = \ f -> \ g -> \ x -> f (g x)

Then

bot . id = ((\ f -> \ g -> \ x -> f (g x)) bot) id = (\ g -> \ x -> bot (g x)) id = \ x -> bot (g x)

I didn't follow the reduction here. Shouldn't id replace g everywhere? This would give = \x -> bot x and by eta reduction = bot

which /= bot since (seq bot () = bot) but (seq (\ x -> M) () = ()) regardless of what expression we substitute for M.

Why is seq introduced?

Jonathan Cast wrote:

On 16 Dec 2007, at 3:21 AM, Dominic Steinitz wrote:

...

...

...

Do you have a counter-example of (.) not being function composition in the categorical sense?

Let bot be the function defined by

bot :: alpha -> beta bot = bot

By definition,

(.) = \ f -> \ g -> \ x -> f (g x)

Then

bot . id = ((\ f -> \ g -> \ x -> f (g x)) bot) id = (\ g -> \ x -> bot (g x)) id = \ x -> bot (g x)

I didn't follow the reduction here. Shouldn't id replace g everywhere?

Yes, sorry.

...

This would give

= \x -> bot x

and by eta reduction

This is the point --- by the existence of seq, eta reduction is unsound in Haskell.

Am I correct in assuming that if my program doesn't contain seq then I can reason using eta reduction?

...

Why is seq introduced?

Waiting for computers to get fast enough to run Haskell got old.

I'm guessing you were not being entirely serious here but I think that's a good answer.

Oh, you mean here? Equality (=) for pickier Haskellers always means Leibnitz' equality:

Given x, y :: alpha

x = y if and only if for all functions f :: alpha -> (), f x = f y

f ranges over all functions definable in Haskell, (for some version of the standard), and since Haskell 98 defined seq, the domain of f includes (`seq` ()). So since bot and (\ x -> bot x) give different results when handed to (`seq` ()), they must be different.

The `equational reasoning' taught in functional programming courses is unsound, for this reason. It manages to work as long as everything terminates, but if you want to get picky you can find flaws in it (and you need to get picky to justify extensions to things like infinite lists).

Reasoning as though you were in a category with a bottom should be ok as long as seq isn't present? I'm recalling a paper by Freyd on CPO categories which I can't lay my hands on at the moment or find via a search engine. I suspect Haskell (without seq) is pretty close to a CPO category.

On 16 Dec 2007, at 9:47 AM, Dominic Steinitz wrote:

Jonathan Cast wrote:

...

On 16 Dec 2007, at 3:21 AM, Dominic Steinitz wrote:

...

...

...

Do you have a counter-example of (.) not being function composition in the categorical sense?

Let bot be the function defined by

bot :: alpha -> beta bot = bot

By definition,

(.) = \ f -> \ g -> \ x -> f (g x)

Then

bot . id = ((\ f -> \ g -> \ x -> f (g x)) bot) id = (\ g -> \ x -> bot (g x)) id = \ x -> bot (g x)

I didn't follow the reduction here. Shouldn't id replace g everywhere?

Yes, sorry.

...

This would give

= \x -> bot x

and by eta reduction

This is the point --- by the existence of seq, eta reduction is unsound in Haskell.

Am I correct in assuming that if my program doesn't contain seq then I can reason using eta reduction?

Yes.

...

...

Why is seq introduced?

Waiting for computers to get fast enough to run Haskell got old.

I'm guessing you were not being entirely serious here but I think that's a good answer.

...

Oh, you mean here? Equality (=) for pickier Haskellers always means Leibnitz' equality:

Given x, y :: alpha

x = y if and only if for all functions f :: alpha -> (), f x = f y

f ranges over all functions definable in Haskell, (for some version of the standard), and since Haskell 98 defined seq, the domain of f includes (`seq` ()). So since bot and (\ x -> bot x) give different results when handed to (`seq` ()), they must be different.

The `equational reasoning' taught in functional programming courses is unsound, for this reason. It manages to work as long as everything terminates, but if you want to get picky you can find flaws in it (and you need to get picky to justify extensions to things like infinite lists).

Reasoning as though you were in a category with a bottom should be ok as long as seq isn't present? I'm recalling a paper by Freyd on CPO categories which I can't lay my hands on at the moment or find via a search engine. I suspect Haskell (without seq) is pretty close to a CPO category.

Not quite --- not if by `a category with bottom' you mean the standard category of pointed CPOs and strict functions, because Haskell functions aren't necessarily strict. In the actual category Hask, you don't even have finite products, because surjective pairing still fails (seq can be defined in the special case of pairs directly in Haskell). The usual solution is to ensure that everything terminates (more precisely, that everythin is total). In that case, you can pretend you're in a nice, neat purely set-theoretic model most of the time, and only worry about CPOs when you need to do fixed-point or partial- list induction or something like that. jcc

Roberto Zunino writes:

without seq, there is no way to distinguish between undefined and (const undefined),

"no way to distinguish" is perhaps too strong. They have slightly different types. Jerzy Karczmarczuk

Roberto Zunino wrote:

Dominic Steinitz wrote:

...

This would give

= \x -> bot x

and by eta reduction

This is the point: eta does not hold if seq exists.

undefined `seq` 1 == undefined (\x -> undefined x) `seq` 1 == 1

Ok I've never used seq and I've never used unsavePerformIO. Provided my program doesn't contain these then can I assume that eta reduction holds and that (.) is categorical composition?

The "(.) does not form a category" argument should be something like:

id . undefined == (\x -> id (undefined x)) /= undefined

where the last inequation is due to the presence of seq. That is, without seq, there is no way to distinguish between undefined and (const undefined), so you could use a semantic domain where they coincide. In that case, eta does hold.

It would be a pretty odd semantic domain where 1 == undefined. Or perhaps, I should say not a very useful one.

Excellent! This has all been very helpful. Thanks a lot everybody! :-) -Corey On 12/14/07, Benja Fallenstein wrote:

Hi Corey,

On Dec 14, 2007 8:44 PM, Corey O'Connor wrote:

...

The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor?

Recall the definition of functor. From Wikipedia:

"A functor F from C to D is a mapping that

* associates to each object X in C an object F(X) in D, * associates to each morphism f:X -> Y in C a morphism F(f):F(X) -> F(Y) in D

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

http://en.wikipedia.org/wiki/Functor

We consider C = D = the category of types. Note that any type constructor is a mapping from types to types -- thus it associates to each object (type) X an object (type) F(X).

Declaring a type constructor to be an instance of Functor means that you have to provide 'fmap :: (a -> b) -> (f a -> f b)" -- that is, a mapping that associates to each morphism (function) "fn :: a -> b" a morphism "fmap fn :: f a -> f b".

Making sure that the two laws are fulfilled is the responsibility of the programmer writing the instance of Functor. (I.e., you're not supposed to do this: instance Functor Val where fmap f (Val x) = Val (x+1).)

Hope this helps with seeing the correspondence? :-) - Benja

-- -Corey O'Connor