Alfredo Di Napoli | 13 Jan 13:15 2013
Picon

Where is the "convergence point" between Category Theory and Haskell?

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alexander Solla | 13 Jan 18:44 2013
Picon

Re: Where is the "convergence point" between Category Theory and Haskell?

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


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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alfredo Di Napoli | 13 Jan 19:53 2013
Picon

Re: Where is the "convergence point" between Category Theory and Haskell?

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 <alex.solla <at> gmail.com> wrote:
There was a conversation on the cafe about this last month.  Check out:


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 <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
wren ng thornton | 14 Jan 00:18 2013

Re: Where is the "convergence point" between Category Theory and Haskell?

On 1/13/13 1:53 PM, Alfredo Di Napoli wrote:
> Thank you Alexander for the reply.
> My wondering is: is Hask a category created by Haskell researchers or was
> something already present in literature?

Hask was created by Haskellers in discussions on blogs etc. If one is 
being particular about the details, it's not clear that Haskell types 
and functions actually do form a category of interest, let alone one 
with the properties commonly attributed to Hask (e.g., Cartesian 
closedness). One of the big problems is how laziness/bottoms are treated 
(e.g., eta-conversion does not hold in general).

Thus, I'm not sure it's ever been discussed in the literature; it's more 
a helpful fiction than a legitimate mathematical object.

--

-- 
Live well,
~wren
wren ng thornton | 14 Jan 00:12 2013

Re: Where is the "convergence point" between Category Theory and Haskell?

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
Aleksandar Dimitrov | 14 Jan 09:42 2013
Picon

Re: Where is the "convergence point" between Category Theory and Haskell?

> [1] For more discussion on this point, see n-Lab and n-Cafe:
> 
>     http://ncatlab.org/
>     http://golem.ph.utexas.edu/category/

Wren, thanks very much for these two links. I've been trying for forever to get
a foot into metamathematics and type theory in particular (not having the option
of actually taking any university grade classes on the subject,) and I think
these two links shall prove very helpful. In particular, I already like at least
two posts of the blog very much, and am continuing to scavenge the archives :-).

Regards,
Aleks
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Christopher Howard | 14 Jan 00:43 2013

Re: Where is the "convergence point" between Category Theory and Haskell?

On 01/13/2013 03:15 AM, Alfredo Di Napoli 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.
> 
> 

You want to give us the link to that blog?

If you can keep your explanations reasonably illustrative and easy to
understand, you'll get a regular reader out of me.

--

-- 
frigidcode.com

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alfredo Di Napoli | 14 Jan 09:37 2013
Picon

Re: Where is the "convergence point" between Category Theory and Haskell?

Thanks everyone for the answers. Mine is just an experiment, but if I succeed in keeping it

up and to come with something useful, I won't hesitate to poke you :)
Btw, in case I succeed, posts will appear here:


and here:


Bye,
Alfredo

On 13 January 2013 23:43, Christopher Howard <christopher.howard <at> frigidcode.com> wrote:
On 01/13/2013 03:15 AM, Alfredo Di Napoli 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.
>
>

You want to give us the link to that blog?

If you can keep your explanations reasonably illustrative and easy to
understand, you'll get a regular reader out of me.

--
frigidcode.com


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


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

Gmane