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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

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

Improve this answer
$\endgroup$
8
  • 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
    Commented Aug 31, 2012 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
    Commented Sep 1, 2012 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
    Commented Sep 1, 2012 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
    Commented Sep 1, 2012 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
    Commented Sep 1, 2012 at 18:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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