8

Consider a type class whose members are of type * -> *. For example: the Functor typeclass. It is a well-known fact that, in Haskell, there is a correspondence between this typeclass and its mathematical (i.e., Category Theoretic) analogue. Generalizing:

Question 1: Does every every typeclass in Haskell whose members are of kind * -> * correspond to some function between categories?

Now consider a typeclass whose members are of type *. For example, one could imagine a type class Group which corresponds to the category of Groups (technically, Group would be a subcategory of Hask whose objects comprise all of Haskell's types). Generalizing:

Question 2: Does every typeclass in Haskell whose members are of kind * correspond to some category (technically: some subcategory of Hask)?

From this, the next general question can be asked:

Question 3: Do typeclasses of kind equal to or higher than * -> * -> * correspond to some category theoretic notion?

And really, this entire question could be summarized as follows:

General Question: Does every Haskell type class correspond to some category theoretic notion?

EDIT: At the very least, it seems you could say that since every type class contains some set of Haskell types as its members, you could view every type class as some subcategory of Hask (closed under . and making use of id).

George
  • 6,927
  • 4
  • 34
  • 67
  • To what category theoretic notion does `Foldable` correspond? – Zeta May 21 '16 at 20:16
  • @Zeta: Catamorphisms. – Dietrich Epp May 21 '16 at 20:18
  • @DietrichEpp That holds for `(Foldable f, Functor f) => f`. But then again, there is no `Foldable` that's not also a `Functor` (at least I can't think of one at the moment). – Zeta May 21 '16 at 20:22
  • 1
    I'd say **2** holds true by definition of the term _subcategory_, but **1** and **3** seem quite far out to me. If I write some silly class whose only members are `Proxy` and `Flip (Kleisli IO) Bool`, then this is highly unlikely to have much mathematical meaning. – leftaroundabout May 21 '16 at 20:38
  • 1
    @leftaroundabout, but wouldn't such a typeclass still trivially serve as some (bizarre) subcategory of `Hask`? – George May 21 '16 at 20:39
  • 1
    @George: Not of **Hask**. Of the degenerate category (actually a monoid) of kinds, whose only object is `*` and whose morphisms are `* -> *` type constructors? Yes, I suppose again trivially. But that really is not very interesting. – leftaroundabout May 21 '16 at 20:49
  • @leftaroundabout: I think that is really all he is asking. Of course it is possible to define a typeclass with little to no mathematical significance, but you don't need Haskell to do that! The interesting thing (assuming it is true) is that every typeclass *has* a category theoretic analog, not what those analogs actually are. – Kwarrtz May 21 '16 at 20:57

3 Answers3

15

When interpreted sufficiently pedantically, the answer to all of these questions is "yes", but for uninformatively trivial reasons.

Every category C restricts to a discrete subcategory |C| with the same objects as C but only identity morphisms (and hence no interesting structure). At the very least, operations on Haskell types can be boringly interpreted as operations on the discrete category |*|. The recent "roles" story amounts to (but is not spun as) an attempt to acknowledge that the morphisms matter, not just the objects. The "nominal" role for types amounts to working in |*| rather than *.

(Note, I dislike the use of "Hask" as the name of the "category of Haskell types and functions": I fear that labelling one category as the Haskell category has the unfortunate side-effect of blinding us to the wealth of other categorical structure in Haskell programming. It's a trap.)

Being differently pedantic, I'd note that you can make up any old crap as a typeclass over any old kind, with no interesting structure whatsoever (but with trivial structure that can still be talked about categorically, if one must). However, the classes you find in the library are very often structure-rich. Classes over * -> * are often, by design, subclasses of Functor, requiring the existence of certain natural transformations in addition to fmap.

For question 2. Yes, of course a class over * gives a subcategory of *. It's no problem to chuck objects out of a category, because the categorical requirement that identities and composites exist require morphisms to exist, given objects, but make no demands about which objects exist. The fact that it's boringly possible makes it a boring fact. However, many Haskell typeclasses over * give rise to much more interesting categories than those arising just as subcategories of *. E.g., the Monoid class gives us a category where the objects are instances of Monoid and the arrows are monoid homomorphisms: not just any old function f from one Monoid to another, but one which preserves the structure: f mempty = mempty and f (mappend x y) = mappend (f x) (f y).

For question 3, well, in that there's a ton of categorical structure lurking everywhere, there's certainly a ton of categorical structure available (possibly but not necessarily) at higher kinds. I'm particularly fond of functors between indexed families of sets.

type (s :: k -> *) :-> (t :: k -> *) = forall x. s x -> t x

class FunctorIx (f :: (i -> *) -> (j -> *)) where
  mapIx :: (s :-> t) -> (f s :-> f t)

When i and j coincide, it becomes sensible to ask when such an f is a monad. The usual categorical definition suffices, even though we've left * -> * behind.

The message is this: nothing about being a typeclass inherently induces interesting categorical structure; there is plenty of interesting categorical structure which can usefully be presented via type classes over all manner of kinds. There are most certainly interesting functors from * (sets and functions) to * -> * (functors and natural transformations). Don't be blinded by careless talk about "Hask" to the richness of categorical structure in Haskell.

pigworker
  • 43,025
  • 18
  • 121
  • 214
6

One of the problems here is that category theory, a.k.a. general abstract nonsense, 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 might not produce any interesting results.

Does every every typeclass in Haskell whose members are of kind * -> * correspond to some function between categories?

No. This question contains a type error! A function maps sets to sets, but a category is not a set. (Put another way, functions are morphisms in the category Set.) Categories are formulated using classes, often proper classes, so you cannot feed a category to a function.

We would call objects in * -> * morphisms in the category of Haskell types. A subcategory of this category is the category of functors between Haskell types, which is called Functor.

Does every typeclass in Haskell whose members are of kind * correspond to some category (technically: some subcategory of Hask)?

Yes. This is true, but it's not terribly interesting. Just remove every object from Hask that is not in your typeclass, and remove any morphism in Hask that does not consume and produce elements from your typeclass, and you are left with a subcategory of Hask. This category should have at least one object, , and at least one morphism, id.

Do typeclasses of kind equal to or higher than * -> * -> * correspond to some category theoretic notion?

Yes. Again, this won't be very interesting. Let's take a typeclass X with kind * -> * -> *.

Is X an object in a category of typeclasses with the same kind? Well, yes. But this category isn't very interesting, because it's hard to imagine any nontrivial morphisms.

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

Is X a functor mapping a subcategory of types in Hask to a subcategory of morphisms on types in Hask? Sure, but we would have to have some special knowledge that both X Y a b and X Z a b are permissible for the same a b before we allow morphisms into our starting subcategory on types of Hask.

This doesn't seem to me like it will produce any useful insights, which is not really surprising because we don't really know anything about X.


Conclusions

Category theory is one of those tools that is really quite easy to overthink and overapply. If you are not interested in category theory as a subject of study in and of itself, my recommendation is to find concrete motivations to use it. Specific typeclasses (functors, lenses, monads, comonads, etc) will sometimes provide you with enough structure or "raw mathematical material" from which you can construct an interesting proof in category theory. But the study of typeclasses in general may be a bit more abstract than it is useful.

Dietrich Epp
  • 205,541
  • 37
  • 345
  • 415
  • "We would call objects in * -> * morphisms in the category of Haskell types." Is it not also true that these objects are themselves members of **Hask**? For example, `[a]` is a type of kind `* -> *`, but `[a]` is also a member of **Hask** since it is itself a type (in this case a higher-kinded type). Using the same reasoning, both `IO`(higher-kinded type) and `IO String` (concrete type) are also members of **Hask**. Is this true? – George May 21 '16 at 21:19
  • 1
    I think your confusion here is from the use of `[]` as an example. Remember, `[]` and `[Int]` are different things. So `[Int]` is an object in Hask, but `[]` is a morphism in Hask. Using `[a]` is a bit confusing—it's like talking about f(x): am I talking about the function f? Or am I talking about the value of the function f when evaluated at x? These are different concepts. – Dietrich Epp May 21 '16 at 21:26
  • I understand that `[]` can be viewed as a morphism of kind `* -> *`; however, it also seems to me that `[]` is a **Type**. It is not a concrete type, but it is a type nonetheless (and hence a member of **Hask**, it seems to me). Note also that I'm not talking about `[]` as a value that is a member of all concrete list types, but rather `[]` as the (higher-kinded) type. Does it still seem to you that I am confused here? – George May 21 '16 at 21:29
  • For example: it seems me that when we write `data T a = ...` in Haskell, we have defined a new **type** `T a` which is a member of **Hask**; in addition, `T Int` is a concrete **type** which is also a member of **Hask**. Yet I agree that `T a` can also be viewed as a morphism of kind `* -> *` since it can take concrete types and produce other concrete types. Is this not the case? – George May 21 '16 at 21:31
  • Again, let's get rid of these extra variables we are using. When you write `data T a`, then `T` is not in Hask, but `T Int` is in Hask. I specifically avoided talking about `T a` because, again, I'm not sure whether you are talking about some specific a, an implicit universal quantifier, or a type formula with a free variable. This is one of the rather elegant features of Haskell: we can talk about `T` and `T Int` without introducing any extra variables like `a`. – Dietrich Epp May 21 '16 at 21:40
  • By comparison, `forall a. T a` is indeed in Hask. It is called a "rank 2 type". – Dietrich Epp May 21 '16 at 21:41
  • I'm not talking about some specific `a` (lower case variables denote universally quantified variables). I'm talking about an implicit universal quantifier. And I'm now deeply confused that you say `T` is not in Hask: for example, it would make sense to add `T` to a type class in Haskell (i.e., if `T` were `[]`, then `T` would be a member of `Functor`); yet how could something be a member of a type class but not `Hask`? Isn't `Hask` a strict superset of all types (including higher-kinded types, like `[]`)? – George May 21 '16 at 21:44
  • Your last comment about the rank 2 type is comforting. I think we might be talking past each other (perhaps with me using incorrect notation). I was treating `forall a. T a` as synonymous with `T a` as synonymous with `T`. If you are saying that `forall a. T a` is indeed a member of **Hask**, then that means I'm not conceptually confused here (but might be incorrectly treating these terms as synonymous). – George May 21 '16 at 21:48
  • @George: Implicit universal quantifiers are very nice when you are writing code or proofs, but for discussions like these we should be a bit more explicit so things are clear. Remember that `forall a. T a` cannot be a functor, because it has the wrong kind. Functors must have kind `* -> *` and are not in Hask. Hask is just the category of concrete types, like `Int`, and higher ranked versions, like `forall a. X`. pigworker puts it rather well: it is unfortunate that the name "Hask" is not all of Haskell, but just `*` types and functions between them. – Dietrich Epp May 21 '16 at 21:52
  • I thought **Hask** was indeed all of Haskell. That's where my confusion might be coming from. Here is a [link which explains the definition of **Hask**](https://wiki.haskell.org/Hask). According to that link, I fail to see how it is distinct from all of Haskell: it seems to clearly say "the objects of Hask are Haskell types", and never qualifies it down to merely the Haskell types of kind `*`. Why think that the objects of **Hask** must only contain types of kind `*`? – George May 21 '16 at 22:06
  • 3
    Some of us use "type" to mean exclusively "thing of kind `*`". Some of us use "type" to mean "thing of any kind". Many of us vacillate between these positions without warning, thus adding to the amount of confusion in the universe. – pigworker May 21 '16 at 22:12
  • 1
    Ok, I see. This is just a terminological convention issue. I appreciate this dialogue and everyone's answers. – George May 21 '16 at 22:14
3

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

A bare type constructor of the kind *->* has no provision for mapping morphisms. So the best you can do, as @pigworker explained, is to interpret them as functors from |C| to C, only because |C| has no nontrivial morphisms to be mapped.

Haskell Functor is an endofunctor, as long as it satisfies functor laws (which cannot be enforced in Haskell). An endofunctor is not an object in the category that it maps, therefore is not a type. But that's also true with morphisms -- they are not objects. There is, however, a way to represent morphisms as objects, if the category supports exponentials. Haskell's category of types is Cartesian closed, so it supports exponentials.

So does it also provide objects (types) representing endofunctors? As far as I know, it doesn't. So a functor is not a member of Hask (or whatever we call it).

Incidentally, a mapping of the kind *->*->* can have a nontrivial categorical interpretation as a bifunctor -- a structure-preserving functor from the product category CxC to C. See the definition of Bifunctor in Haskell.

Bartosz Milewski
  • 11,012
  • 5
  • 36
  • 45