Difference between revisions of "Category theory"

From HaskellWiki
Jump to navigation Jump to search
m
 
(10 intermediate revisions by 4 users not shown)
Line 69: Line 69:
   
 
Catamorphisms and related concepts, categorical approach to functional programming, categorical programming. Many materials cited here refer to category theory, so as an introduction to this discipline see the [[#See also]] section.
 
Catamorphisms and related concepts, categorical approach to functional programming, categorical programming. Many materials cited here refer to category theory, so as an introduction to this discipline see the [[#See also]] section.
* Erik Meijer, Maarten Fokkinga, Ross Paterson: [http://research.microsoft.com/en-us/um/people/emeijer/Papers/fpca91.pdf Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire]. See also related documents (in the CiteSeer page). Understanding the article does not require knowledge of category theory—the paper is self-contained with regard to understanding catamorphisms, anamorphisms and other related concepts.
+
* Erik Meijer, Maarten Fokkinga, Ross Paterson: [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.125 Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire]. See also related documents (in the CiteSeer page). Understanding the article does not require knowledge of category theory—the paper is self-contained with regard to understanding catamorphisms, anamorphisms and other related concepts.
 
* Roland Backhouse, Patrik Jansson, Johan Jeuring and Lambert Mertens. [http://www.cse.chalmers.se/~patrikj/poly/afp98/ Generic Programming - an Introduction]: Detailed introduction to categorial sums, product, polynomial functors and folds for the purpose of generic programming. Supplements the bananas paper.
 
* Roland Backhouse, Patrik Jansson, Johan Jeuring and Lambert Mertens. [http://www.cse.chalmers.se/~patrikj/poly/afp98/ Generic Programming - an Introduction]: Detailed introduction to categorial sums, product, polynomial functors and folds for the purpose of generic programming. Supplements the bananas paper.
 
* Varmo Vene and Tarmo Uustalu: [http://citeseer.ist.psu.edu/vene98functional.html Functional Programming with Apomorphisms / Corecursion]
 
* Varmo Vene and Tarmo Uustalu: [http://citeseer.ist.psu.edu/vene98functional.html Functional Programming with Apomorphisms / Corecursion]
 
* Varmo Vene: [http://www.cs.ut.ee/~varmo/papers/thesis.pdf Categorical Programming with Inductive and Coinductive Types]. The book gives Haskell examples to illustrate the deep categorical theory topic.
 
* Varmo Vene: [http://www.cs.ut.ee/~varmo/papers/thesis.pdf Categorical Programming with Inductive and Coinductive Types]. The book gives Haskell examples to illustrate the deep categorical theory topic.
* Tatsuya Hagino: [http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf A Categorical Programming Language]
+
* Tatsuya Hagino: [http://web.sfc.keio.ac.jp/~hagino/thesis.pdf A Categorical Programming Language]
 
* [http://pll.cpsc.ucalgary.ca/charity1/www/home.html Charity], a categorical programming language implementation.
 
* [http://pll.cpsc.ucalgary.ca/charity1/www/home.html Charity], a categorical programming language implementation.
 
* [http://okmij.org/ftp/Haskell/categorical-maxn.lhs Deeply uncurried products, as categorists might like them] article mentions a conjecture: relatedness to [[Combinatory logic]]
 
* [http://okmij.org/ftp/Haskell/categorical-maxn.lhs Deeply uncurried products, as categorists might like them] article mentions a conjecture: relatedness to [[Combinatory logic]]
Line 79: Line 79:
 
==Haskell libraries and tools==
 
==Haskell libraries and tools==
   
  +
* Originally, there was a package, [http://www.eyrie.org/~zednenem/2004/hsce/ Category extras], by [http://www.eyrie.org/~zednenem/about/dave.html David Menendez]: libraries for e.g. functors, bifunctors, comonads, natural transformations, adjunctions and infinite data types. This package has been superseded by other more-focused and self-contained packages, as documented in the [http://hackage.haskell.org/package/category-extras category-extras] metapackage in Hackage. Almost all of them (e.g. [http://hackage.haskell.org/package/comonad comonad], [http://hackage.haskell.org/package/bifunctors bifunctors], [http://hackage.haskell.org/package/categories categories], [http://hackage.haskell.org/package/adjunctions adjunctions], [http://hackage.haskell.org/package/contravariant contravariant], [http://hackage.haskell.org/package/free free], [http://hackage.haskell.org/package/profunctors profunctors], [http://hackage.haskell.org/package/distributive distributive], [http://hackage.haskell.org/package/semigroupoids semigroupoids], [http://hackage.haskell.org/package/kan-extensions kan-extensions], [http://hackage.haskell.org/package/recursion-schemes recursion-schemes]) are done by [http://hackage.haskell.org/user/EdwardKmett Edward A. Kmett].
* [http://www.eyrie.org/~zednenem/2004/hsce/ Category extras] by [http://www.eyrie.org/~zednenem/about/dave.html David Menendez]: libraries for e.g. comonads, infinite data types.
 
  +
  +
* Notable other encoding of category theory is [http://hackage.haskell.org/package/data-category data-category] by [http://hackage.haskell.org/user/SjoerdVisscher Sjoerd Visscher].
   
 
==Books==
 
==Books==
   
  +
* [https://www.schoolofhaskell.com/user/bartosz Bartosz Milewski] Category Theory for Programmers. Series of [https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ blog posts] turned into [https://github.com/hmemcpy/milewski-ctfp-pdf a book]. Covers many abstractions and constructions starting from basics: category, functor up to kan extensions, topos, enriched categories, F-algebras. There are video recordings with those content: [https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ part 1], [https://www.youtube.com/watch?v=3XTQSx1A3x8&list=PLbgaMIhjbmElia1eCEZNvsVscFef9m0dm part II] and [https://www.youtube.com/watch?v=F5uEpKwHqdk&list=PLbgaMIhjbmEn64WVX4B08B4h2rOtueWIL part III].
*Michael Barr and Charles Wells: [http://www.cwru.edu/artsci/math/wells/pub/ttt.html Toposes, Triples and Theories]. The online, freely available book is both an introductory and a detailed description of category theory. It also contains a category-theoretical description of the concept of ''monad'' (but calling it a ''triple'' instead of ''monad'').
 
   
 
* Michael Barr and Charles Wells: [http://www.tac.mta.ca/tac/reprints/articles/12/tr12abs.html Toposes, Triples and Theories]. The online, freely available book is both an introductory and a detailed description of category theory. It also contains a category-theoretical description of the concept of ''monad'' (but calling it a ''triple'' instead of ''monad'').
*R. F. C. Walters: [http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=0521419972 Categories and Computer Science]. Category Theory has, in recent years, become increasingly important and popular in computer science, and many universities now introduce Category Theory as part of the curriculum for undergraduate computer science students. Here, the theory is developed in a straightforward way, and is enriched with many examples from computer science.
 
  +
 
* R. F. C. Walters: [http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=0521419972 Categories and Computer Science]. Category Theory has, in recent years, become increasingly important and popular in computer science, and many universities now introduce Category Theory as part of the curriculum for undergraduate computer science students. Here, the theory is developed in a straightforward way, and is enriched with many examples from computer science.
   
 
* Arbib&Manes: Arrow, Structures and Functors - The Categorical Imperative. (c)1975 Academic Press, ISBN 0-12-059060-3. Sadly now out of print but very little prerequisite knowledge is needed. It covers monads and the Yoneda lemma.
 
* Arbib&Manes: Arrow, Structures and Functors - The Categorical Imperative. (c)1975 Academic Press, ISBN 0-12-059060-3. Sadly now out of print but very little prerequisite knowledge is needed. It covers monads and the Yoneda lemma.
  +
  +
* Brendan Fong, David I Spivak: [https://arxiv.org/abs/1803.05316 Seven Sketches in Compositionality: An Invitation to Applied Category Theory]. Different exposition to category theory focusing on applications in databases, circuits and signal flows.
  +
  +
* Eugenia Cheng: [https://www.cambridge.org/core/books/joy-of-abstraction/00D9AFD3046A406CB85D1AFF5450E657 The Joy of Abstraction]. An introduction to category theory for anyone who wants to get into the formality of the subject but does not necessarily have the mathematical background to read a standard textbook.
   
 
==See also==
 
==See also==
   
 
* Michael Barr and Charles Wells have a [http://www.math.upatras.gr/~cdrossos/Docs/B-W-LectureNotes.pdf paper] that presents category theory from a computer-science perspective, assuming no prior knowledge of categories.
 
* Michael Barr and Charles Wells have a [http://www.math.upatras.gr/~cdrossos/Docs/B-W-LectureNotes.pdf paper] that presents category theory from a computer-science perspective, assuming no prior knowledge of categories.
*[http://wwwhome.cs.utwente.nl/~fokkinga/mmf92b.html A Gentle Introduction to Category Theory - the calculational approach] written by [http://wwwhome.cs.utwente.nl/~fokkinga/index.html Maarten M Fokkinga].
+
*[https://maartenfokkinga.github.io/utwente/#detail_0000003536 A Gentle Introduction to Category Theory - the calculational approach] written by [https://maartenfokkinga.github.io/utwente/ Maarten M Fokkinga].
 
* Wikipedia has a good [http://en.wikipedia.org/wiki/List_of_category_theory_topics collection of category-theory articles], although, as is typical of Wikipedia articles, they are rather dense.
 
* Wikipedia has a good [http://en.wikipedia.org/wiki/List_of_category_theory_topics collection of category-theory articles], although, as is typical of Wikipedia articles, they are rather dense.
   

Latest revision as of 04:11, 14 February 2023

Haskell theoretical foundations

General:
Mathematics - Category theory
Research - Curry/Howard/Lambek

Lambda calculus:
Alpha conversion - Beta reduction
Eta conversion - Lambda abstraction

Other:
Recursion - Combinatory logic
Chaitin's construction - Turing machine
Relational algebra

Category theory can be helpful in understanding Haskell's type system. There exists a "Haskell category", of which the objects are Haskell types, and the morphisms from types a to b are Haskell functions of type a -> b.

The Haskell wikibooks has an introduction to Category theory, written specifically with Haskell programmers in mind.

Definition of a category

A category consists of two collections:

Ob, the objects of

Ar, the arrows of (which are not the same as Arrows defined in GHC)

Each arrow in Ar has a domain, dom , and a codomain, cod , each chosen from Ob. The notation means is an arrow with domain and codomain . Further, there is a function called composition, such that is defined only when the codomain of is the domain of , and in this case, has the domain of and the codomain of .

In symbols, if and , then .

Also, for each object , there is an arrow , (often simply denoted as or , when there is no chance of confusion).

Axioms

The following axioms must hold for to be a category:

  1. If then (left and right identity)
  2. If and and , then (associativity)

Examples of categories

  • Set, the category of sets and set functions.
  • Mon, the category of monoids and monoid morphisms.
  • Monoids are themselves one-object categories.
  • Grp, the category of groups and group morphisms.
  • Rng, the category of rings and ring morphisms.
  • Grph, the category of graphs and graph morphisms.
  • Top, the category of topological spaces and continuous maps.
  • Preord, the category of preorders and order preserving maps.
  • CPO, the category of complete partial orders and continuous functions.
  • Cat, the category of categories and functors.
  • Hask
  • the category of data types and functions on data structures
  • the category of functions and data flows (~ data flow diagram)
  • the category of stateful objects and dependencies (~ object diagram)
  • the category of values and value constructors
  • the category of states and messages (~ state diagram)

Further definitions

With examples in Haskell at:

Categorical programming

Catamorphisms and related concepts, categorical approach to functional programming, categorical programming. Many materials cited here refer to category theory, so as an introduction to this discipline see the #See also section.

Haskell libraries and tools

Books

  • Bartosz Milewski Category Theory for Programmers. Series of blog posts turned into a book. Covers many abstractions and constructions starting from basics: category, functor up to kan extensions, topos, enriched categories, F-algebras. There are video recordings with those content: part 1, part II and part III.
  • Michael Barr and Charles Wells: Toposes, Triples and Theories. The online, freely available book is both an introductory and a detailed description of category theory. It also contains a category-theoretical description of the concept of monad (but calling it a triple instead of monad).
  • R. F. C. Walters: Categories and Computer Science. Category Theory has, in recent years, become increasingly important and popular in computer science, and many universities now introduce Category Theory as part of the curriculum for undergraduate computer science students. Here, the theory is developed in a straightforward way, and is enriched with many examples from computer science.
  • Arbib&Manes: Arrow, Structures and Functors - The Categorical Imperative. (c)1975 Academic Press, ISBN 0-12-059060-3. Sadly now out of print but very little prerequisite knowledge is needed. It covers monads and the Yoneda lemma.
  • Eugenia Cheng: The Joy of Abstraction. An introduction to category theory for anyone who wants to get into the formality of the subject but does not necessarily have the mathematical background to read a standard textbook.

See also