Tomatoes are a subtype of vegetables
November 14, 2014
Subtyping is one of those concepts that seems to makes sense when you first learn it (“Sure, convertibles are a subtype of vehicles, because all convertibles are vehicles but not all vehicles are convertibles”) but can quickly become confusing when function types are thrown into the mix. For example, if a is a subtype of b, is (a -> r) -> r a subtype of (b -> r) -> r? (If you know the answer to this question, this blog post is not for you!) When we asked our students this question, invariably some were lead astray. True, you can mechanically work it out using the rules, but what’s the intuition?
Maybe this example will help. Let a be tomatoes, and b be vegetables. a is a subtype of b if we can use an a in any context where we were expecting a b: since tomatoes are (culinary) vegetables, tomatoes are a subtype of vegetables.
What about a -> r? Let r be soup: then we can think of Tomato -> Soup as recipes for tomato soup (taking tomatoes and turning them into soup) and Vegetable -> Soup as recipes for vegetable soup (taking vegetables—any kind of vegetable—and turning them into soup). As a simplifying assumption, let’s assume all we care about the result is that it’s soup, and not what type of soup it is.

What is the subtype relationship between these two types of recipes? A vegetable soup recipe is more flexible: you can use it as a recipe to make soup from tomatoes, since tomatoes are just vegetables. But you can’t use a tomato soup recipe on an eggplant. Thus, vegetable soup recipes are a subtype of tomato soup recipes.


This brings us to the final type: (a -> r) -> r. What is (Vegetable -> Soup) -> Soup? Well, imagine the following situation…
One night, Bob calls you up on the phone. He says, “Hey, I’ve got some vegetables left in the fridge, and I know your Dad was a genius when it came to inventing recipes. Do you know if he had a good soup recipe?”

“I don’t know…” you say slowly, “What kind of vegetables?”
“Oh, it’s just vegetables. Look, I’ll pay you back with some soup, just come over with the recipe!” You hear a click on the receiver.
You pore over your Dad’s cookbook and find a tomato soup recipe. Argh! You can’t bring this recipe, because Bob might not actually have tomatoes. As if on cue, the phone rings again. Alice is on the line: “The beef casserole recipe was lovely; I’ve got some tomatoes and was thinking of making some soup with them, do you have a recipe for that too?” Apparently, this happens to you a lot.
“In fact I do!” you turn back to your cookbook, but to your astonishment, you can’t find your tomato soup recipe any more. But you do find a vegetable soup recipe. “Will a vegetable soup recipe work?”
“Sure—I’m not a botanist: to me, tomatoes are vegetables too. Thanks a lot!”
You feel relieved too, because you now have a recipe for Bob as well.
Bob is a person who takes vegetable soup recipes and turns them into soup: he’s (Vegetable -> Soup) -> Soup. Alice, on the other hand, is a person who takes tomato soup recipes and turns them into soup: she’s (Tomato -> Soup) -> Soup. You could give Alice either a tomato soup recipe or a vegetable soup recipe, since you knew she had tomatoes, but Bob’s vague description of the ingredients he had on hand meant you could only bring a recipe that worked on all vegetables. Callers like Alice are easier to accommodate: (Tomato -> Soup) -> Soup is a subtype of (Vegetable -> Soup) -> Soup.

In practice, it is probably faster to formally reason out the subtyping relationship than it is to intuit it out; however, hopefully this scenario has painted a picture of why the rules look the way they do.
What a coincidence, I too wrote today about the composition of contravariant functors: http://productivedetour.blogspot.com.es/2014/11/pawn-shops-refrigerators-and.html
But I like your analogy better (and it has prettier pictures!)
I notice that in English, the word “of” indicates covariance, while the word “for” indicates contravariance. For example, “Soup” is covariant: tomato soup is soup of tomatoes. “Recipe” is contravariant: tomato soup recipe is recipe for tomato soup.
Also I’ve come to the conclusion that “subtype” means exactly that there is an injective map in all possible worlds. Obviously subtypes imply injective maps, but surprisingly the converse seems to be true too.
Very cool. This feels like something out of Learn You a Haskell. I have one confusion: you say
But you also say
And I can’t seem to reconcile the former with the latter; specifically, if tomatoes are a subtype of vegetables, which seems to be implied by the latter, then how can vegetable soup recipes be a subtype of tomato soup recipes?
Maybe I’m missing a point here….
So if I’m understanding right,
Tomato Soup Soup
(Tomato -> Soup) -> Soup Soup) -> Soup
So every time we add an arrow to take our type to some other type (invert control), the subtyping relationship flips around?
I feel that this provides an example, but it doesn’t (explicitly) point out any intuition, though the intuitions are “hidden in plain sight.” The key intuition, that certainly can be faster than formal reasoning (though that’s pretty quick and easy too) is whether you have/can provide a value of some type, or whether you need/must receive a value of some type. The former behaves covariantly, the latter contravariantly. (More correctly, would be to say the former precludes contravariant behavior, and the latter precludes covariant behavior.) This intuition is useful for understanding polymorphic, and particularly higher rank types too. This is no accident as polymorphic instantiation induces subtyping relationships, where the polymorphic type is a subtype of its instances.
If you have a Tomato, you have a Vegetable. If you need a Tomato, you don’t need an arbitrary Vegetable but a particular one, namely a Tomato. For Alice to make use of a recipe turning Tomatoes into Soup, she’d actually have to have some Tomatoes.
> Also I’ve come to the conclusion that “subtype” means exactly that there is an injective map in all possible worlds. Obviously subtypes imply injective maps, but surprisingly the converse seems to be true too.
More technically and concisely, in category theory a subobject of B is a monic arrow between an object A and B (where monic arrows generalize injective functions), or an “equivalence class” of such arrows with the appropriate notion of isomorphism. See Wikipedia. https://en.wikipedia.org/wiki/Subobject
I wonder if calling them subtypes and implying a linear order (just because sub would seem to imply that) is part of the reason this is unintuitive.
Is there another way of describing this concept in English that just works?
b <: a
(a -> r) <: (b -> r)
(b -> r) -> r <: (a ->r ) -> r
Hmm… what about saying: b is an example of a? Yeah. That works. a -> r is an example of b -> r, (b -> r) -> r is an example of (a -> r) -> r. I kinda like that!
Does saying “example” instead of “subtype” make sense in all cases?
I think Ashley might be on to something too!
(Editor: Updated formatting)