What is Expressiveness in a Computer Language

[Andreas Rossberg]

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