<p>N.B. I asked the <a href="https://stackoverflow.com/questions/24705418/generalizing-haskell-could-we-replace-hask-with-cat">same question on Stack Overflow</a> but it was suggested that it is too theoretical for this forum.</p>

<p>It is great that Haskell allows us to walk around in the category $Hask$. But sometimes I feel it is too tight. So I had this idea about a programming language that would allow us to move around in the category $Cat$ of small categories, where categories would be types and functors from categories $C$ to $D$ would be functions of type $C \to D$. At first it seemed a crazy idea, but I found an <a href="http://www.brics.dk/RS/01/27/">article</a> by Glynn Winskel and his student Mario Jose Cáccamo about such calculus! However it is limited to a fragment of $Cat$. Do you think that it would be possible to extend Haskell in this spirit, i.e., instead of working in the category $Hask$, it would work in the category (or better, 2-category) $Cat$? Are you aware of any calculus similar to the one by Cáccamo and Winskel?</p>

<p><a href="http://www.brics.dk/RS/01/27/">http://www.brics.dk/RS/01/27/</a></p>

CC BY-SA 3.0
2014-07-21T15:54:33.413Z
$Cat$ contains uncountable categories which you could not "walk though". You would be limited to at least the "computable" categories. I'm not sure what that would entail but at the very least your collections of objects and arrows would have to be countable.
Jake
CC BY-SA 3.0
2015-01-09T15:30:38.580Z
@Jake: I guess you could have uncountable models, you just wouldn't be able to denote most of them — just like with real numbers. But then, your language is anyway likely to map to a countable subcategory, so my nitpicking might leave your point essentially intact.
Blaisorblade
CC BY-SA 3.0
2015-01-09T15:31:59.333Z
Consequence: @Jake's limitation of "being countable" seems to mean that Cáccamo' and Winskel' calculus is general enough — they seem to just restrict to small categories (as far as I've read). Or do they later add further restrictions?
Blaisorblade
<pl.programming-languages><type-theory><functional-programming><ct.category-theory><haskell>
Generalizing Haskell: could we replace Hask with Cat?
Bob
# Generalizing Haskell: could we replace Hask with Cat?

(Asked by: username_0 on 2014-07-20)

N.B. I asked the [same question on Stack Overflow](https://stackoverflow.com/questions/24705418/generalizing-haskell-could-we-replace-hask-with-cat) but it was suggested that it is too theoretical for this forum.

It is great that Haskell allows us to walk around in the category $Hask$. But sometimes I feel it is too tight. So I had this idea about a programming language that would allow us to move around in the category $Cat$ of small categories, where categories would be types and functors from categories $C$ to $D$ would be functions of type $C \to D$. At first it seemed a crazy idea, but I found an [article](http://www.brics.dk/RS/01/27/) by Glynn Winskel and his student Mario Jose Cáccamo about such calculus! However it is limited to a fragment of $Cat$. Do you think that it would be possible to extend Haskell in this spirit, i.e., instead of working in the category $Hask$, it would work in the category (or better, 2-category) $Cat$? Are you aware of any calculus similar to the one by Cáccamo and Winskel?

<http://www.brics.dk/RS/01/27/>

**Tags:** pl.programming-languages, type-theory, functional-programming, ct.category-theory, haskell

> **Comments:**
> **username_1**: $Cat$ contains uncountable categories which you could not "walk though". You would be limited to at least the "computable" categories. I'm not sure what that would entail but at the very least your collections of objects and arrows would have to be countable.  
> **username_2**: @username_1: I guess you could have uncountable models, you just wouldn't be able to denote most of them — just like with real numbers. But then, your language is anyway likely to map to a countable subcategory, so my nitpicking might leave your point essentially intact.  
> **username_2**: Consequence: @username_1's limitation of "being countable" seems to mean that Cáccamo' and Winskel' calculus is general enough — they seem to just restrict to small categories (as far as I've read). Or do they later add further restrictions?  

---

## 0 answers

