I thought Hask was supposed to be the category of Haskell types with functions between them. My Haskell is pretty rusty... how exactly does (->) resolve to this meaning?
Also, on a more theoretical level, since Haskell types themselves belong to the category Hask, by definition, to what extent can Haskell truly model category theory when the objects of a category are evidently being represented here as Haskell types?
1. Hask has Haskell types as objects, and functions between them as morphisms. "a" is a type, "b" is a type, and "a -> b" is an arrow between them.
2. Haskell cannot model (the entirety of) category theory. Everything in Haskell is in Hask, and the only way to get to an entirely different category (say Set) is on paper. This great talk gives some insight into the issue: https://vimeo.com/67174266
1. Hask has exponentials, so (a -> b) is the exponential object final in the category of c's such that we have arrows from a * c to b.
2. It's incorrect that the only category in Haskell is Hask, after all it's easy enough to formulate subcategories of Hask and do your algebra there. I don't know how to answer to what degree you can model category theory, but you can do a lot.
Regarding 2, you're right of course about subcategories of Hask, but I'm more interested in completely different categories.
My question really boils down to this: given the Category class provided in this article, which mathematical categories occur as instances of this Category? Are they necessarily all subcategories of Hask?
I think the answer to that question is better understood in the dependently-typed literature. Haskell does not have easily accessible dependent types, but many of the techniques could be translated and would help to answer your question.
Offhandedly, I'd say you could model many categories of interest, but since you're working in a "challenging" of constructive logic there are a lot of limitations on what can be modeled. At the end of the day, your objects will always be Haskell types, but a lot can be encoded in those types.
Again, though, the DT literature is really where people are attacking this question. Haskell's Category is usually just used when there's a meaningful subcategory of Hask that you want to overload composition and identity on.
Also, on a more theoretical level, since Haskell types themselves belong to the category Hask, by definition, to what extent can Haskell truly model category theory when the objects of a category are evidently being represented here as Haskell types?