What is a categorical model of arrows?

Research output: Contribution to journalConference Contribution

7 Citations (Scopus)

Abstract

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.
LanguageEnglish
Pages19-37
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume229
Issue number5
DOIs
Publication statusPublished - 8 Mar 2011

Fingerprint

Functional programming
Categorical
Model
Enriched Category
Functional Programming
Formulation
Isomorphic
Alternatives

Keywords

  • arrows
  • categorical model
  • functional programming
  • Hughes arrows
  • Freyd categories

Cite this

@article{c1c292e9e27446f093835ed17398345d,
title = "What is a categorical model of arrows?",
abstract = "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.",
keywords = "arrows, categorical model, functional programming , Hughes arrows, Freyd categories",
author = "Robert Atkey",
year = "2011",
month = "3",
day = "8",
doi = "10.1016/j.entcs.2011.02.014",
language = "English",
volume = "229",
pages = "19--37",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
number = "5",

}

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 journalConference 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 -