> more or less invented types to solve a problem he was having with set theory.

For people who haven't encountered it yet, this problem is the famous "Russell's Paradox"[1], which can be stated as

Consider the set R, consisting of all sets S such that S is not an element of S.

Ie in set builder notation

R = {S : S ∉ S}

and then the paradox comes from the followup question. Is R an element of R? Because of course if it is in R, then it is an element of itself so it should not be. And if it's not in R, then it is not an element of itself, so it should be. This is a logical paradox along the same lines as the famous "The barber in this town shaves all men who do not shave themselves. Does he shave himself?"

In modern axiomatic set theory, Russell's paradox is avoided these days by the "axiom of regularity"[2] which prevents a set builder like "the set of all sets who are not members of themselves", so what I wrote above would not be accepted as a valid set builder for this reason by most people.

Russell proposed instead Type theory which got revived when computer science got going.

[1] https://en.wikipedia.org/wiki/Russell%27s_paradox

[2] https://en.wikipedia.org/wiki/Axiom_of_regularity

> The barber in this town shaves all men who do not shave themselves. Does he shave himself?

I'm not familiar with this one but is it misstated here? The barber doesn't only shave men who don't shave themselves. If he doesn't shave himself then he shaves himself and therefore can shave himself without contradiction. If he shaves himself he can shave himself without contradiction. Either way he shaves himself.

(Or maybe I'm just bad at logic)