Re: [Haskell-cafe] Article review: Category Theory
I wrote: Time to re-write the "Note" paragraph yet again. David House wrote: This was a bit much to include in the introduction section I agree 100%. I added a footnote. It's excellent! I tend to take the view that we should ignore seq when talking about abstract language properties That is certainly the right approach in an introductory text. Regards, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
One nit and one massive praise. nit first. in 'the monad laws and their importance' you say "given a monad M" and then outline the laws a functor must satisfy to be a monad. I would find it clearer to say 'a functor M', and then emphasise the iff relationship between the laws and the functor M. the praise: footnote 3. the relationship between join and bind is why monads are useful and interesting for programmers. i haven't seen it stated more clearly before. i supose because people who know it assume it. suggestion: don't bury this in a footnote. On 1/16/07, David House <[EMAIL PROTECTED]> wrote: Hey all, I've written a chapter for the Wikibook that attempts to teach some basic Category Theory in a Haskell hacker-friendly fashion. http://en.wikibooks.org/wiki/Haskell/Category_theory >From the article's introduction: "This article attempts to give an overview of category theory, insofar as it applies to Haskell. To this end, Haskell code will be given alongside the mathematical definitions. Absolute rigour is not followed; in its place, we seek to give the reader an intuitive feel for what the concepts of category theory are and how they relate to Haskell." I'd love comments from newcomers and experts alike regarding my approach, the content, improvements and so on. Of course, it's on the wikibook, so if you have anything to add (that's not _too_ substantial otherwise I'd recommend discussion first) then go ahead. Thanks in advance. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 19/01/07, Yitzchak Gale <[EMAIL PROTECTED]> wrote: OK, thanks! Time to re-write the "Note" paragraph yet again. Here goes a first shot at it: This was a bit much to include in the introduction section, so I added a footnote. Hopefully I got everything right; I tend to take the view that we should ignore seq when talking about abstract language properties so if the comment seems biased towards blaming seq, that's why. :) -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On Fri, 19 Jan 2007, Ulf Norell <[EMAIL PROTECTED]> wrote: > Personally I think that the distinction between _|_ and \x -> _|_ is > a mistake and should be ignored whenever possible. If you want to write an accessible tutorial you should probably use a total programming language, or at least the total fragment of some language, for the programming-related examples. I'd mention the problems with Haskell, restrict the language in some way, and then move on. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On Jan 19, 2007, at 1:06 PM, Yitzchak Gale wrote: Hmm. I wrote: for simplicity, we will ignore these distinctions But do we really want to do that? Are the "monads" that we use every day in Haskell really monads if we check the axioms using (.!) instead of (.) as we should? I'm not so sure anymore... Personally I think that the distinction between _|_ and \x -> _|_ is a mistake and should be ignored whenever possible. / Ulf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Hmm. I wrote: for simplicity, we will ignore these distinctions But do we really want to do that? Are the "monads" that we use every day in Haskell really monads if we check the axioms using (.!) instead of (.) as we should? I'm not so sure anymore... Maybe this is the explanation of the problems we have been discussing recently about strictness in the MTL monads. -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
I wrote:
OK, so then how about
> f .! g = ((.) $! f) $! g
Ulf Norell wrote:
That should probably do the trick.
OK, thanks! Time to re-write the "Note"
paragraph yet again. Here goes a first
shot at it:
: id . f = f . id = f
'Note:' It turns out that the usual identity function id
and composition function (.) in Haskell are actually not
exactly what we need for the '''Hask''' category.
The function id in Haskell is ''polymorphic'' - it can
take many different types for its domain and range, or, in
category-speak, can have many different source and target objects. But
morphisms in category theory are by definition ''monomorphic'' - each
morphism has one specific source object and one specific target
object. A polymorphic Haskell function can be made monomorphic by
specifying its type (''instantiating'' with a monomorphic type), so it
would be more precise if we said that the identity morphism from
'''Hask''' on a type A is (id :: A -> A).
With this in mind, the above law would be rewritten as:
: (id :: B -> B) . f = f . (id :: A -> A)
The Haskell composition function (.) is lazy, so the
required identity
id . f = f is not true when we take f = undefined:
we have (id . undefined) `seq` "foo" = "foo", but
undefined `seq` "foo" is equivalent to undefined.
To fix this problem, we can define a strict composition function:
: f .! g = ((.) $! f) $! g
Now the above law looks like this:
: (id :: B -> B) .! f = f .! (id :: A -> A)
In this form, the law is correct, and ''Hask'' is a category.
However, for simplicity, we will ignore these distinctions
when the meaning is clear.
-Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On Jan 18, 2007, at 10:09 PM, Yitzchak Gale wrote: I wrote: Will (id :: A -> A $!) do the trick? Ulf Norell wrote: The problem is not with id, it's with composition. For any f and g we have f . g = \x -> f (g x) So _|_ . g = \x -> _|_ for any g. OK, so then how about f .! g = ((.) $! f) $! g That should probably do the trick. / Ulf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
I wrote: Will (id :: A -> A $!) do the trick? Ulf Norell wrote: The problem is not with id, it's with composition. For any f and g we have f . g = \x -> f (g x) So _|_ . g = \x -> _|_ for any g. OK, so then how about f .! g = ((.) $! f) $! g -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 18/01/07, Daniel Fischer <[EMAIL PROTECTED]> wrote: Since I don't know whether I would have to register to modify the wiki or something (and don't know what markup to use either), I just send you a few corrections by e-mail. Thanks; I've corrected them all, with the exceptions of the ones shown below. http://en.wikibooks.org/w/index.php?title=Haskell/Category_theory&diff=723109&oldid=722587 perhaps index join/unit with the appropriate objects, e.g. join_X . M(join_X) = join_X . join_M(X), to aid the newcomers? the picture's left is the text's right. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 18/01/07, David House <[EMAIL PROTECTED]> 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, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 18/01/07, Joachim Breitner <[EMAIL PROTECTED]> wrote: But if _|_ can take on any type, it can take on a -> b. And in what way does it then differ from \x -> _|_? _|_ is bottom. \x -> _|_ is a function that takes a value and returns bottom. You can tell them apart, using seq, as Neil showed, but apart from that I guess they're unique. If you had: f = undefined g = \x -> undefined Then f x = g x for all x. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Hi, Am Donnerstag, den 18.01.2007, 16:45 + schrieb David House: > On 18/01/07, Joachim Breitner <[EMAIL PROTECTED]> 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: [EMAIL PROTECTED] Homepage: http://www.joachim-breitner.de ICQ#: 74513189 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 18/01/07, Joachim Breitner <[EMAIL PROTECTED]> 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 -> _|_. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Hi Isn't _|_ = \x -> _|_? _|_ `seq` () = _|_ (\x -> _|_) `seq` () = () Whether this is the fault of seq or not is your call... Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Hi, Am Donnerstag, den 18.01.2007, 15:05 +0100 schrieb Ulf Norell: >_|_ . id = \x -> _|_ ≠ _|_ Isn’t _|_ = \x -> _|_? Or better stated: For your first _|_ to be used in (.), it has to take an argument, therefore it is \x -> _|_. (.) :: (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) Joachim -- Joachim Breitner e-Mail: [EMAIL PROTECTED] Homepage: http://www.joachim-breitner.de ICQ#: 74513189 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On Jan 16, 2007, at 7:22 PM, David House wrote: Hey all, I've written a chapter for the Wikibook that attempts to teach some basic Category Theory in a Haskell hacker-friendly fashion. http://en.wikibooks.org/wiki/Haskell/Category_theory 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 -> _|_ ≠ _|_ Also it's a bit strange to state that morphisms are closed under composition after the associativity law. Wouldn't it be nicer to introduce composition as a total operation off the bat? / Ulf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
I wrote: It is nice that you gave proofs of the >>= monad laws in terms of the join monad laws... Maybe give the proofs in the opposite direction as an exercise. David House wrote: Yes, they are, here are my proofs:... I've added the suggested exercise. Alas, too late - you've published the solutions! :) Regards, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 17/01/07, Brian Hulley <[EMAIL PROTECTED]> 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, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 17/01/07, Yitzchak Gale <[EMAIL PROTECTED]> 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, [EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Yitzchak Gale wrote: 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. 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. Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
David House wrote:
I've written a chapter for the Wikibook that attempts to teach some
basic Category Theory in a Haskell hacker-friendly fashion.
http://en.wikibooks.org/wiki/Haskell/Category_theory
Very, very nice!
A few comments:
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?
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.
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.
Regards,
Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 17/01/07, Brian Hulley <[EMAIL PROTECTED]> wrote: I still have no idea what the solution to the second exercise is though. 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. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
David House wrote: http://en.wikibooks.org/wiki/Haskell/Category_theory I'd love comments from newcomers and experts alike regarding my approach, the content, improvements and so on. Of course, it's on the wikibook, so if you have anything to add (that's not _too_ substantial otherwise I'd recommend discussion first) then go ahead. Hi David, In the introduction you say that Set is the category of all sets with morphisms as standard functions and composition as standard function composition. But in the second exercise in the intro it's clear that function composition is not associative. Therefore surely this means everything based on function composition can't be a category? Also, why does this exercise contain redundant morphisms (I hope I'm not spoiling it for anyone by saying this or perhaps I've just totally misunderstood everything)? Thanks, Brian. -- http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On 16/01/07, Neil Mitchell <[EMAIL PROTECTED]> 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, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
Hi David, 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... Any way to fix that? Perhaps uploading diagrams with white backgrounds, instead of transparent (if that is currently the case) Thanks Neil On 1/16/07, David House <[EMAIL PROTECTED]> wrote: Hey all, I've written a chapter for the Wikibook that attempts to teach some basic Category Theory in a Haskell hacker-friendly fashion. http://en.wikibooks.org/wiki/Haskell/Category_theory >From the article's introduction: "This article attempts to give an overview of category theory, insofar as it applies to Haskell. To this end, Haskell code will be given alongside the mathematical definitions. Absolute rigour is not followed; in its place, we seek to give the reader an intuitive feel for what the concepts of category theory are and how they relate to Haskell." I'd love comments from newcomers and experts alike regarding my approach, the content, improvements and so on. Of course, it's on the wikibook, so if you have anything to add (that's not _too_ substantial otherwise I'd recommend discussion first) then go ahead. Thanks in advance. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
