4
$\begingroup$

In typical object-oriented programming languages like Java, classes are used as types. On the other hand, type-theoretic approaches to object-oriented languages treat interfaces as types.

Are there any theoretical frameworks that formalize the use of classes as types?

$\endgroup$
6
$\begingroup$

Core calculi for Java typically take the classes-as-types approach. Two well-known examples are Featherweight Java and Classic Java.

$\endgroup$
  • 1
    $\begingroup$ Given OO researchers' actual practice, this is clearly the right answer. As a personal prejudice, I've never liked the FJ style of fixing the class table up-front and not letting it vary during program execution. It feels like a trick, sort of like interpreting functional languages by defunctionalizing them. I don't do objects often enough to do anything about it, though! $\endgroup$ – Neel Krishnaswami Aug 31 '12 at 15:49
  • $\begingroup$ @NeelKrishnaswami, if you wanted to model Pascal, wouldn't you start with a table of procedures, as in the IMP language in Winskel's book? In Java, the set of classes is fixed up front (unless you're modeling class-loaders, or something like that). $\endgroup$ – Sam Tobin-Hochstadt Sep 1 '12 at 13:16
  • $\begingroup$ Thanks Sam. Featherweight Java is a very useful data point. I had forgotten about that. On the other hand, FJ seems to be used mainly for defining type systems and type checking, and there seems to be very little on its semantics. So, what a class means as a type is still an open question. $\endgroup$ – Uday Reddy Sep 1 '12 at 14:18
  • $\begingroup$ @NeelKrishnaswami I wonder why the assumption is made that the class table is fixed. If it is merely to define the operational semantics, then the assumption would be quite reasonable because the entire class table would be available before a program is run. Is it restrictive for other reasons? $\endgroup$ – Uday Reddy Sep 1 '12 at 14:23
  • $\begingroup$ @UdayReddy, I'm not sure what more you're looking for. FJ (and Classic Java) both provide operational semantics for the languages. $\endgroup$ – Sam Tobin-Hochstadt Sep 1 '12 at 18:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.