As a predicate Russell's paradox translates to an infinite loop in programming, not an impossibility. And yes, you get in trouble if you define a set from an ar

As a predicate Russell's paradox translates to an infinite loop in programming, not an impossibility. And yes, you get in trouble if you define a set from an arbitrary predicate, but a type is not (necessarily) a set: a type can be a predicate without asking that it be explicitly cast as a set. You can certainly consider the "set of all lists", but you can't enumerate it, because you can have a list of any type and you don't know all the types that can be put into a list. Anyway, I feel like you missed my point. It's that, if you are wondering why types seem to obey algebra but ALSO obey the laws of set theory and the two seem compatible, that this is why: predicates obey the algebra of sets while enumerated types have cardinalities which obey algebra.