What we talk about when we talk about types

These dialogues somewhat pedantically dissect what we mean when we say a type is an instance of a typeclass or a type has an instance of a typeclass and why. Through the course of conversation, we touch on the nature of types, type constructors, and typeclasses, which led to us talking about math, set theory and category theory, and what they have to do with types and typeclasses.

Examples of the phrases we’re discussing, using “semigroup” as an example:

The takeaway is that when we use the word “type” it can mean any of several things: “type declaration” on its own, “type plus instances”, names of “types” or “type constructors”, a property of an algebraic structure. These are not in conflict; they are all essential, in our view, to understanding what types and typeclasses are.

●●●
Julie:

Oh, dear, there are still many unanswered tickets in the (haskellbook) Zendesk. This one I just opened is a complaint/question because we say a type “has an instance” of a typeclass.

Chris:

What are people’s objections to that?

Julie:

That it can’t be both “is an instance” and “has an instance” and the Haskell Report says “is” – or if they haven’t checked the report, then generally that they think “has” is confusing because they see “is” elsewhere.

Chris:

Hmmm, indeed the Report does. Very pointedly, too.

Julie:

Yes. The book used to kind of alternate between the two “is” and “has” and it bothered me. I don’t like the emphasis, though. I think there isn’t as much contrast between the two things as other people seem to think.

Chris:

I think “is-a” makes sense for the mathematical object and “has-a” makes sense for the Haskell type.

Julie:

Maybe. I’m not sure enough about the distinction you’re making. For me, as a learner, the thing that bothered me is that if a type “is” an instance of a typeclass, why do I have to write an instance (or derive one)? If I write a type, it exists before its typeclass instance, and the type declaration is not the same piece of code as its instance declaration. It can exist as a type without any typeclass instances. You can’t do much with it, but it can. So, saying a type is an instance of a typeclass seemed pedagogically misleading to me.

Chris:

Yes, that’s kinda my thinking.

Julie:

I mean, I understand what they’re getting at with that, but as a learner I found that a difficult thing to grasp.

Chris:

Like, there’s the type itself, and the type-with-instances, and they both have the same name. The former has an instance, the latter is an instance. They both work, but “has-a” corresponds more to what you do when you’re programming.

Julie:

They do, yeah. But to keep things clear, I switched them all to “has”. We do say “this type is a Monoid” as a kind of synecdoche of “this type-with-instances is a Monoid.” I should write a form letter response I can send to the people who send in this complaint.

●●●
Julie:

I told you the guy who wants to argue about “is” vs “has” an instance of a type replied, right? I just re-read it and noticed that his argument consists of twice repeating verbatim what the Haskell Report says. I don’t think he can articulate what the difference is without using the exact same phrasing.

Chris:

Does he actually have an argument beyond an appeal to authority?

Julie:

No.

Chris:

Just draw circles around some code and be like, “Look: This is a type. This is an instance. The type is clearly not the instance. QED.”

Julie:

LOL. The usage of “is” started to bother me in particular once I found out that some types, like Integer, are monoidal but don’t have a Monoid instance. Because they form monoids under (at least) two different operations.

Chris:

I still have objections to saying a type is inherently monoidal, or of any other class.

Julie:

Martin, are we going to argue about monoids again? Addition and multiplication are canonical monoidal operations. I don’t know if ‘canonical’ is a mathematically approved term.

Lists also admit different monoids, but we’ve chosen one as the default. Is concatenation more monoidal than zipping?

Chris:

I think the only open question to that guy’s point is whether we consider the instance definition to be “part of the type” in some sense.

Julie:

Yeah, and that’s a reasonable point. I chose “no” for the book to make it more apparent that the instance is a separate piece of code – an implementation! – whether you write it or derive it.

Chris:

But we kinda pretend it is, right? Which is why we get all antsy about orphans and hand-wavy about typeclass cohesion.

●●●

One day, Chris tweeted this:

Typeclass instances can be very boilerplatey but usually in a satisfyingly shove-it-under-the-rug-and-don’t-worry-about-it-again sort of way

And the replies rekindled our discussion.

Chris:

I’m gonna get real tired of answering the question of whether an instance and an instance declaration are the same thing, aren’t I?

Julie:

Yes. It’s okay with me if you want to switch for Joy. Many people are going to prefer to stick to the Report wording. But to me it’s like shrugging away a chunk of code.

Chris:

Why does this man feel the right to demand I justify my word choice? I can just not reply, right.

Julie:

Yes. When people email our book support, I feel compelled to reply, but it’s Twitter, you’re not obligated to anything.

Chris:

It’s like getting upset when someone refers to a type declaration by calling it a type.

Julie:

Do you want to write a blog post about this?

Chris:

A little. But a very short one, focusing not on the Haskell syntax, but on the math definitions. For example, “a semigroup is a set with a binary associative operation”, so it is weird to say that String is an instance of semigroup. It is a set with a binary associative operation, so it is a semigroup, right?

Julie:

There’s a semigroup over strings – actually, more than one – isn’t that the more mathematical way to put it? Not that they are or have? Or maybe that they admit a semigroup or form a semigroup under concatenation, I’m not sure. Like, the semigroup is the combination of the set and the operations, and String can be the “set” part of that.

…If that makes sense.

Chris:

Now one might rightfully distinguish “is a semigroup”, “is a Semigroup instance”, and “is an instance of the Semigroup typeclass.”

Julie:

What’s the distinction between the last two?

Chris:

I didn’t mean to say there are three different things, but there are three phrases and you could reasonably choose to draw the line at any point. There could be a difference between the last two if you choose to say “semigroup” for the math concept and “Semigroup typeclass” for the Haskell thing. But nobody would ever do that consistently so that’s not a good prescription to fight for.

Julie:

Another weird thing, to me, about saying the type is the instance: a String has at least two operations under which it forms a semigroup, right? So, okay, it is, or admits, a semigroup. But saying it is an instance of Semigroup seems strange, from a programming perspective. I suppose it’s the CT idea that we have a structure called Semigroup and the set String is an instance, or an object in that category or something?

With the typeclass, as with the category theoretic notion, we don’t really care what the operations are, just that there exists some operation under which it forms this structure. So, that’s all cool, it just seems weird to talk about Haskell that way. When we program, we do care about those operations and how they work, so we care about the instance declaration. But this gets weirder, in my humble opinion, when you’re talking about, say, Num. What is the algebraic structure called Num?

Chris:

Num is an algebraic structure; it’s like a fucked up ring with some other shit tacked on.

●●●
Julie:

I find it unhelpful the way programmers talk about “an algebra,” but it makes more sense as an algebraic structure – at least to me, although I think this is a question of terminology, not meaning. An algebraic structure is a set with one or more operations defined on it that satisfies a list of axioms. I forget how we ended up defining “an algebra” in haskellbook, but we did try to define it because it was bothering me.

Chris:

Things like semigroup, group, ring, field, etc., are those algebraic structures, or classifications of algebraic structures?

Julie:
(quoting from Haskell book)
And so, as we said above, an algebra refers to some operations and the set they operate over. Here again, we care less about the particulars of the values or data we’re working with and more about the general rules of their use.

So, those are algebraic structures. A monoid is an algebraic structure. A monoid is not just a binary associative operation but a structure that includes a set (a type, in Haskell?) and that operation.

Chris:

Wait, but … so it’s the instance that’s the algebraic structure? Not “monoid” itself but like “the monoid of summed integers”?

Julie:

I think that’s right. A monoid in general is a structure with a set and a monoidal operation defined for it that follows some axioms or whatever, right? But that’s a monoid in general. A specific monoid, a specific structure, I think it’s right to say, e.g., “the monoid of summed integers” is an algebraic structure. Does that make sense? I do not have high confidence about this.

Chris:

Yes, and that jibes with the Wikipedia summary.

●●●

Another day, another Twitter thread, in which someone said this:

But there are no * or + operators for IO.
Julie:

But IO does have a Monoid. Those are monoidal operators. This seems like a confusion of the operator for the algebra. Wait, IO is a Monoid now, right?

Chris:

Pretty sure it’s a monoid. GHC 8 and up, I think.

Julie:

Well, that’s sort of making me feel better about saying “has an instance.” That type didn’t used to have a monoidal operation defined for it. But now that it has an instance defined, it is a monoid: a type with the appropriate operation defined over it.

●●●
Julie:

Hmm, Real World Haskell says:

This says that we are declaring a typeclass named BasicEq, and we’ll refer to instance types with the letter a. An instance type of this typeclass is any type that implements the functions defined in the typeclass… The key is that, when you list the types of your functions, you must use that name to refer to instance types… “For all types a, so long as a is an instance of BasicEq, isEqual…,

It’s like they start out saying “a is an instance type” if it implements the functions, then they elide the “type” and start saying “a is an instance of Eq” etc. I think I’m more comfortable saying “is an instance type” for “is a type for which an instance is defined” than just “is an instance” which on the surface seems to conflate the type declaration and the instance declaration.

Chris:

“an instance type”? This is unfamiliar phrasing to me. I need to think about that.

Julie:

Yeah, it’s unusual phrasing, I think. To me it suggests no one is super comfortable with what we’re talking about here.

Chris:

I’m bothered immediately by the fact that it’s not necessarily a type. We’re really lacking a word that encompasses both types and type constructors.

Julie:

Yes, there is that, too. It conflates those two things in a way that is sorta okay when you’re talking about Eq but not good for Functor and disastrous for the difference between Monoid and Alternative. Maybe “disastrous” is hyperbolic.

I’ve been trying to decide if i should try to include Monad in that talk proposal about different species of monoids. It might be too much for 30 minutes. I could probably spend 30 minutes only talking about why Monad is a monoid (in the category of endofunctors). I consider this nonobvious.

Chris:

I was thinking about that recently. I couldn’t remember what an endofunctor is.

Julie:

In Haskell, it’s just a functor. So, it’s a monoid of functors, like Alternative is a monoid of applicative functors. Oh, and it’s “a monad in X is a monoid in the category of endofunctors of X” not just the category of endofunctors.

Chris:

Right. Quoting Categories for the Working Mathematician: “An endofunctor, T : X → X” (in Haskell, a type constructor of kind * -> * with a Functor instance).

Julie:

This phrasing has always bothered me a bit, but I think it’s for similar reasons. It means “a monoid of type constructors that have instances of Functor (or Applicative in the case of Alternative)”, or, if you prefer, type constructors that are functors or applicatives. But I’ve always thought it makes it sound like they are monoids of a sort of function called a functor, almost like they are monoids of the function type, but for a functor-function. And since both Monad and Applicative involve a functor operation, it’s easy to make this mistake. But Monad and Alternative are monoids of type constructors that are functors (but Monad also involves fmapping, whereas Alternative does not). Applicative differs from Monad in where the extra “layer” comes from, so it needs join instead of (implicitly, I guess) a conjunctive monoid.

●●●

During this next conversation, Julie was on airplanes, texting on her phone, wondering why we tolerate phone autocorrects.

Julie:

I pushed the start of that dialogue about types and instances, if you want to take a look at it.

Chris:
Oh,
and it’s really “a monad in X is a monoid in the category of endofunctors of X” not just the category of endofunctors.

I think I missed that the first time around. That… makes a lot more sense. I’ve always read “the category of endofunctors” literally, to mean all endofunctors.

Julie:

Yeah. I did too for a long time, and still forget it sometimes. Oh, I just had a thought. Is functor (or endofunctor) considered an algebraic structure? That is, a set with a functor operation over it?

Chris:

I suppose it must be. It’s easy to forget about functor because it’s the best abstraction.

Julie:

Suddenly it makes more sense to me. I guess a monad in Hask is a monoid in the category of functors of Hask, i.e. the type constructors that have Functor instances.

Chris:

There’s rarely any question about “which fmap” to use; it’s nearly always clear, so we don’t talk about it like we say “a type and a semigroup operator”, but we don’t say “a type constructor and a functor operation” because it’s not “a” functor operation, it’s always “the” obvious/only fmap implementation.

Julie:

Right. I think it’s also less clear what the essence of a functor operation is, unlike semigroup/monoid. We don’t seem to talk much about what is a functor the way we do with semigroup/monoid. Joy is going to, though.

Chris:

Can we say monad is a monoid in the category of type constructors for which there is a functor? That’s what screwed me up, thinking it was a monoid over the values, where really it’s a monoid over the type constructors, right? It’s also hard for me that we end up alternating between the set theory definition of monoid and the category theory definition.

Julie:

Ooooh, what do you mean? Because I’m not aware of this, I don’t think.

Chris:

What you and I usually talk about is the set theory notion of monoid: a set, one element of the set being an identity, a binary associative operation on the set.

Julie:

Because in the category theory notion, there’s not a distinction between conjunction and disjunction and the operation details themselves don’t matter?

Chris:

Category theory: a monoid is a category with exactly one object. We say “a monoid over X”, sometimes I puzzle between whether X refers to a set, or to the single object in a monoidal category.

Julie:

I don’t think the notion of a one-object category is all that useful, though, when we’re talking about Haskell. In the set theory case, I think “a set” means “a type” in Haskell. In the category theory it means “the set of types.” …And type constructors? I think at that level of abstraction the distinction between types and type constructors is irrelevant.

Chris:

I don’t think the set theory notion is any different in that regard. The set definition of a monoid makes no mention of what the operation details are either.

Julie:

Can’t quite agree with that.

Chris:

I think they’re entirely equivalent definitions.

Julie:

Technically equivalent, yes. But not functionally equivalent, by which I mean they allow us to know and talk about different things. What do you know about a Haskell Monoid from knowing it’s a one-object category with arrows pointing only to itself? It’s useful for some things but only after knowing about the set theory notion of monoids.

Chris:

What do you know about a set theory monoid knowing there’s a binary associative operation, without talking about what that operation is?

Julie:

Ah but we do know what those operations are in set theory because set theory is Boolean algebra. When we’re talking about sets, we know what the monoidal operations are.

Chris:

What are they?

Julie:

Conjunction and disjunction.

Chris:

But if all you know if that you have a monoid, you don’t know which one it is.

Julie:

That is true. At that level we don’t care yet. And most (all?) sets, like most types in Haskell, have at least two, a conjunctive and a disjunctive monoid.

Chris:

The monoid abstraction removes that detail just as much as the category does.

Julie:

Not as much. CT is a further level of abstraction.

Chris:

If you map the category arrows to functions that they represent, now you can talk about conjunction and disjunction again.

Julie:

Then we’re talking about set theory though, at least when the objects are sets. Which is my point. Because now we care about the objects and arrows in that category and what sorts of things they are. They lose some polymorphism in a sense. It’s like the relationship between parametricity and constrained polymorphism a bit.

Chris:

Yeah, so it does take one restriction: the arrows have to be a set in order to go from category theory monoid to set theory monoid. Nothing stops me from talking about what the arrows in a category represent and using that to reason about the category, does it?

Julie:

No, it’s just that then you’re not really at the level of abstraction that category theory exists for. Then you’re talking about something more concrete, even if not yet fully concrete.

Chris:

We can talk about a monoidal category in which the arrows represent additions or multiplications.

Julie:

Now I think you’re conflating the set theory notion with the category theory one.

Chris:

But isn’t abstract algebra also the wrong level of abstraction for that?

Julie:

Wrong for what purpose?

Chris:

Talking about additions or multiplications solely as a monoidal algebra, not talking about their relationships in a ring or something.

Julie:

I have lost the point of this. First, you said you were confused because you couldn’t tell sometimes if we were talking about the set theory notion or the category theory notion, but now you appear to be arguing that they’re the same thing.

Chris:

Equivalent things.

Julie:

They are and they aren’t; it depends on your point. It depends on what we are talking about them for. Usually when I’m talking about monoids, what I care about is closer to the set theory notion because the category theory notion is not very useful for thinking/talking about the monoidal operations, and it’s not meant to be.

Chris:

Yeah, that makes sense.

Julie:

Category theory exists so we can talk about things without caring about what kinds of things they are, only comparing them by what they have in common.

Chris:

That confused me for a long time. Basically up to just now.

Julie:

It’s like when we talk about very abstract syntax in linguistics. In some sense it maps to languages that people speak, but we’re abstracting out that far because we want to talk about certain properties of language without caring about the implementation details of how humans construct meaningful sentences and speak or write them.

That’s why I compared it to parametric versus constrained polymorphism. At the level of parametricity, we can’t know, don’t want to know, what the type will be, so there’s little that we do know about what we’re doing. That’s useful for some things. At the level of constrained polymorphism, we know some things (like when we talk about monoids in set theory) but not everything, not yet. It’s not until things become concrete (as they do when we talk about “integers form a monoid under…”) that we really know a lot of detail. We can talk about all those levels, they all have their uses, things can be equivalent between those levels, but we can still make useful distinctions and use those levels of abstraction for different purposes, to make it easier to talk about precisely the thing we care about at the time.

I’m about to get on the next plane. I’m all, “I can’t board right now; I’m too busy arguing about math.”"

Chris:

I still feel fuzzy about a lot of this.

Julie:

Yeah, a lot of what I just said was stuff I’ve never thought before, so I don’t know yet if I’m way off base or what. I have thought about how the kind of syntax I used to do is like the category theory of language, though.

I did work on real languages, too, and their specific syntax, but some of what I did is to be able to compare cross-linguistically without talking at all about what the grammar of any particular language looks like. Like category theory is so abstract that triangles and types and integers and functions maybe, depending on the category, can be seen as more similar than different because they’re all just objects. And multiplication and addition are the same too. The difference between them has been abstracted away. And yet it’s relevant to us, as programmers.

In set theory, I suppose the distinction between conjunction and integral multiplication for example has also been abstracted away. So what comparisons it allows us to make and examine and talk about are different from when we talk about more concrete things or category theory notions. There is purpose to all the layers of abstraction, though. At each layer we can “see” and talk about different things and it’s wonderful and exciting.

Category theory is so close to the metal, where “metal” means brain, something fundamental about how our brains work. It’s exciting as hell. Sorry. I’m having a religious moment here.

That said, I think the upshot here is don’t let a category theory sense of what a monoid is dictate what makes sense when we talk about Haskell.

Chris:

Yes, this sounds good. I was intrigued when I saw Milewski lay out that notion of category theory being how our brains work.

I don’t think I’d heard anyone describe that.

Julie:

I’ve had this thought about it and syntax being about how our brains really fundamentally work for a long time, like since the first time I heard Snively and Laucher’s talk about types that convinced me to learn Haskell because types are like generative syntax.

Chris:

He makes a joke about how even the language of “arrows” is an allusion to something humans have been doing for tens of thousands of years.

Julie:

Well, there’s Lakoff again.

Chris:

oh?

Julie:

METAPHORS. Metaphors are like the kan extensions of language.