Comments on A Neighborhood of Infinity: Categories of polynomials and comonadic plumbing

Dan, Edward, thank you for the explanation; it ma...

2008-07-18T18:54:00.000-07:00

Dan, Edward, thank you for the explanation; it makes sense now.

Sorry about that. I forgot the context of the arti...

2008-07-03T08:21:00.000-07:00

Sorry about that. I forgot the context of the article. It has been long enough that this thread has kind of taken on a life of its own. =)

Edward,

I did mention that I was dealing wi...

2008-07-03T08:05:00.000-07:00

Edward,

I did mention that I was dealing with a subset of Haskell that allows only total functions. It's messy otherwise.

() has two inhabitants _|_ and (), so there are mu...

2008-07-03T04:55:00.000-07:00

() has two inhabitants _|_ and (), so there are multiple functions from a -> () the moment you allow recursion, which causes () to fail to be terminal.

Also because Haskell is not total you need to be careful, since

data Void

has a single inhabitant _|_ and satisfies (most of) the conditions for a terminal object.

Of course all of this is a pleasant fiction because in the presence of seq you can even distinguish some inhabitants of a -> _|_. But if we ignore seq we get nice properties.

Unfortunately, since _|_ is an inhabitant of every type in Haskell, there is no initial object in Hask.

One way to see Void is not initial is to see that there is no uniqueness to the function from Void -> a for each a in Haskell. you are free to choose any inhabitant of a, each giving rise to another morphism in the category. The uniqueness constraint is violated. If we were strict then we might be able to say that the only member of that type was a function returning _|_.

Another way to look at it: for Hask to be comonoidal there would have to be a type Void for which 'Either Void a' can only contain 'Right a's since you can have 'Left _|_'s. This prevents the category of Haskell types from being CoCartesian.

This is why in category-extras this constraint is captured by saying Hask is pre-(co-Cartesian closed).

Piet,

1 is definitely terminal, there's alw...

2008-07-03T03:08:00.000-07:00

Piet,

1 is definitely terminal, there's always a map from X to 1 defined (in Haskell) by

const () :: a -> ()

0, or the 'empty' type defined by the (extended) Haskell

data Void

is initial.

'Elements' of objects X can be picked out using maps from the terminal object to X. So in Set maps 1->X are the same as elements of X.

"[...] introduce the function x:1->A where...

2008-07-02T02:59:00.000-07:00

"[...] introduce the function x:1->A where 1 is the terminal object in Hask, normally called ()."

s/terminal/initial/ ?

sigfpe, FYI, the link to wikipedia for Ring seems ...

2008-06-26T06:29:00.000-07:00

sigfpe, FYI, the link to wikipedia for Ring seems to be broken. The link on your blog currently points to ...

http://sigfpe.blogspot.com/%E2%80%9Dhttp://en.wikipedia.org/wiki/Ring_%28mathematics%29%E2%80%9D

... which doesn't seem to work. The link to Ring in wikipedia that does work is the following:

http://en.wikipedia.org/wiki/Ring_(mathematics)

sigfpe, the link to Wikipedia for rings seems to b...

2008-06-26T06:26:00.000-07:00

sigfpe, the link to Wikipedia for rings seems to be broken. The link that I got working is the following:

http://en.wikipedia.org/wiki/Ring_(mathematics)

... but the link on the blog entry is currently ...

http://sigfpe.blogspot.com/%E2%80%9Dhttp://en.wikipedia.org/wiki/Ring_%28mathematics%29%E2%80%9D

... which seems not to work

Off-topic, Dan, but would you have any opinion on ...

2008-06-25T08:01:00.000-07:00

Off-topic, Dan, but would you have any opinion on Dorst/Mann's use of geometric algebra to present a unified view of ray-tracing?

Hmm, I suppose "Kleisli category of T" for some fu...

2008-06-22T11:36:00.000-07:00

Hmm, I suppose "Kleisli category of T" for some functor T is ambiguous if T is both a monad and a comonad. Then you could say "Kleisli category of T as a monad" and "Kleisli category of T as a comonad", but since they're pretty verbose you'd rather just say "(co)Kleisli category", understanding that "Kleisli" refers to the monad and "coKleisli" to the comonad.

Peter:

The 'Kleisli category of a comonad' ...

2008-06-22T09:09:00.000-07:00

Peter:

The 'Kleisli category of a comonad' is unambiguous. It is also more verbose than saying 'coKleisli category'. Since one often just says the 'Kleisli construction', this enables the use of 'coKleisli construction' without introducing ambiguity into the root term.

That said, one might argue that 'co' is used a little to freely. e.g. Why aren't 'cofree comonads' just free? After all, you have to say 'comonad' in there anyways. On the other hand, you have codensity monads and density comonads, so the co- in the adjective doesn't always follow from the root idea.

In the end, I tend to subscribe to the idea that using the shotgun approach of 'co-' everywhere it is applicable enables easier application and facilitates easier communication than requiring the user of the term to know in every case which form is appropriate.

What's wrong with the idea of "Kleisli category of...

2008-06-21T18:24:00.000-07:00

What's wrong with the idea of "Kleisli category of a comonad"? It seems unambiguous to me (even if I don't fully understand comonads). Or is there some difference between "Kleisli" and "coKleisli", e.g. does it make sense to have the coKleisli category of a monad?

kim-ee:

An implementation of the exponent c...

2008-06-16T19:48:00.000-07:00

kim-ee:

An implementation of the exponent comonad:

http://comonad.com/haskell/category-extras/src/Control/Comonad/Exponent.hs

The exponent comonad is to the reader monad what the writer monad is to the product comonad.

Mikael,

the dual of the writer monad is tak...

2008-06-16T19:01:00.000-07:00

Mikael,

the dual of the writer monad is takes a comonoidal structure. in other words instead of a binary operation

join :: a * a -> a,

you need a

split :: a -> a * a

The Iavor's implementation of Augustsson, Rittri, and Synek's Supply comonad (included in category-extras) models this approximately, but uses dirty unsafePerformIO tricks to avoid excessive splitting.

http://comonad.com/haskell/category-extras/dist/doc/html/category-extras/Control-Comonad-Supply.html

I have intended to get around to adding a SupplyT comonad transformer and a pure Supply comonad, but haven't taken the time.

Finally, note that linear implicit parameters in Haskell (plague though they may be on the semantics of Haskell) implement pretty much this very idea and are a useful source of inspiration if you are looking for intuition on the use of this comonad.

Thanks Derek, that paper looks does look interesti...

2008-06-16T13:28:00.000-07:00

Thanks Derek, that paper looks does look interesting.

Mikael,

There is a monoidal comonad, althou...

2008-06-16T08:16:00.000-07:00

Mikael,

There is a monoidal comonad, although I'm not sure you'd want to call it a writer comonad. See Tarmo.

The usage is distinctly different, and I don't believe you get another monad/comonad isomorphism. The one above is the only one I know of, a consequence of product being left-adjoint to exponentiation.

Perhaps sigfpe might want to blog a nice illustration of the monoidal comonad?

Hmm...if we dualise this we should get the notion ...

2008-06-15T12:48:00.000-07:00

Hmm...if we dualise this we should get the notion of a coindeterminate, a symbol that sucks the value of subexpressions out of expressions.

Edward, does that difference in categories needed ...

2008-06-15T09:22:00.000-07:00

Edward, does that difference in categories needed dualize neatly? Is there such a thing as a writer comonad, and do you get similar differences in category properties needed between the writer monad and comonad?

Edward,

And of course the 'three way' versi...

2008-06-15T07:08:00.000-07:00

Edward,

And of course the 'three way' version of the isomorphism I give involving monads requires a CCC as it uses currying. I should write out the full details as it's not in the book. When I have a moment...

My favorite part about the reader comonad is that ...

2008-06-15T03:18:00.000-07:00

My favorite part about the reader comonad is that you can define it in weaker categories than you can define the reader monad, for much the same effect. As they noted, the reader comonad works in any Cartesian category, while the reader monad works only in a CCC.

You will probably find this paper and the papers a...

2008-06-14T18:36:00.000-07:00

You will probably find this paper and the papers also discussed (at least some of which I'm sure you've already read) interesting.

Decomposing typed lambda calculus into a couple of categorical programming languages

Anonymous,

While I tried to make it clear f...

2008-06-14T15:46:00.000-07:00

Anonymous,

While I tried to make it clear for categories, I should have also made it clearer for ordinary polynomials too - you need to have a suitable equivalence relationship on your polynomials before they are in 1-1 correspondence with functions written in terms of elements of R, multiplication and addition.

Nice post. I've also found that haskell can really...

2008-06-14T15:39:00.000-07:00

Nice post. I've also found that haskell can really help in learning category theory.

Btw, what you say about polynomials as functions is incorrect:

"So a polynomial in R[x] is the same as a function from R to R that can be written in terms of elements of R, multiplication and addition."

This is not true in general, as for example x^p - x == 0 as a function in F_p. It is of course true only for infinite fields.