6
$\begingroup$

N.B. I asked the same question on Stack Overflow 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 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/

Improve this question
$\endgroup$
3
  • $\begingroup$ $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. $\endgroup$
    – Jake
    Jul 21, 2014 at 15:54
  • 1
    $\begingroup$ @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. $\endgroup$
    – Blaisorblade
    Jan 9, 2015 at 15:30
  • $\begingroup$ 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? $\endgroup$
    – Blaisorblade
    Jan 9, 2015 at 15:31

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.