Categories for types

Categories for types

[Michaël Grünewald]

Dear OCaml folks,

I am an happy OCaml amateur programmer since many years now, and I ever
wondered why the language has ``functors'' --- I was puzzled by the
name.

My curiosity had a renewal when I found this book in the math department
library: Categories for types, by Crole. Before checking the book out, I
would like to know if the term ``functor'' was chosen because they are
actually functors. Maybe someone can also suggests other readings to me.
(I have a strong math education, although I am not used to work with
categories.)
-- 
Cheers,
Michaël

Re: [Caml-list] Categories for types

[Gabriel Kerneis]

[-- Attachment #1: Type: text/plain, Size: 337 bytes --]

Hello,

Le Wed, 27 Feb 2008 10:08:00 +0100, Michaël Grünewald
<michael.grunewald@laposte.net> a écrit :
> Before checking
> the book out, I would like to know if the term ``functor'' was chosen
> because they are actually functors. 

No.

Functors (in Ocaml) are just functions that produce modules.

Regards,
-- 
Gabriel

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: [Caml-list] Categories for types

[Pierre-Evariste Dagand]

>  Maybe someone can also suggests other readings to me.

/!\ Disclaimer /!\

I'm not a category theory guru, it just happened that I had one
lecture on that topic, I'm still trying to understand that field. The
following references come from my teacher.

Feel free to comment this choice / to comment over my comments, I am
eager to learn more about this topic.



This book is a "classic", targeting the use of category theory for
programming languages :

Basic Category Theory for Computer Scientists, Benjamin C. Pierce

It's "understandable", i.e: to be read with a pen and a paper. That's
not a thriller...

Then comes the Crole, Categories for Types. Quite hard to grasp but
hey... that's category theory... Spoiler : at the end, the
hyper-doctrine classify the \omega \lambda theory, I look forward
Season 2 to know how she reacts.

Less computer science oriented, you have :

Conceptual Mathematics: A First Introduction to Categories, Lawvere & Schanuel

This one is very pedestrian, it starts with stones, Anna, Joe and
Richard to end with "higher universal mapping properties". I find it
quite good at developping some intuitions of what all these
thingy-morphisms are, among other thingysm.

On the other hand, you have the H-Bomb :

Categories for the Working Mathematician, Mac Lane

Probably a very good book. But I can't comment it : as soon as I open
it, read a line, I fall asleep. It's a very dense book.

I have also heard a good review of the following :

Category Theory (Oxford Logic Guides),  Steve Awodey

As an intermediate between Mac Lane and Pierce.



Good luck and don't forget to buy a lot of coffee,


-- 
Pierre-Evariste Dagand

Re: [Caml-list] Categories for types

[Michaël Grünewald]

Le Mercredi 27 février 2008 à 14:38 +0100, Gabriel Kerneis a écrit :
> Hello,
> 
> Le Wed, 27 Feb 2008 10:08:00 +0100, Michaël Grünewald
> <michael.grunewald@laposte.net> a écrit :
> > Before checking
> > the book out, I would like to know if the term ``functor'' was chosen
> > because they are actually functors. 
> 
> No.
> 
> Functors (in Ocaml) are just functions that produce modules.

Concise and precise answer! :)
Thank you,
MG

Re: [Caml-list] Categories for types

[Michaël Grünewald]

Le Mercredi 27 février 2008 à 15:19 +0100, Pierre-Evariste Dagand a
écrit :
> >  Maybe someone can also suggests other readings to me.
> 
> /!\ Disclaimer /!\
> 
> I'm not a category theory guru, it just happened that I had one
> lecture on that topic, I'm still trying to understand that field. The
> following references come from my teacher.
> 
> Feel free to comment this choice / to comment over my comments, I am
> eager to learn more about this topic.
> 
> 
> 
> This book is a "classic", targeting the use of category theory for
> programming languages :
> 
> Basic Category Theory for Computer Scientists, Benjamin C. Pierce
> 
> It's "understandable", i.e: to be read with a pen and a paper. That's
> not a thriller...
> 
> Then comes the Crole, Categories for Types. Quite hard to grasp but
> hey... that's category theory... Spoiler : at the end, the
> hyper-doctrine classify the \omega \lambda theory, I look forward
> Season 2 to know how she reacts.
> 
> Less computer science oriented, you have :
> 
> Conceptual Mathematics: A First Introduction to Categories, Lawvere & Schanuel
> 
> This one is very pedestrian, it starts with stones, Anna, Joe and
> Richard to end with "higher universal mapping properties". I find it
> quite good at developping some intuitions of what all these
> thingy-morphisms are, among other thingysm.
> 
> On the other hand, you have the H-Bomb :
> 
> Categories for the Working Mathematician, Mac Lane
> 
> Probably a very good book. But I can't comment it : as soon as I open
> it, read a line, I fall asleep. It's a very dense book.
> 
> I have also heard a good review of the following :
> 
> Category Theory (Oxford Logic Guides),  Steve Awodey
> 
> As an intermediate between Mac Lane and Pierce.
> 
> 
> 
> Good luck and don't forget to buy a lot of coffee,

Thank you for the pointers, I will read the introductions of the books I
manage to find. And yes, I enjoy drinking coffee.

Re: [Caml-list] Categories for types

[Axel Poigné]

Hello

Well, maybe one should not advertise oneself but a long time ago I  
wrote a chapter on "Basic Category Theory" in the Handbook of Logic in  
Computer Science" (Eds. S. Abramsky, D.Gabbay, T.S.E. Maibaum). Basic  
notions of category theory (and somewhat more) are introduced from the  
viewpoint of functional programming (and other applications in  
computer science).
Maybe a bit outdated if you consider developments in linear logic,  
coalbras, and applications of categories in particular in physics (http://categorieslogicphysics.wikidot.com/video 
), but the chapter still may help to understand some of the basic  
concepts from a programmers point of view (for adjunctions some  
familiarity with automata theory is assumed, though - in former times  
standard knowledge in CS).

Regards

Axel

PS. Mildly ignore the mistakes.