Abstract
| Language | English |
|---|---|
| Pages | 19-37 |
| Number of pages | 19 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 229 |
| Issue number | 5 |
| DOIs | |
| Publication status | Published - 8 Mar 2011 |
Fingerprint
Keywords
- arrows
- categorical model
- functional programming
- Hughes arrows
- Freyd categories
Cite this
}
What is a categorical model of arrows? / Atkey, Robert.
In: Electronic Notes in Theoretical Computer Science, Vol. 229, No. 5, 08.03.2011, p. 19-37.Research output: Contribution to journal › Conference Contribution
TY - JOUR
T1 - What is a categorical model of arrows?
AU - Atkey, Robert
PY - 2011/3/8
Y1 - 2011/3/8
N2 - We investigate what the correct categorical formulation of Hughes’ Arrows should be. It has long been folklore that Arrows, a functional programming construct, and Freyd categories, a categorical notion due to Power, Robinson and Thielecke, are somehow equivalent. In this paper, we show that the situation is more subtle. By considering Arrows wholly within the base category we derive two alternative formulations of Freyd category that are equivalent to Arrows—enriched Freyd categories and indexed Freyd categories. By imposing a further condition, we characterise those indexed Freyd categories that are isomorphic to Freyd categories. The key differentiating point is the number of inputs available to a computation and the structure available on them, where structured input is modelled using comonads.
AB - We investigate what the correct categorical formulation of Hughes’ Arrows should be. It has long been folklore that Arrows, a functional programming construct, and Freyd categories, a categorical notion due to Power, Robinson and Thielecke, are somehow equivalent. In this paper, we show that the situation is more subtle. By considering Arrows wholly within the base category we derive two alternative formulations of Freyd category that are equivalent to Arrows—enriched Freyd categories and indexed Freyd categories. By imposing a further condition, we characterise those indexed Freyd categories that are isomorphic to Freyd categories. The key differentiating point is the number of inputs available to a computation and the structure available on them, where structured input is modelled using comonads.
KW - arrows
KW - categorical model
KW - functional programming
KW - Hughes arrows
KW - Freyd categories
UR - http://www.scopus.com/inward/record.url?scp=79952421374&partnerID=8YFLogxK
UR - http://www.sciencedirect.com/science/article/pii/S157106611100051X
UR - http://personal.cis.strath.ac.uk/~raa/arrows.html
U2 - 10.1016/j.entcs.2011.02.014
DO - 10.1016/j.entcs.2011.02.014
M3 - Conference Contribution
VL - 229
SP - 19
EP - 37
JO - Electronic Notes in Theoretical Computer Science
T2 - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
IS - 5
ER -