What is Expressiveness in a Computer Language

[Marshall]

Andreas Rossberg wrote:
> Marshall wrote:
> >
> > 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.

I don't follow. Are you saying that a set cannot be described
intentionally? How is "the set of all objects that implement the
Foo interface" not sufficiently abstract? Is it possible you are
mixing in implementation concerns?


> >>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

Okay. Since this paper is in the ACM walled garden, I'll have to
wait until next week to get a look at it. But thanks for the reference.


> >>(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.

Fair enough.


Marshall