On 16/01/07, Neil Mitchell wrote:

For some reason, in Firefox printing those diagrams to a black and white printer gives black for the background. It means that the arrows and annotations are in black on black, not the most readable...

I've uploaded new versions using a white background. If it still doesn't work, yell. -- -David House, dmhouse@gmail.com

Brian Hulley wrote:

David House wrote:

...

http://en.wikibooks.org/wiki/Haskell/Category_theory But in the second exercise in the intro it's clear that function composition is not associative.

Apologies. I got totally confused with the way function composition is back to front etc. I still have no idea what the solution to the second exercise is though. Thanks, Brian. -- http://www.metamilk.com

David House wrote:

I've added a bit more explanation, so it may now be palatable. It is quite a hard exercise, though, perhaps it shouldn't come so early on.

In my opinion, it is now much more clear. And it is a very instructive example. If people still find it too hard, you could add the additional hint: Keep in mind that there are no morphisms other than the ones shown in the diagram. Regards, Yitz

On 17/01/07, Brian Hulley wrote:

Ok I understand it now, because David has just clarified offlist the thing that puzzled me about the diagram: namely that morphisms have an individuality of their own that isn't fully determined by the lhs and rhs of the arrow like the relationship between a function and its type.

I've written a bit more, moved things around and just generally made the intro section clearer. Your troubles have been addressed with an explanatory sentence that gives sin and cos as examples of morphisms with the same source and target objects but that are different. We now deal with composition a bit better too; when we're defining a category we briefly mention composition but the closure under the composition operator is now defined and exemplified alongside the other two laws. Thanks, Brian, for your input, it's been valuable. I hope everything's clear now. -- -David House, dmhouse@gmail.com

On 17/01/07, Yitzchak Gale wrote:

A few semicolons were missing in the do blocks of the Points-free style/Do-block style table. I fixed that. I think it would be simpler without the do{} around f x and m - are you sure it's needed?

They're not needed, but I think it makes it more symmetric. It also clarifies that we're talking about moving things around within do-blocks; one could potentially have statements before and after the given statements. There isn't much of a case either way, I guess.

You wrote: "category theory doesn't have a notion of 'polymorphism'". Well, of course it does - after all, this is "abstract nonsense", it has a notion of *everything*. But obviously we don't want to get into that complexity here. Here is a first attempt at a re-write of that paragraph:

Note: The function id in Haskell is 'polymorphic' - it can have many different types as its domain and range. But morphisms in category theory are by definition 'monomorphic' - each morphism has one specific object as its domain and one specific object as its range. A polymorphic Haskell function can be made monomorphic by specifying its type, so it would be more precise if we said that the Haskell function corresponding to idA is (id :: A -> A). However, for simplicity, we will ignore this distinction when the meaning is clear.

I've changed the paragraph to almost what you said, modulo a few tweaks to make it sit nicer with the rest of the article.

It is nice that you gave proofs of the >>= monad laws in terms of the join monad laws. I think you should state more clearly that the two sets of laws are completely equivalent. (Aren't they?) Maybe give the proofs in the opposite direction as an exercise.

Yes, they are, here are my proofs: join . fmap join = join . join join . fmap join (\m -> m >>= id) . fmap (\m -> m >>= id) \m -> (m >>= (\n -> return (n >>= id))) >>= id \m -> m >>= (\n -> return (n >>= id) >>= id) \m -> m >>= (\n -> id (n >>= id)) \m -> m >>= (\n -> n >>= id) \m -> m >>= (\n -> id n >>= id) \m -> (m >>= id) >>= id \m -> join m >>= id \m -> join (join m) join . join join . fmap return = id join . fmap return (\m -> m >>= id) . (\m -> m >>= return . return) \m -> (m >>= return . return) >>= id \m -> m >>= (\n -> return (return n) >>= id) \m -> m >>= (\n -> id (return n)) \m -> m >>= (\n -> return n) \m -> m >>= return \m -> m id join . return = id join . return (\m -> m >>= id) . (\m -> return m) \m -> return m >>= id \m -> id m id return . f = fmap f . return return . f (\x -> fmap f x) . return \x -> fmap f (return x) \x -> return x >>= return . f \x -> (return . f) x return . f join . fmap (fmap f) = fmap f . join join . fmap (fmap f) (\m -> m >>= id) . (\m -> m >>= return . (\n -> n >>= return . f)) \m -> (m >>= return . fmap f) >>= id \m -> (m >>= \x -> return (fmap f x)) >>= id \m -> m >>= (\x -> return (fmap f x) >>= id) \m -> m >>= (\x -> id (fmap f x)) \m -> m >>= (\x -> fmap f x) \m -> m >>= (\x -> x >>= return . f) \m -> m >>= (\x -> id x >>= return . f) \m -> (m >>= id) >>= return . f (\m -> m >>= id) >>= return . f fmap f . (\m -> m >>= id) fmap f . join I've added the suggested exercise. -- -David House, dmhouse@gmail.com

Hi

Isn't _|_ = \x -> _|_?

_|_ `seq` () = _|_ (\x -> _|_) `seq` () = () Whether this is the fault of seq or not is your call... Thanks Neil

Hi, Am Donnerstag, den 18.01.2007, 16:45 +0000 schrieb David House:

On 18/01/07, Joachim Breitner wrote:

...

(.) :: (b -> c) -> (a -> b) -> a -> c id :: a -> a therefore b = a therefore _|_ :: a -> c

(This is mostly rough guesswork, I might be totally wrong)

That much is right, but remember that just because _|_ has type a -> c doesn't mean it takes a parameter. Bottom can take any type, and I don't think _|_ == \x -> _|_.

But if _|_ can take on any type, it can take on a -> b. And in what way does it then differ from \x -> _|_? Greetings, Joachim -- Joachim Breitner e-Mail: mail@joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189

On 18/01/07, David House wrote:

You can tell them apart, using seq, as Neil showed, but apart from that I guess they're unique. If you had:

s/unique/the same/ -- -David House, dmhouse@gmail.com

On 18/01/07, Johan Gršnqvist wrote:

f = idA . f = (h . g) . f = h . (g . f) = h . idB = h

Thus in the figure f=h must hold, nad one arrow can be removed from the graph.

The point from here was to conclude that this graph can't represent a category, not that f = h. You have the gist of the exercise, though! :) -- -David House, dmhouse@gmail.com

Ulf Norell wrote:

In the section on the category laws you say that the identity morphism should satisfy

f . idA = idB . f

This is not strong enough. You need

f . idA = f = idB . f

Unfortunately, fixing this means that the category Hask is no longer a category since

_|_ . id = \x -> _|_ =/= _|_

Neil Mitchell wrote:

...

Isn't _|_ = \x -> _|_?

_|_ `seq` () = _|_ (\x -> _|_) `seq` () = ()

Whether this is the fault of seq or not is your call...

Subtle, subtle.

From the point of view of denotational semantics, the functions (x \mapsto _|_) and _|_ are the same as equality and the semantic approximation order are defined point-wise. Usually, the morphisms of some category arising from a (non-normalizing or polymorphic) lambda calculus are given by such partial functions.

The key point about lambda calculi is that the "external" morphisms sets can be "internalized", i.e. represented as objects of the category themselves. So, the set of morphisms from 'Integer' to 'Integer' can be represented by the type 'Integer -> Integer'. But, as the example with `seq` shows, this is not entirely true. Apparently, Haskell represents function types in a boxed way, i.e. they are lifted by an extra _|_: newtype ClosureInt2Int = Closure (Integer -> Integer)# Thus, Hask is not a category, at least not as defined in the article. The problem is that (either) morphisms or the morphism composition ('.') are not internalized correctly in Haskell. Regards, apfelmus

Lennart Augustsson wrote:

On Jan 19, 2007, at 08:05 , apfelmus@quantentunnel.de wrote:

...

Thus, Hask is not a category, at least not as defined in the article. The problem is that (either) morphisms or the morphism composition ('.') are not internalized correctly in Haskell.

And this is why some of us think that adding polymorphic seq to Haskell was a mistake. :(

I've often wondered why seq is the primitive and not $! Would this solve the problem? Is there any solution that would allow excess laziness to be removed from a Haskell program such that Hask would be a category? Thanks, Brian. -- http://www.metamilk.com

Neil Mitchell wrote:

Hi Brian,

...

Is there any solution that would allow excess laziness to be removed from a Haskell program such that Hask would be a category?

class Seq a where seq :: a -> b -> b

Then you have a different seq based on the types, and it doesn't go wrong. You would probably want deriving Seq support.

This seems an amazingly neat solution to a really terrible problem, so: 1) Does anyone know why this was not used in the first place? 2) Would it be good to use this in future versions of Haskell? 3) Is there any practical program which requires the current seq that could not be rewritten to use the typeclass seq? Thanks, Brian. -- http://www.metamilk.com

On 1/20/07, Brian Hulley wrote:

Neil Mitchell wrote:

...

Hi Brian,

...

Is there any solution that would allow excess laziness to be removed from a Haskell program such that Hask would be a category?

class Seq a where seq :: a -> b -> b

Then you have a different seq based on the types, and it doesn't go wrong. You would probably want deriving Seq support.

This seems an amazingly neat solution to a really terrible problem, so:

1) Does anyone know why this was not used in the first place?

It *was* used before. See section 6.2.7 of the Haskell 1.4 report. It was throw out in Haskell98. I don't remember why though.

2) Would it be good to use this in future versions of Haskell?

3) Is there any practical program which requires the current seq that could not be rewritten to use the typeclass seq?

I'll pass on these two questions. /Josef

On Friday 19 January 2007 18:09, Brian Hulley wrote:

Neil Mitchell wrote:

...

Hi Brian,

...

Is there any solution that would allow excess laziness to be removed from a Haskell program such that Hask would be a category?

class Seq a where seq :: a -> b -> b

Then you have a different seq based on the types, and it doesn't go wrong. You would probably want deriving Seq support.

This seems an amazingly neat solution to a really terrible problem, so:

1) Does anyone know why this was not used in the first place?

It was this way in Haskell 1.4, but was changed for Haskell 98. IIRC, there is a fairly complete discussion of this issue in the "History of Haskell" paper draft that SP Jones et al circulated about for comment. Unfortunately, those drafts seem to have been pulled now, so I can't double check or give you a link.

2) Would it be good to use this in future versions of Haskell?

3) Is there any practical program which requires the current seq that could not be rewritten to use the typeclass seq?

Thanks, Brian.

| IIRC, there is a fairly complete discussion of this issue in the "History of | Haskell" paper draft that SP Jones et al circulated about for comment. | Unfortunately, those drafts seem to have been pulled now, so I can't double | check or give you a link. We're revising it. It'll be back online in a week or two. Incidentally, it's SPJ or S Peyton Jones or Simon PJ or Simon Peyton Jones, but not SP Jones! ("Peyton Jones" is my last name.) Simon

No, making $! the primitive would not help. You can define seq from $!. I think seq is a "suitable" primitive, it's just that it ruins nice properties. The original formulation of seq in Haskell was the right one in my opinion: class Eval where seq :: a -> b -> b This way you get a context on anything that uses seq and you can tell that there is some funny business going on. -- Lennart On Jan 19, 2007, at 13:07 , Brian Hulley wrote:

Lennart Augustsson wrote:

...

On Jan 19, 2007, at 08:05 , apfelmus@quantentunnel.de wrote:

...

Thus, Hask is not a category, at least not as defined in the article. The problem is that (either) morphisms or the morphism composition ('.') are not internalized correctly in Haskell.

...

And this is why some of us think that adding polymorphic seq to Haskell was a mistake. :(

I've often wondered why seq is the primitive and not $! Would this solve the problem? Is there any solution that would allow excess laziness to be removed from a Haskell program such that Hask would be a category?

Thanks, Brian. -- http://www.metamilk.com