From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id B0064BBCA for ; Thu, 28 Feb 2008 01:26:24 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPGNxUfUGyojkWdsb2JhbACQaAEBAQEHAggJCBidRQ X-IronPort-AV: E=Sophos;i="4.25,416,1199660400"; d="scan'208";a="8688264" Received: from smtp5-g19.free.fr ([212.27.42.35]) by mail1-smtp-roc.national.inria.fr with ESMTP; 28 Feb 2008 01:26:24 +0100 Received: from smtp5-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp5-g19.free.fr (Postfix) with ESMTP id EF14A387F24; Wed, 27 Feb 2008 23:33:36 +0100 (CET) Received: from [192.168.0.63] (ron34-3-82-236-236-194.fbx.proxad.net [82.236.236.194]) by smtp5-g19.free.fr (Postfix) with ESMTP id D586D38226E; Wed, 27 Feb 2008 21:15:33 +0100 (CET) Subject: Re: [Caml-list] Categories for types From: =?ISO-8859-1?Q?Micha=EBl_Gr=FCnewald?= To: Pierre-Evariste Dagand Cc: caml-list@yquem.inria.fr In-Reply-To: <6cb897b30802270619p44a07d7bpefb081eaf14ea4d2@mail.gmail.com> References: <1204103280.10964.16.camel@Llea.celt.neu> <6cb897b30802270619p44a07d7bpefb081eaf14ea4d2@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-15 Date: Wed, 27 Feb 2008 21:16:04 +0100 Message-Id: <1204143364.1724.6.camel@Llea.celt.neu> Mime-Version: 1.0 X-Mailer: Evolution 2.12.3 FreeBSD GNOME Team Port Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; 0100,:01 lambda:01 developping:01 pointers:01 anna:98 caml-list:01 benjamin:01 pierce:02 pierce:02 intuitions:03 languages:03 programming:03 logic:04 suggests:04 types:05 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.