Aug. 7th, 2016

Rebutting

Aug. 7th, 2016 09:38 pm
migmit: (Default)
Roman Cheplyaka posted an excellent answer to the Andrej Bauer's statement that "Hask is not a category", saying "Does it matter if Hask is (not) a category?". I'd like to add a few words of my own to that discussion.

We really don't care about whether Hask is a category; that is, if types and functions defineable in Haskell form a category. But not because we are totally OK with an imperfect model (although we are); the real reason is that we never really work in Hask. We only work in some other category, into which Hask can be embedded. Bauer mentiones one of such categories — the category of "continuous posets" (probably domains); there are others, more refined categories such as the category of dI-domains. The point is, we never really care about Hask itself. I think it's possible to define, in a strong mathematical sense, the the category whose object would be EXACTLY the types we can define in a certain variant of Haskell, and the functions would be EXACTLY the functions that we can define between them (although I'm not sure if undefined should be considered a valid function, despite what Wikipedia might say). But, first of all, that category would be very implementation dependent (and even compiler-extensions dependent), and, what's worse, it won't have virtually any nice properties. We won't even have cartesian products in that category!

So, who cares? We embed this category into some larger (although not much larger) category that has all those nice properties. There are different ways to do that, some more refined than the other; and the results we obtain stay true as soon as you choose a refined enough embedding. That works great; there is no need to use Hask itself.