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?
• $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.