Relevance and applicability of category theory
Category theory seems to have an inconsistent relationship to Haskell - both documentation and the language's implementations of categorical concepts. I come from a math background that makes the Haskell's tight coupling to its mathematical foundation very appealing. But, I may have found some inconsistencies. Whether you agree or not I hope we can get some discussion going that will clarify the wikibooks, etc. My issues: 1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship 1. Categorical monads are a class of functors, that is, morphisms on Cat. Haskell's monads are at least a bit closer to the categorical idea than Haskell's functors by virtue of having the same domain and codomain: Hask -> Hask. I think applicability of Haskell monads beyond sequencing computation, and the validity of their definition, would be much more clear if someone explained the meaning of adjoint functors to and from Hask. In other words, provide the mathematical characterization to make Haskell monads a precise representation of categorical monads on Hask. 2. Functors are structure preserving maps in the category Cat. The Haskell Functor class represents structure preserving maps in the category Hask, which seem to me more like the categorical notion of arrows or the algebraic notion of homomorphisms. If we talk about functors relating to Haskell, it seems more likely we'd be referring to functors to or from the category Hask than functions (or arrows or whatever) between elements of Hask. Maybe categorical functors are useful as an abstract characterization of programs themselves: a program defines a functor from the problem domain into Hask, or from Hask into output in a problem domain. The name "Arrow" is already taken; what about renaming Functor to Automorphism? 3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing. My guess is that the concept of Hask is too murky to be any use right now. The documentation may be more clear by avoiding it until we work out a formal definition... or is there one already? - Aaron Altman
On Wed, 2008-01-30 at 16:23 -0800, aaltman@pdx.edu wrote:
Category theory seems to have an inconsistent relationship to Haskell - both documentation and the language's implementations of categorical concepts. I come from a math background that makes the Haskell's tight coupling to its mathematical foundation very appealing. But, I may have found some inconsistencies. Whether you agree or not I hope we can get some discussion going that will clarify the wikibooks, etc.
My issues: 1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship
1. Categorical monads are a class of functors, that is, morphisms on Cat. Haskell's monads are at least a bit closer to the categorical idea than Haskell's functors by virtue of having the same domain and codomain: Hask -> Hask. I think applicability of Haskell monads beyond sequencing computation, and the validity of their definition, would be much more clear if someone explained the meaning of adjoint functors to and from Hask. In other words, provide the mathematical characterization to make Haskell monads a precise representation of categorical monads on Hask.
Adjunctions and monads are related, but you don't have to talk about adjunctions to talk about monads. There are potentially multiple adjunctions that correspond to a monad. At any rate, the definitions for adjunction and monad aren't dependent on the category. Once you create a suitable Hask category (which takes some fudging or a bit of care), the meaning of "monad" and "adjunction" are clear. Given a reasonable Hask category, Haskell Monads are categorical monads if they satisfy the monad laws. Haskell does not enforce those laws, but otherwise, Haskell monads are monads.
2. Functors are structure preserving maps in the category Cat. The Haskell Functor class represents structure preserving maps in the category Hask, which seem to me more like the categorical notion of arrows or the algebraic notion of homomorphisms. If we talk about functors relating to Haskell, it seems more likely we'd be referring to functors to or from the category Hask than functions (or arrows or whatever) between elements of Hask. Maybe categorical functors are useful as an abstract characterization of programs themselves: a program defines a functor from the problem domain into Hask, or from Hask into output in a problem domain. The name "Arrow" is already taken; what about renaming Functor to Automorphism?
If you view Hask as a category of Haskell types and Haskell functions, then a type constructor is the object mapping of a functor (possibly, co-, contra-, in-, free-variant). The Functor type class singles out those that are covariant functors in their last type argument, except again, Haskell doesn't enforce the functor laws. Haskell Functors and Monads do not capture the general notion of functor and monad, they only deal with the special case of strong (endo)functors from Hask -> Hask.
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing.
The name "Arrow" is in reference to categorical arrows, but isn't trying to be categorical arrows. Haskell Arrows correspond to Freyd categories. The correspondence is pretty direct and intuitive.
My guess is that the concept of Hask is too murky to be any use right now. The documentation may be more clear by avoiding it until we work out a formal definition... or is there one already?
An accurate Hask category takes some care to define, but it isn't conceptually murky.
1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship
I'm confused. It seems for me that either I don't understand math or I don't understand you.
1. Categorical monads are a class of functors, that is, morphisms on Cat. Haskell's monads are at least a bit closer to the categorical idea than Haskell's functors by virtue of having the same domain and codomain: Hask -> Hask. I think applicability of Haskell monads beyond sequencing computation, and the validity of their definition, would be much more clear if someone explained the meaning of adjoint functors to and from Hask. In other words, provide the mathematical characterization to make Haskell monads a precise representation of categorical monads on Hask.
Well, Haskell monad, you know, consists of three parts: 1) a map m:Ob(Hask) -> Ob(Hask) (by Ob I mean the class of objects of a category); 2) a morphism X -> m(X) for all X's, and 3) a map from Hask(X,m(Y)) to Hask(m(X),m(Y)) - that is, from the set of morphisms X-
m(Y) to the set of morphisms m(X)->m(Y) - for all X's and Y's. That is, I believe, what's called a 'Kleisli triple' in math; it's well known that Kleisli triples are equivalent to monads (in mathematical sense).
2. Functors are structure preserving maps in the category Cat. The Haskell Functor class represents structure preserving maps in the category Hask
What do you mean? A Haskell Functor, first of all, maps types to types - that is, objects of Hask to objects of Hask. Therefore, it becomes a math functor from Hask to Hask.
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain?
Of course not. They have Haskell objects as domains and codomains. I mean, by defining an Arrow class, you really define another category, which has the same objects as Hask, but different morphisms (arrows).
Or is one particular element in Hask its domain and possibly another its codomain?
What do you mean by 'element in Hask'? Hask is a category, it has objects, it has morphisms (arrows), but elements?
I assume you have read the references in http://www.haskell.org/haskellwiki/Research_papers/Monads_and_arrows The penultimate sentence in question 1 below (role of adjoint functors in Haskell monads) was addressed by David Menendez in a recent post to this list: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036361.html There was discussion of Category theory monad <----> Haskell monad subsequent to the thread http://www.haskell.org/pipermail/haskell-cafe/2005-August/011021.html A categorical approach to graph transformations with Haskell is described in: http://philippsen.com/Personen/schneide/gtbook/appendix-a.pdf?language=de There are several Haskell modules (named e.g. Category) floating around that attempt to better reflect categorical usage in Haskell, but I do not have a reference handy. Dan aaltman@pdx.edu wrote:
Category theory seems to have an inconsistent relationship to Haskell - both documentation and the language's implementations of categorical concepts. I come from a math background that makes the Haskell's tight coupling to its mathematical foundation very appealing. But, I may have found some inconsistencies. Whether you agree or not I hope we can get some discussion going that will clarify the wikibooks, etc.
My issues: 1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship
1. Categorical monads are a class of functors, that is, morphisms on Cat. Haskell's monads are at least a bit closer to the categorical idea than Haskell's functors by virtue of having the same domain and codomain: Hask -> Hask. I think applicability of Haskell monads beyond sequencing computation, and the validity of their definition, would be much more clear if someone explained the meaning of adjoint functors to and from Hask. In other words, provide the mathematical characterization to make Haskell monads a precise representation of categorical monads on Hask.
2. Functors are structure preserving maps in the category Cat. The Haskell Functor class represents structure preserving maps in the category Hask, which seem to me more like the categorical notion of arrows or the algebraic notion of homomorphisms. If we talk about functors relating to Haskell, it seems more likely we'd be referring to functors to or from the category Hask than functions (or arrows or whatever) between elements of Hask. Maybe categorical functors are useful as an abstract characterization of programs themselves: a program defines a functor from the problem domain into Hask, or from Hask into output in a problem domain. The name "Arrow" is already taken; what about renaming Functor to Automorphism?
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing.
My guess is that the concept of Hask is too murky to be any use right now. The documentation may be more clear by avoiding it until we work out a formal definition... or is there one already?
- Aaron Altman
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
David's post looks like it has cleared up what I was wondering about. I think it was the specific contents of Ob(Hask) and Haskell functions as arrows in Hask that I was unclear on. With that in mind I understand and agree with Miguel's explanations. Thanks, guys. Dan Weston wrote:
I assume you have read the references in http://www.haskell.org/haskellwiki/Research_papers/Monads_and_arrows
The penultimate sentence in question 1 below (role of adjoint functors in Haskell monads) was addressed by David Menendez in a recent post to this list:
http://www.haskell.org/pipermail/haskell-cafe/2007-December/036361.html
There was discussion of Category theory monad <----> Haskell monad subsequent to the thread
http://www.haskell.org/pipermail/haskell-cafe/2005-August/011021.html
A categorical approach to graph transformations with Haskell is described in:
http://philippsen.com/Personen/schneide/gtbook/appendix-a.pdf?language=de
There are several Haskell modules (named e.g. Category) floating around that attempt to better reflect categorical usage in Haskell, but I do not have a reference handy.
Dan
aaltman@pdx.edu wrote:
Category theory seems to have an inconsistent relationship to Haskell - both documentation and the language's implementations of categorical concepts. I come from a math background that makes the Haskell's tight coupling to its mathematical foundation very appealing. But, I may have found some inconsistencies. Whether you agree or not I hope we can get some discussion going that will clarify the wikibooks, etc.
My issues: 1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship
1. Categorical monads are a class of functors, that is, morphisms on Cat. Haskell's monads are at least a bit closer to the categorical idea than Haskell's functors by virtue of having the same domain and codomain: Hask -> Hask. I think applicability of Haskell monads beyond sequencing computation, and the validity of their definition, would be much more clear if someone explained the meaning of adjoint functors to and from Hask. In other words, provide the mathematical characterization to make Haskell monads a precise representation of categorical monads on Hask.
2. Functors are structure preserving maps in the category Cat. The Haskell Functor class represents structure preserving maps in the category Hask, which seem to me more like the categorical notion of arrows or the algebraic notion of homomorphisms. If we talk about functors relating to Haskell, it seems more likely we'd be referring to functors to or from the category Hask than functions (or arrows or whatever) between elements of Hask. Maybe categorical functors are useful as an abstract characterization of programs themselves: a program defines a functor from the problem domain into Hask, or from Hask into output in a problem domain. The name "Arrow" is already taken; what about renaming Functor to Automorphism?
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing.
My guess is that the concept of Hask is too murky to be any use right now. The documentation may be more clear by avoiding it until we work out a formal definition... or is there one already?
- Aaron Altman
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
aaltman wrote:
My issues: 1. Are Haskell monads useful in a truly categorical sense? 2. Is Haskell's functor class misnamed? 3. Haskell arrows and Haskell monads have a misleading relationship
1.+2. The stumbling block is probably that Hask has exponentials and polymorphism. Hence, all morphisms and even natural transformations can/are internalized, i.e. they are objects in Haskell themselves. 2. The Functor class is for endofunctors only. 3. Arrows depart from Functor and Monad by giving rise to categories different from Hask. In other words, while morphisms and objects are both objects of Hask, the morphisms are not longer plain functions. A simple example (not of Arrows but of the "not a subcategory of Hask" phenomenon) is class Category hom where id :: hom a a (.) :: hom b c -> hom a b -> hom a c newtype Monoid m => Mon m a b = Mon m instance Monoid m => Category (Mon m) where id = Mon mempty (Mon f) . (Mon g) = Mon (f `mappend` g) Regards, apfelmus
Am 31.01.2008 um 01:23 schrieb aaltman@pdx.edu:
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing.
Without being able to dive into this matter now, I just want to say that both the Haskell monads and arrows can be generalized to something I call a "thrist", which appears to be the moral equivalent of a free category. The underlying category is obtained by a two-parameter GADT (defining the morphisms) and the domains and codomains of its members (which are Haskell types) being the objects. Here is my blog entry that motivates the concept a bit: http://heisenbug.blogspot.com/2007/11/trendy-topics.html Cheers, Gabor
Even though you cannot "dive into this matter now", maybe when you get time you can update your blog with an explicit embedding of Haskell monads and arrows in your Thrist construction. Concrete examples will help me (and probably others) more quickly see the novelty, increased generality, and usefulness of a Thrist. Also, although you say that thrists are the moral equivalent of a free category, it appears (at least to me) possible that the first Thrist argument enables the construction of a restricted domain monad, e.g. (Eq a => Set a) monad. Is this so? Dan Gabor Greif wrote:
Am 31.01.2008 um 01:23 schrieb aaltman@pdx.edu mailto:aaltman@pdx.edu:
3. I believe the documentation stating that Haskell arrows are a generalization of Haskell monads, but arrows are a categorical thing too and in that context bear a much more distant relationship to monads. Does a Haskell arrow have Hask as domain and codomain? Or is one particular element in Hask its domain and possibly another its codomain? Those are not at all the same thing.
Without being able to dive into this matter now, I just want to say that both the Haskell monads and arrows can be generalized to something I call a "thrist", which appears to be the moral equivalent of a free category. The underlying category is obtained by a two-parameter GADT (defining the morphisms) and the domains and codomains of its members (which are Haskell types) being the objects.
Here is my blog entry that motivates the concept a bit:
http://heisenbug.blogspot.com/2007/11/trendy-topics.html
Cheers,
Gabor
------------------------------------------------------------------------
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Am 31.01.2008 um 18:13 schrieb Dan Weston:
Even though you cannot "dive into this matter now", maybe when you get time you can update your blog with an explicit embedding of Haskell monads and arrows in your Thrist construction. Concrete examples will help me (and probably others) more quickly see the novelty, increased generality, and usefulness of a Thrist.
Okay, I took my time and came up with: http://heisenbug.blogspot.com/2008/01/embeddings-part-one-arrow- thrist.html Comments welcome.
Also, although you say that thrists are the moral equivalent of a free category, it appears (at least to me) possible that the first Thrist argument enables the construction of a restricted domain monad, e.g. (Eq a => Set a) monad. Is this so?
Hmmm, not sure what you asking for. If you have a monad instance Set a that has Eq a attached, this already would do what you want, no? An example would help me to understand...
Dan
Cheers, Gabor
Hmmm, not sure what you asking for. If you have a monad instance Set a that has Eq a attached, this already would do what you want, no? An example would help me to understand...
Sorry, I meant uppercase (and got the constraint wrong anyway). I meant that Ord a => Set a was a monad (lowercase 'm') under the obvious semantics, but cannot be an instance of Monad. The type signature of Haskell's Monad class is too free (admits too many types, not just Ord a => a) to have a Set instance. [But for solutions, see http://www.randomhacks.net/articles/2007/03/15/data-set-monad-haskell-macros http://okmij.org/ftp/Haskell/types.html#restricted-datatypes http://hackage.haskell.org/packages/archive/monad-param/0.0.2/doc/html/Contr... ] I was just wondering if your Thrist type constructor included (e.g. in its first argument) a mechanism for embedding a Set monad, since this is already a subject of some interest to many people. Dan Gabor Greif wrote:
Am 31.01.2008 um 18:13 schrieb Dan Weston:
Even though you cannot "dive into this matter now", maybe when you get time you can update your blog with an explicit embedding of Haskell monads and arrows in your Thrist construction. Concrete examples will help me (and probably others) more quickly see the novelty, increased generality, and usefulness of a Thrist.
Okay, I took my time and came up with:
http://heisenbug.blogspot.com/2008/01/embeddings-part-one-arrow-thrist.html
Comments welcome.
Also, although you say that thrists are the moral equivalent of a free category, it appears (at least to me) possible that the first Thrist argument enables the construction of a restricted domain monad, e.g. (Eq a => Set a) monad. Is this so?
Hmmm, not sure what you asking for. If you have a monad instance Set a that has Eq a attached, this already would do what you want, no? An example would help me to understand...
Dan
Cheers,
Gabor
participants (7)
-
aaltman＠pdx.edu -
Aaron Altman
-
apfelmus -
Dan Weston -
Derek Elkins -
Gabor Greif -
Miguel Mitrofanov