Marshall wrote: >Andreas Rossberg wrote: >>Chris Uppal wrote: >> >>>I have never been very happy with relating type to sets of values (objects, >>>whatever). >> >>Indeed, this view is much too narrow. In particular, it cannot explain >>abstract types, which is *the* central aspect of decent type systems. > > What prohibits us from describing an abstract type as a set of values?
If you identify an abstract type with the set of underlying values then it is equivalent to the underlying representation type, i.e. there is no abstraction. >>There were papers observing this as early as 1970. > > References? This is 1973, actually, but most relevant: James Morris Types Are Not Sets. Proc. 1st ACM Symposium on Principles of Programming Languages, 1973 >>(There are also theoretic problems with the types-as-sets view, because >>sufficiently rich type systems can no longer be given direct models in >>standard set theory. For example, first-class polymorphism would run >>afoul the axiom of foundation.) > > There is no reason why we must limit ourselves to "standard set theory" > any more than we have to limit ourselves to standard type theory. > Both are progressing, and set theory seems to me to be a good > choice for a foundation. What else would you use? I'm no expert here, but Category Theory is a preferred choice in many areas of PLT. - Andreas -- http://mail.python.org/mailman/listinfo/python-list
