As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data types as set that does not contain itself, can we say that in practice type is an infinite set of its members where instance membership is defined by of number of features that are intrinsic to this type/set (existence of certain properties, methods)? If no what would be the counterexample?
Type system based on naive set theory
type theory;set theory;type systems
The main reason for avoiding sets in semantics of types is that a typical programming language allows us to define arbitrary recursive functions. Therefore, whatever the meaning of a type is, it has to have the fixed-point property. The only set with such a property is the singleton set.To be more precise, a recursively defined value $v$ of type $\tau$ (where typically $\tau$ is a function type) is defined by a fixed-point equation $v = \Phi(v)$ where $\Phi : \tau \to \tau$ can be any program. If $\tau$ is interpreted as the set $T$ then we would expect every $f : T \to T$ to have a fixed point. But the only set $T$ with this property is the singleton.Of course, you could also realize that the culprit is classical logic. If you work with intuitionistic set theory, then it is consistent to assume that there are many sets with fixed-point property. In fact, this has been used to give semantics of programming language, see for exampleAlex Simpson, Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory, In Annals of Pure and Applied Logic, 130:207-275, 2004.