[TYPES] Book on Category Theory

Wed Nov 1 10:37:53 EDT 2017

Thank you for all the suggestions I have ordered yet another book on
category theory Lavere's - Conceptual Mathematics: A First Introduction to
Categories
<https://www.amazon.co.uk/gp/product/052171916X/ref=oh_aui_detailpage_o01_s00?ie=UTF8&psc=1>
, and am going to follow Steve Awodey's Category Theory Foundations,
Lectures on YouTube :-

    https://www.youtube.com/user/p473r/search?query=Category+Theory

I have found what I was looking for now regarding the different types of
morphisms so am posting links to the two papers here so other following the
thread and are interested can have the references.

Graham Hutton's - Bananas in space: extending fold and unfold to
exponential types :-

    http://www.cs.nott.ac.uk/~pszgmh/bib.html#bananas

Revisiting Catamorphisms over Datatypes with Embedded Functions :-

    https://lambda.uta.edu/popl96.pdf

These give good extended material to understand applications for algebraic
data types, recursive datatypes and datatypes containing functionality.

For those who don't know what I am working on and the strange angle I came
from I am outside of acedemia I came across the need to understand type
theory in order to specify and implement my own object oriented language
SOOL which is hopefully going to be a staticly typed feature complete
orthoganally complete Object Oriented Language, with meta and grammatical
extensions (hence the interest in cata and ana morphisms).

Kind regards,

Aaron

On 1 November 2017 at 02:11, Aaron Gray <aaronngray.lists at gmail.com> wrote:

> Hi Gabrel,
>
> Congratulations on becoming moderator I have had a look at your homepage
> and your work looks very interesting. I need to read your GADT's and
> subtyping paper as this is an area I have avoided looking at due to their
> inter-complexity.
>
> Sorry I have not really responded properly on the list it takes me a long
> time to digest things and am currently still learning what is very complex
> ground. I do find I understand things when they are very well formulated
> this is often in founding papers or in disseminations of them.
>
> Thank you for all the suggestions I have ordered yet another book on
> category theory Lavere's - Conceptual Mathematics: A First Introduction
> to Categories
> <https://www.amazon.co.uk/gp/product/052171916X/ref=oh_aui_detailpage_o01_s00?ie=UTF8&psc=1>
> , and am going to follow Steve Awodey's Category Theory Foundations,
> Lectures on YouTube :-
>
>     https://www.youtube.com/user/p473r/search?query=Category+Theory
>
> I have found what I was looking for now regarding the different types of
> morphisms so am posting links to the two papers here so other following the
> thread and are interested can have the references.
>
> Graham Hutton's - Bananas in space: extending fold and unfold to
> exponential types :-
>
>     http://www.cs.nott.ac.uk/~pszgmh/bib.html#bananas
>
> Revisiting Catamorphisms over Datatypes with Embedded Functions :-
>
>     https://lambda.uta.edu/popl96.pdf
>
> These give good extended matterial to understand the area for recursive
> datatypes and datatypes containing functionality.
>
> For those who don't know what I am working on and the strange angle I came
> from I am outside of acedemia I came across the need to understand type
> theory in order to specify and implement my own object oriented language
> SOOL which is hopefully going to be a staticly typed feature complete
> orthoganally complete Object Oriented Language, with meta and grammatical
> extensions (hence the interest in cata and ana morphisms).
>
> Kind regards,
>
> Aaron
>
>
> On 24 October 2017 at 08:22, Gabriel Scherer <gabriel.scherer at gmail.com>
> wrote:
>
>> Hi Aaron,
>>
>> I think you may misunderstand what "category theory for type theory" is
>> about and its focus area. It is perfectly natural for an outsider to be a
>> bit confused about the topic you want to learn about (that's the point of
>> learning), but my impression is that you have some work to do find out what
>> you actually want before you can usefully tap types-list as a direct
>> citation source. Maybe some people around here can help you do this
>> unraveling work (Sean Leather's last reference seems to go in the same
>> direction), but otherwise there are other places where people may be more
>> knowledgeable about orienting people living in the gap between "category
>> theory keywords I hear when I hang around Haskellers" and "category theory
>> books", for example https://www.reddit.com/r/haskell/ .
>>
>> (Reverse engineering what you say, it also sounds like Bartosz Milewski's
>> book mentioned by François Thiré above may be one of the closer to what you
>> are looking for.)
>>
>> On Mon, Oct 23, 2017 at 4:56 PM, Aaron Gray <aaronngray.lists at gmail.com>
>> wrote:
>>
>>> [ The Types Forum, http://lists.seas.upenn.edu/ma
>>> ilman/listinfo/types-list ]
>>>
>>> Thanks everyone, but as far as I can tell none of these books give me any
>>> real stuff on covariance, contravariance, anamophisms and catamophisms.
>>>
>>> On 19 October 2017 at 16:59, John Leo <leo at halfaya.org> wrote:
>>>
>>> > I agree Pierce's book is great, and my favorite overall reference
>>> Awodey
>>> > also has some material on applications to type theory.
>>> >
>>> > For specific connections, the best sources are probably lecture notes
>>> for
>>> > various summer school courses.  My three favorites are those in the
>>> > "Category Theory and Functional Programming" section of this page:
>>> > https://github.com/halfaya/BayHac/blob/master/references.md
>>> >
>>> > John
>>> >
>>> >
>>> >
>>> > On Thu, Oct 19, 2017 at 2:50 AM, Moez A. AbdelGawad <moez at cs.rice.edu>
>>> > wrote:
>>> >
>>> >> [ The Types Forum, http://lists.seas.upenn.edu/ma
>>> >> ilman/listinfo/types-list ]
>>> >>
>>> >> In addition to Pierce's book, which was earlier mentioned, I strongly
>>> >> recommend Spivak's Category Theory for The Sciences and Lawvere &
>>> >> Schanuel's Conceptual Mathematics. Even though neither book is
>>> specifically
>>> >> for computer scientists, but both books are more modern, very
>>> accessible,
>>> >> and frequently discuss CS applications.
>>> >>
>>> >> -Moez
>>> >>
>>> >> -------- Original message --------
>>> >> From: Aaron Gray <aaronngray.lists at gmail.com>
>>> >> Date: 18/10/2017  21:22  (GMT+02:00)
>>> >> To: The TYPES forum <types-list at lists.seas.upenn.edu>
>>> >> Subject: [TYPES] Book on Category Theory
>>> >>
>>> >> [ The Types Forum, http://lists.seas.upenn.edu/ma
>>> >> ilman/listinfo/types-list ]
>>> >>
>>> >> I am looking for a book on Category Theory that is ideally either
>>> aimed at
>>> >> Type Theory or has the relevant topics to support the area.
>>> >>
>>> >> I have bought three books on the topic so far, one 'Categories for
>>> Typesw'
>>> >> by Crole did not even cover covariance and contravariance.I would also
>>> >> like
>>> >> coverage of monoid and monads, and morphisms like anamorphisms and
>>> >> catamorphisms.
>>> >>
>>> >> I am also interested in papers applying category theory to areas of
>>> type
>>> >> theory.
>>> >>
>>> >> Suggestions of either online or printed material would be appreciated.
>>> >>
>>> >> Many tahnks in advance,
>>> >> --
>>> >> Aaron Gray
>>> >>
>>> >> Independent Open Source Software Engineer, Computer Language
>>> Researcher,
>>> >> Information Theorist, and amateur computer scientist.
>>> >>
>>> >
>>> >
>>>
>>>
>>> --
>>> Aaron Gray
>>>
>>> Independent Open Source Software Engineer, Computer Language Researcher,
>>> Information Theorist, and amateur computer scientist.
>>>
>>
>>
>
>
> --
> Aaron Gray
>
> Independent Open Source Software Engineer, Computer Language Researcher,
> Information Theorist, and amateur computer scientist.
>

-- 
Aaron Gray

Independent Open Source Software Engineer, Computer Language Researcher,
Information Theorist, and amateur computer scientist.