Do all class types in Haskell have a theoretical analogue to the category?

Question

Consider a class of type whose members are of type * -> * . For example: class Functor . It is well known that in Haskell there is a correspondence between this class and its mathematical (i.e., categorical) counterpart. Summarizing:

Question 1: Does each class class in Haskell, whose members have the form * -> * , support some kind of function between the categories?

Now consider a class whose members are of type * . For example, you could imagine a class of type Group , which corresponds to the category of groups (technically, Group will be a subcategory of Hask , whose objects consist of all types of Haskell). Summarizing:

Question 2: Does each class category in Haskell whose members have the form * correspond to a certain category (technically: some Hask subcategory)?

From this, one can ask the following general question:

Question 3: Do type types equal to or greater than * -> * -> * have any categorical concept?

Indeed, this whole question can be summarized as follows:

General question: Does each class of type Haskell correspond to a certain theoretical representation of the category?

EDIT:. At least it seems you could say that, since each type of class contains a certain set of Haskell types, you can view each type of class as some Hask subcategory (closed under . And using id ).

Answer 1

When interpreted quite meticulously, the answer to all these questions is yes, but for non-informatively trivial reasons.

Each category C is limited to a discrete subcategory | C | with the same objects as C, but only with morphisms of identity (and, therefore, no interesting structure). At the very least, operations on Haskell types can be bored as operations on a discrete category |*| . A recent history of "roles" boils down to (but does not force as) an attempt to recognize that morphisms matter, not just objects. The "nominal" role for types is equal to the work |*| , not * .

(Note that I do not like the use of “Hask” as the name for the “Haskell type and function category”: I am afraid that designating one category as a Haskell category has an unfortunate side effect that will blind us to the wealth of another categorical structure in Haskell programming. This is a trap .)

Being pedantic in different ways, I would say that you can compose any old shit as a class over any old look, without any interesting structure (but with a trivial structure, which can still be categorically talked about if necessary). However, the classes you find in the library are very often structured. Classes above * -> * are often, by design, subclasses of Functor , requiring the existence of some natural transformations in addition to fmap .

For question 2. Yes, of course the class over * gives a subcategory of * . There is no problem to pull objects out of a category, because the categorical requirement for the existence of identities and composites requires morphisms, given objects, but does not require any requirements as to which objects exist. The fact that it is boring makes it a boring fact. However, many of the cool Haskell categories above * lead to much more interesting categories than those that arise as subcategories * . For example, the Monoid class gives us a category where the objects are Monoid instances, and the arrows are monoid homomorphisms: not only any old function f from one Monoid to another, but one that preserves the structure: f mempty = mempty and f (mappend xy) = mappend (fx) (fy) .

In question 3, well, in the sense that a ton of categorical structure is hidden all over the world, there is a certain ton of categorical structure (possibly, but not necessarily) in higher forms. I especially like functors between indexed sets families.

 type (s :: k -> *) :-> (t :: k -> *) = forall x. sx -> tx class FunctorIx (f :: (i -> *) -> (j -> *)) where mapIx :: (s :-> t) -> (fs :-> ft) 

When i and j coincide, it makes sense to ask when such f is a monad. The usual categorical definition is enough, although we left * -> * behind.

This message: nothing about the fact that this class inherently causes an interesting categorical structure; There is a lot of interesting categorical structure that can be usefully represented through type classes of all kinds. There are, of course, interesting functors from * (sets and functions) to * -> * (functors and natural transformations). Do not dazzle careless talk about "Hask" with a wealth of categorical structure in Haskell.

Answer 2

One problem is that category theory, general abstract absurdity, is a theory that you can use to talk about almost anything in mathematics. So, everything that we are talking about can be expressed using the language of category theory, but we cannot give any interesting results.

Does each class class in Haskell, whose members are of the form * -> * , correspond to some kind of function between the categories?

Not. This question contains a type error! A function displays many sets, but a category is not a set. (In other words, functions are morphisms in the Set category.) Categories are formulated using classes, often the correct classes, so you cannot pass a category to a function.

We will call objects in * -> * morphisms in the Haskell type category. A subcategory of this category is the Haskell type functor category called Functor .

Does each class line in Haskell, whose members have the form * , correspond to a certain category (technically: some subcategory in Hask)?

Yes. It is true, but it is not very interesting. Just remove every object from Hask that is not in your class, and remove any morphism in Hask that does not consume and does not create elements from your class, and you remain a subcategory of Hask. This category must have at least one object, ⊥ and at least one morphism, id .

Do type types equal to or greater than * -> * -> * have any categorical concept?

Yes. Again, this will not be very interesting. Take class X with type * -> * -> * .

Is X object in the same category class category? Well yes. But this category is not very interesting, because it is difficult to imagine any non-trivial morphisms.

Is X morphism in some category? No, because it cannot be composed.

Is X functor displaying a subcategory of types in Hask, a subcategory of morphisms on types in Hask? Of course, but we would need to have special knowledge that both XY ab and XZ ab valid for the same ab before we resolve morphisms into our initial subcategory on Hask types.

It does not seem to me that this will give any useful ideas, which is not surprising, because we do not know anything about X

---

conclusions

Category theory is one of those tools that is very easy to overdo and overdo. If you are not interested in category theory as a matter of study in itself, my recommendation is to find specific motives for using it. Special types (functors, lenses, monads, comonads, etc.) Sometimes provide you with enough structure or "raw mathematical material" from which you can build an interesting proof in category theory. But studying class types in general can be a little more abstract than useful.

Answer 3

You can imagine comparisons between categories that do not preserve their categorical structure. But they are not interesting. In category theory, we want to work with structure-preserving mappings, and they are called functors.

The bare type constructor of type *->* does not have the ability to display morphisms. Thus, the best you can do, as @pigworker explained, is to interpret them as functors from | C | in C, just because | C | has no nontrivial morphisms for mapping.

A Haskell Functor is an endofector if it satisfies functorial laws (which cannot be applied in Haskell). An entouctor is not an object in the category that it displays, therefore it is not a type. But this is also true with morphisms - they are not objects. However, there is a way to represent morphisms as objects if the category supports exponents. The Haskell type category is Cartesian closed, so it supports exponents.

Does it also provide objects (types) representing endofunctors? As far as I know, this is not so. So the functor is not a member of Hask (or as we call it).

By the way, a mapping of the form *->*->* can have a non-trivial categorical interpretation as a bifunctor functor preserving the structure from the CxC to C product category. See the Bifunctor definition.