0
$\begingroup$

In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java,

The predicate override(m, D, C→C0) judges whether a method m with argument types C and a result type C0 may be defined in a subclass of D. In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

I am not sure what the predicate override(m, D, C→C0) means.

Does the predicate apply only to the case of overriding? (The first sentence doesn't imply so.)

Isn't it always possible to define a method with any name and any type in any class?

  • In case of non-overriding, that is true.
  • In case of overriding, that is also true.

Could you give examples where it is possible and where it isn't?

Figure 19-2: Featherweight Java (auxiliary definitions) says:

Valid method overriding:

If mtype(m, D) = E→E0 implies C = E and C0 = E0, then override(m, D, C→C0 )

How can mtype(m, D) = E→E0 imply C = E and C0 = E0? mtype(m, D) = E→E0 only means that class D has a method m whose type is E→E0.

Why is "mtype(m, D) = E→E0 implies C = E and C0 = E0" a condition for override(m, D, C→C0 )?

Thanks.

$\endgroup$
1
$\begingroup$

The important sentence in the first quote is

In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

So if you have

class C1 { ... }
class C2 { ... }

class Cls {
    C1 foo(C2 x) { ... }
}

override(foo, Cls, (C2)->C1) holds but override(foo, Cls, (C2)->C2) doesn't; the subclass

class SubCls extends Cls {
    C2 foo(C2 x) { ... }
}

is illegal. In FJ, you can't have

class SubCls extends Cls {
    C2 foo() { ... }
}

either, unlike in Java.

If mtype(m, D) = E→E0 implies C = E and C0 = E0, then override(m, D, C→C0 )

This is implicitly quantified "for all E and E0". If mtype(m, D) is undefined, then mtype(m, D) = E→E0 is always false, so it implies anything. If it's defined, then "mtype(m, D) = E→E0 implies C = E and C0 = E0" is equivalent to mtype(m, D) = C→C0.

So it ends up being the same as

If mtype(m, D) = C→C0 or mtype(m, D) is undefined, then override(m, D, C→C0)

(unless I went wrong somewhere)

| cite | improve this answer | |
$\endgroup$

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.