Thank you Alexander for the reply. My wondering is: is Hask a category created by Haskell researchers or was something already present in literature? Cheers, A. On 13 January 2013 17:44, Alexander Solla wrote:

There was a conversation on the cafe about this last month. Check out:

https://groups.google.com/forum/#!topic/haskell-cafe/tBO2AowUvMY

Category theory is a "language" of composition. In "logical" terms, different categories are models of different axioms. That said, a "rich enough" category is suitable for encoding the "whole" of category theory (as a language -- not necessarily as a model containing sub-models. Typing introduces some complications, since types meant to help us escape logical paradoxes like Russell's by introducing a notion of "foundedness")

Hask is the category whose objects are types and whose morphisms are Haskell functions.

Hask is a very rich category, and is suitable for encoding a lot (but not all) of category theory. As far as I know, the actual boundary is as yet unknown.

On Sun, Jan 13, 2013 at 4:15 AM, Alfredo Di Napoli < alfredo.dinapoli@gmail.com> wrote:

...

Morning Cafe,

I'm planning to do a series of write-ups about Category Theory, to publish them on the company's blog I'm currently employed. I'm not a CT expert, but since the best way to learn something is to explain it to others, I want to take a shot :) In my mind I will structure the posts following Awodey's book, but I'm wondering how can I make my posts a little more "real world". I always read about the "Hask category", which seems to be the "bootstrap" of the whole logic behind Haskell. Can you please give my materials/papers/links/blogs to the Hask category and briefly explain me how it relates to Category Theory and Haskell itself?

I hope my question is clear enough, in case is not, I'll restate :P

Cheers, A.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 1/13/13 12:44 PM, Alexander Solla wrote:

Hask is a very rich category, and is suitable for encoding a lot (but not all) of category theory. As far as I know, the actual boundary is as yet unknown.

I'm not sure that's the most appropriate way to render things. In general, rich categories like CCCs and Toposes are "good places" to do mathematics. This means that we can translate the bulk of mathematics into those settings--- where mathematics means the study of particular structures like rings, groups, vector spaces, etc. These rich categories also provide a good place to do logic/lambda-calculi; from which we get the idea of categorifying Haskell and seeing where that leads us (i.e., asking what Hask looks like). However, standard category theory does not provide a good place for doing category theory. In order to provide a good place for doing category theory, people move on to enriched CT and higher CT[1]. HCT is about coming up with category theoretic definitions for things like co/limits, adjunctions, etc, while moving away from the set theoretic notions inherited from the original conceptions of these terms. In other words, HCT is a good place for doing *meta*mathematics (and metalogic). While there are apparent similarities, there are big differences between doing mathematics and doing metamathematics, and one should be careful not to get them confused. Asking what Haskell looks like when viewed from CT is very different than asking what portions of CT we can implement in Haskell. Haskell is a great place for doing mathematics, but I'm wary of how good it is for doing metamathematics; we conflate too many things which should be kept distinct (e.g., morphisms vs exponentials) and we fail to monitor the boundary between object and meta languages (e.g., a morphism in a category vs a mapping as described in the language of category theory). [1] For more discussion on this point, see n-Lab and n-Cafe: http://ncatlab.org/ http://golem.ph.utexas.edu/category/ -- Live well, ~wren