This is a scholarly collaboration with @knuton.
This repository will hold our explorations of Arrows both as category theoretic objects and as notions in computation (in particular, in Haskell).
Here is a tentative table of contents:
1. Introduction
.... What is the problem of treating general forms of computation
in pure languages? How does Haskell approach it? Announce
problem with monadic approach, arrow solution and interest
for category theoretical interpretation.
2. Modelling Computation in Theory and Practice
2.1 Arrows in Haskell
.... Introduce arrows as they appear in Haskell
2.2 Freyd categories
.... Introduce Freyd categories as described in denotational
semantics
2.3 Arrows are Freyd categories!
.... Jump to conclusion on observing obvious parallels, but
backtrack and demand more rigorous analysis.
3. Aligning Theory and Practice
.... Preliminaries & redrawing Jabob &al's construction
3.1 Category Theoretical Preliminaries
3.2 Construction
4. Discussion
.... Success and benefits of theoretical insights; The
Awkwardness of modelling Hask
If time permits:
- A Categorial Model of Hask .... How can we think of Haskell categorically, or more generally, how can we think of pure computation categorically?
- Redraw Atkey's improved version
- Variables denoting categories:
\mathbb
- Names of actual categories:
\mathbf
- Objects of category
\mathbb{C}
:|\mathbb{C}|
- Object of a category: Uppercase math letters
- Haskell types: lowercase verbatim letters