Talk:Haskell/Category theory

From Wikibooks, the open-content textbooks collection

This page is getting there. Some stuff I'd still like to do:

• More exercises
• Diagrammatic explanations of CT concepts

Contents 1 Monad laws are incorrect 2 Strong monads 3 Powerset eq List Monad? 4 Right chapter? 5 Category theory wikibook 6 Suggestion 7 Review from the Haskell-cafe mailing list 8 Diagrams 9 Comment 10 adjoint functors 11 Convention used for function composition 12 Typographical conventions for unit, join

[edit] Monad laws are incorrect

Hi all. I was looking over the monad laws section and noticed some errors in the first and second laws. The first law is incorrect because join cannot be composed with join since it is a function from M^2 to M. The confusion here is on subscripts: the join_x can be lifted to join_{Mx} which will then be ok. It is better to write this as (join M) using the standard monad notion. I.e the first law should read jM.j = j.jM. See the wikipedia article on monads (category theory) for the correct commutative diagrams.

There is a similar abuse of notation problem with the second law. This may be confusing to the inexperienced. I did not change them because of the following example would have to be altered as well. Perhaps a note about the abuse of notation would be sufficient since it will be awkward to explain the haskell code equivalent. -- Marc

The trouble comes from the fact that in Haskell, join is of polymorphic type forall m, a . Monad m => m (m a) -> m a. The parametrization on the monad m is not important here, but the parametric type variable a is. This makes it a function and a natural transformation at the same time with a being the type argument. The point is that the Haskell compiler will accept the composition join . join because it can figure out that the first join takes the base type m X if the other takes a base type X. In other words, it will infer the subscripts automatically. I'm unsure what to do here, but I suspect that this has to be explained at some point anyway. -- apfeλmus 09:30, 8 March 2007 (UTC)

I agree that it is just an abuse of notation and that it doesn't affect the code since the compiler is smart enough to figure out what is going on. This is why I didn't go trampling through the page making changes. I do think that it is worth mentioning that this happens for clarity.

Perhaps something like: Notice that the subscript on the second join is actually Mx so that this composition is proper from a category-theoretic standpoint, but since join is of polymorphic type in Haskell the compiler understands which join is meant from context, so in (coding) practice the distinction is not important. -- Marc

Actually, I think I should have called it "type inference" instead of "compiler". From the Haskell point of view, "subscript" may be confusing :), it's "type specialization". Maybe something like: "note that the second join is specialized to the type m (m (m a)) -> m (m a)".

But the issue is more subtle than that: because of polymorphism, the category Hask allows to internalize not only morphisms but natural transformations as well. I'm not well-versed in category theory but I guess there is some construction corresponding to that? In particular, I suspect that the naturality laws 3 and 4 are free theorems (although I don't know whether higher kinded free theormes have been worked out yet). I think that this what makes innocent looking Haskell notation break with the standard category theory notation.

Maybe it's best to simply introduce natural transformations explicitely in the article and solve notational and conceptional problems with that. Hiding them is probably more confusing than giving a translation between Cat-speak and Haskell-speak. Actually, I like the Tμ notation more than subscripts or type inference because it results in more symmetric monad laws. -- apfeλmus 21:47, 8 March 2007 (UTC)

I am well versed in category theory, but fairly new to haskell. I'm using my category theory skills to understand haskell, which is how I ended up here. I think that laws 3 and 4 are ok -- they are just expressing the requirement that unit and join must be natural transformations.

I'm not sure if it is worth giving a significant introduction to natural transformations into the article, though a mention and a link to a wikipedia page might be appropriate. My main concern is just that the monad laws be replaced with their correct formulations so that others approaching this in the manner that I have won't have to wrestle with the laws for a while before figuring out that they are not what a category theorist would expect. (Normally I would not be such a stickler, but this is the category theory article after all.) I am, however, willing to help make the article more in-depth from a category-theoretic point of view. Perhaps in conjunction with more concepts we will find that we need to discuss natural transformations. Marc Harper 02:19, 9 March 2007 (UTC)

I agree, it's a category theory article, after all :) So, subscripts are important. I'm unsure on how to state the categorially correct monad laws without natural transformations? Concerning the introduction of concepts, the rule of thumb would be that a concept may be introduced as long as there is corresponding Haskell code for it. Of course, it's best introduced if it's also useful. Your additions would be most welcome! -- apfeλmus 09:28, 9 March 2007 (UTC)

I think that we should use the Tμ notation and explain that the type system can infer the correct domain for (M join). For the reader that understands functors, this will not be suprising since monads are functors and we are basically just applying fmap to join to lift it to the correct domain. Natural transformations can be viewed as types of the form for functors m and n, which should be sufficient for most readers.

Once some more content is added that uses natural transformations and gives interesting examples of them it may be appropriate for a more detailed discussion of natural transformations. There is a lot of categorical content to be added -- even relatively simple constructions such as identifying tuple types at the categorical product. Does anyone know of a good reference for a categorical discussion of the properties of Hask? Marc Harper 21:15, 9 March 2007 (UTC)

Agreed.

Note that the tuple is (unfortunately) not the categorial product :) This basically comes from the fact that , i.e. the tuple type has an extra element that breaks the universal property. The sum type (coproduct) Either has the same problem. For more on ("bottom") and the semantics of general recursion, see Haskell/Denotational semantics.

AFAIK, there is no concretely worked out category theory behind Hask. In general, Lambda calculi are connected to cartesian closed categories. A quick google suggests Cartesian closed categories and the λ-calculus as trampoline. I don't know where to find a categorial construction of universal quantification , but the inventors of the polymorphic lambda calculus System F are Girard and Reynolds and they have semantics for it. Then, there are initial algebra semantics for folds and generic programming in general. The "banana and barbed wires"-paper mentioned on the haskell wiki page [1] is one of the most famous in that direction. There is also the work of Moggi in Categorial semantics, he mostly deals with monads. -- apfeλmus 11:01, 10 March 2007 (UTC)

It is disappointing that it is not as elegant as it seems from the surface. Thanks for the references. -- Marc

What about restricting our attention to only strict functions in the category Hask? Then we seem to get better categorical properties. Also, if we consider types to be 'pointed' with basepoint then we can get properties such as by taking the product in the pointed category (much in analogy with pointed topological spaces). -- Marc 74.139.215.32 01:08, 28 October 2007 (UTC)

I don't think that a restriction to strict functions makes things better. While (co)products may work out fine, function types won't: () -> a and a are not isomorphic, the former can be used to simulate call-by-name in a strict language. In other words, ⊥ will still bite when considering function types. Usually, one restricts everything to total functions, thereby kicking out ⊥ completely, and that does give a satisfying category. Partiality ⊥ can then be modeled by a monad (I don't have a good reference for that but maybe [2] is a start).

For an introductory article like this one, I think the most reasonable thing to do is to mention the problem and otherwise declare all functions to be total :-) (The current article "allows" partial functions while ignoring them at the same time, I think that's a bit clumsy.)

-- apfeλmus 09:58, 28 October 2007 (UTC)

[edit] Strong monads

There is another subtlety, namely the fact that every "monad" in Haskell is also a "strong monad", but not the other way round. See Moggi's paper. This means that there is a natural transformation

 t :: Monad m => (a, m b) -> m (a,b)
 t x m = m >>= \b -> return (a,b) = join . fmap (\b -> return (a,b)) $ m

Apparently, the category Hask offers quite a lot of objects for free. -- apfelmus 21:47, 8 March 2007 (UTC)

[edit] Powerset eq List Monad?

This may be irrelevant from a pedagogical standpoint, but most of the times I've heard category theorists talk about the list monad (in the operads world), they seem to view it as something in a symmetric monoidal category, i.e. tensor products of Thingies; and not using powersets -- the powerset analogy is slightly flawed in that it would disallow things like [2,3,2,2,1,2]. On the other hand, proposing a change that actually works out simple enough for an example to be good is over my own head right now. Michiexile 09:29, 29 January 2007 (UTC)

They are not the same. This is because sets are not ordered/indexed by default, i.e. a set would not contain the element 2 twice, but a list could. As far as illustrating the idea though, they are otherwise very similar.

To be precise about the distinction, if you consider sets with the monoidal structure introduced by the cartesian product, then you can view lists as element of a product of sets. (This allows the list elements to be of different types though, so it is more properly viewed as a tuple.) So... lists of length n (in Haskell) are really elements of A^n, the product of A with itself n-times. The proper category theoretic way to view this is to generate a category with the product and a set A. Then n-lists can be viewed as a monad. If you wanted to treat all lists similtaneously, you could toss in the element B=A^{\infty}. It still has a product (B x B = B) and you could consider lists of length n to be infinite lists where all terms after the n-th are zero. -- Marc

Since you mentioned operads, the connection here is that you can view operads as monoids in the monoidal category of symmetric families of a category... I think that a discussion of operads in the article would be unecessarily complicated at this time, and even though the powerset example is not quite the same I think that it is pedagogically sufficient. -- Marc

[edit] Right chapter?

This is in the "Time and space" chapter, but the only connection to time and space (which I understand to mean performance in this context) appears to be the mention of fusion - which is tangential, and doesn't, I think, justify this article's inclusion in this chapter. --Greenrd 21:49, 16 January 2007 (UTC)

Would it be reasonable to rename the Program correctness chapter to something more general and move this there? Actually... would program correctness be reasonable as is? -- Kowey 23:00, 16 January 2007 (UTC)

I also think that it belongs to the chapter currently entitled "Program correctness" as this chapter intents to subsume anything about "Formal program manipulation". While "Program correctness" is too narrow for category theory to fit in, I have been reluctant to change the title because "Formal" could (unfortunately) scare people off. Maybe it's good idea to change the title anyway but to bait people with a subchapter "Why is my program correct?" which serves as a hands-on introduction to the "Formal program manipulation" subject? A sneakier version would be "Help, my program doesn't work" because the chapter won't tell anything about debugging, it will tell about "Program derivation from specification" and how to prove your programs do what they should. In short, it will show how to write correct programs in the first place. -- Apfelmus 10:43, 17 January 2007 (UTC)

[edit] Category theory wikibook

Have you seen Category theory? -- Kowey 09:55, 13 January 2007 (UTC)

[edit] Suggestion

I know what a Set is, but I don't know what a Group is. Perhaps link to the wikipedia pages for these two things - so people can have access to the mathematical definition.

[edit] Review from the Haskell-cafe mailing list

On the 16th Jan 2007, a message was sent regarding this article to the Haskell mailing list, asking for review and comment. This was really helpful, poking holes in my knowledge as well as helping to improve the article manyfold. Most of the changes you can see in the history since that date are tweaks due to that review. Noteable reviewers were Brian Hulley and Yitzchak Gale, whose comments were very encouraging and hopefully had a bit influence on the article's content. DavidHouse 18:32, 19 January 2007 (UTC)

[edit] Diagrams

... were done using the Inkscape vector editing program. The original SVG files are available on request, email me (see my talk page). DavidHouse 18:32, 19 January 2007 (UTC)

The wikimedia projects (e.g. wikibooks) support .svg diagrams. Have you given it a try? It works badly on the ones produced by Omnigraffle; perhaps you would have better luck -- Kowey 19:38, 19 January 2007 (UTC)

Also, it's highly worth it to move the diagrams to commons. This will make the diagrams transparently shareable across all wikimedia projects, for example, a hypothetical French version of the wikibook -- Kowey 19:40, 19 January 2007 (UTC)

[edit] Comment

The first exercise asks 'As was mentioned, any partial order (P, \leq) is a category with objects as the elements of P and a morphism between elements a and b iff a \leq b. Which of the above laws guarantees the transitivity of \leq?' This seems backwards to me. The statement is that a partial order gives rise to a category, not the other way around. Given a paritial order we don't need to gaurantee the transitivity of \leq. That is an axiom. The question should be something along the lines of 'which of the axioms of a poset guarantees the second category theory law?' -- astrolabe

Morphism composition. If the existence of a (unique) f_{a,b} from a to b is equivalent to a \leq b, then: a\leq b and b\leq c means there are f_{a,b} and f_{b,c}, therefore there must be f_{a,c} = f_{b,c} . f_{a,b} --- which amounts to saying a must be \leq c. -- askyle

[edit] adjoint functors

I read somewhere that monad transformers were really adjoint functors, whatever those are. Could some explanation be added? I like this article a lot and it helped me with the traditional stumbling block of understanding monads (I sort of get them now), but I'm still baffled by monad transformers. Thanks

Oh? That would be interesting, I only know that every pair of adjoint functors (like and ) gives rise to a monad (). Concerning monad transformers, the wikibook has a chapter on them, but it's not optimal yet. Meanwhile, have a look at [3]. Concerning adjoint functors, this module will hopefully explain them at some point in the future. -- apfeλmus 10:21, 7 December 2007 (UTC)

[edit] Convention used for function composition

In the section on Category Laws, we have the following:

… if and , then there must be some morphism in the category such that .

This suggests that is being used here for the morphism that results from composition of the morphism f preceding the morphism g. However, this conflicts with the Haskell composition notation, in which (well, f.g) refers to the composition of the morphism f following the morphism g.

The section is also internally inconsistent in that it states that for the category shown in the figure, for which and , and . (This corresponds to the convention used in Haskell.). But for the same category, the text states that (which uses the opposite – and un-Haskell-like – convention).

Which convention should be adopted here? (I’m no authority on Haskell or on category theory, so I wouldn’t wish to make the choice myself.)

See also the compositions for unit and join, which appear to use the Haskell-like convention.

Oh! The "Haskell" convention is correct. In fact, it's the convention used all over mathematics. Fixed. -- apfeλmus 08:16, 10 April 2008 (UTC)

Not used ‘all’ over mathematics – but certainly by far the most common convention, I agree. (And my comment on the last relation there was mistaken, as it wasn’t of course referring to the category in the diagram.) Thanks for fixing this. --Axnicho (talk) 09:17, 10 April 2008 (UTC)

-- It would be more instructive, I think, when in the diagram that explains the existence of f o g and g o f, there is for at least one of them another option than just id. Currently, the example is such that both f o g and g o f are the identity, and this might be misleading for the beginner.

[edit] Typographical conventions for unit, join

In this article, we have, for example:

Is this really the desired typography? I’d have been inclined to use

But perhaps there is some Haskell convention that I’m unaware of? (The same applies to unit.)

Function names in italic (more precisely \mathit{} in LaTeX) have a widespread tradition in papers about functional programming and Haskell, especially when there is some "mathematical" touch to them. A prototypical example is probably the book The Fun of Programming. Some chapters are available online, like Fun with Binary Heap Trees. Naturally, typewriter face is widespread, too. A variable width but upright font is the exception, a prominent example being Chris Okasaki's thesis and corresponding book.

In other words, italic is what we want here :-) -- apfeλmus 08:42, 10 April 2008 (UTC)

OK – I can accept that italic is used in Haskell and functional-programming papers (though why the standard mathematical convention that I mentioned should be used specifically in papers with ‘some "mathematical" touch to them’ eludes me!). Still, at the very least, we should improve the typography so that it looks more like this (I have made this change):

By using math-mode italics (bare $…$) rather than \mathit{…} or \textit{…}, the spacing of the word ‘join’ is pretty awful – and a poor advertisement for TeX. As Lamport notes in the LaTeX 2ε user guide (p. 51):

‘LaTeX normally uses an italic type style for letters in math mode. However, it interprets each letter as a separate mathematical symbol [which is not what we want here], and it produces very different spacing than an ordinary italic typestyle. You should use \mathit for multiletter symbols in formulas.’

--Axnicho (talk) 09:35, 10 April 2008 (UTC)

Yes, thanks for making the change to \mathit{} :-)

Concerning the italic convention, I imagine it as follows: usually, the objects of mathematical discourse have only one-letter names like x or ζ. This is not practical for programming, so multi-letter names like map or foldr are used. But since they're almost on "equal footing" with those nice looking italic letters, they gotta be italic, too. I mean, in the papers with "mathematical touch", they're not so much actual code to be typed into the terminal (-> typewriter face), but mathematical entities that obey laws like . (Hm, same for sin(x) of course. Must be the higher order functions, i.e. the fact that map can also be argument of a function. Oh well, whatever, it looks good :-)

-- apfeλmus 13:15, 11 April 2008 (UTC)