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
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
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: : <code>id . f = f . id = f</code> '''''Note:''''' It turns out that the usual identity function <code>id</code> and composition function <code>(.)</code> in Haskell are actually not exactly what we need for the '''Hask''' category. The function <code>id</code> 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 <code>A</code> is <code>(id :: A -> A)</code>. With this in mind, the above law would be rewritten as: : <code>(id :: B -> B) . f = f . (id :: A -> A)</code> The Haskell composition function <code>(.)</code> is lazy, so the required identity <code>id . f = f</code> is not true when we take <code>f = undefined</code>: we have <code>(id . undefined) `seq` "foo" = "foo"</code>, but <code>undefined `seq` "foo"</code> is equivalent to <code>undefined</code>. To fix this problem, we can define a strict composition function: : <code>f .! g = ((.) $! f) $! g Now the above law looks like this: : <code>(id :: B -> B) .! f = f .! (id :: A -> A)</code> 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
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
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
On Fri, 19 Jan 2007, Ulf Norell
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
On 19/01/07, Yitzchak Gale
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, dmhouse@gmail.com
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
participants (4)
-
David House -
Nils Anders Danielsson -
Ulf Norell -
Yitzchak Gale