[Haskell-cafe] Join and it's relation to >>= and return
franka at cs.uu.nl
Fri Jun 11 08:22:34 EDT 2004
On Jun 9, 2004, at 9:39 AM, Jerzy Karczmarczuk wrote:
> I have *nothing* to add, just a question.
> Do you /anybody/ know of any edible work on ADJUNCTIONS in the context
> of Haskell structures? Perhaps instead of searching for 'inverses' one
> should think more about adjoints?...
Yes, I think this is the right way to go. If you look at work by Power,
Thielecke and Streicher on continuations [*], you will find that they
model type negation as a self-adjoint functor on a closed premonoidal
category, and IIRC a closed premonoidal category is equivalent to a
thing called a closed kappa-category with a computational monad on it.
The self-adjointness corresponds to the involutivity of negation.
This all depends on the tensor product being commutative. It's also
possible to drop commutativity, in which case you end up with _two_
exponentials, also called residuals, corresponding to the two ways to
curry a non-commutative product. Such a category can serve as a
proof-theoretic model for Lambek calculus, which is used in categorial
In this situation, if you demand a multiplicative inverse, or
equivalently a dual to the unit, you get _two_ negations or (better I
think) `dualizers'. Barr treats this in a few of his papers, including
, and  for the simpler commutative case. There is a neat way of
forming such categories, called the Chu construction , which has
provoked much interest in the categorical community.
I once wrote some notes on something I called action logic, which tried
to organize these ideas at a simpler level. The logic was
non-commutative and had two dualizers like I said, and was designed to
be sound and complete for a model where every proposition was
interpreted by an adjoint pair of functions (or, just a Galois
connection), and dualization by replacing a function by its (unique)
adjoint. It all worked out very nicely because adjoints have such neat
properties. I still have the notes if you're interested.
[*] CiteSeer seems kind of broken, so try:
 Michael Barr, Non-symmetric *-autonomous categories, 1999.
More information about the Haskell-Cafe