[comp.lang.eiffel] Types and redefinition

yh10@uk.co.gec-mrc (10/19/90)

I am currently trying to  model the semantics of a decent subset of
Eiffel as part of a postgraduate course. I am confused about how the
typing rules do or should work with features which are redefined in
descendants. Apologies if this is going over old ground but I am new to
Eiffel and this newsgroup. The language definition (in both OOSC and
Interactive's manuals) states that the types of formal parameters of a
routine which is redefined in a descendant must conform (most
specifically be a descendant of) to those of the original.  In changing
the type of a formal to be a descendant, the redefined routine is free
to make use of any extensions (most specifically extra exported
features) which the descendant has made to the class which it inherits
from.

Suppose that SPAM has a feature, f, which expects an argument of type
FOO. PLAP inherits from SPAM and redefines f to expect an argument of
type FUM, a descendant of FOO. But because of the polymorphism rules
any expression x.f(z) for which statically x:SPAM and z:FOO may find
itself in a dynamic situation where x:PLAP and z:FOO. The typing rules
will let this through, the compiler will generate code for it and if
there is no dynamic type testing (is there?) then catastrophe occurs.

Do I have the wrong end of the stick? What should happen?

Changing the type conformance rules to act in reverse for formal
parameters would make the language type safe (on this aspect) but
restrict the number of useful programs which could be expressed. For
example, under the assumption that the rules have been reversed for
formal parameters, if X has a field a:A and a feature set-a(x:A) which
updates the field, then Y inherits from X and redefines a:B, where B
inherits from A, then Y cannot redefine set-a nor use it sensibly!

It would appear that the typing rule for redefinitions has two options,
neither of which is satisfactory. Is the answer to prevent
redefinition, allow it but take the consequences, allow it but restrict
its usefulness, or what?

The following code conforms to the current language definition but is
type unsafe.

class FOO export
	a
feature
	a:INTEGER;

	Create is
		do
			io.putstring("Creating a FOO")
		end
end

class FUM export
	a, b
inherit FOO
feature
	b:INTEGER;

	Create is
		do
			io.putstring("Creating a FUM")
		end

end

class SPAM export
	f
feature
	f(x:FOO):INTEGER is
		do
			Result := x.a;
		end
end

class PLAP export
	f
inherit SPAM redefine f
feature
	f(x:FUM):INTEGER is
		do
			Result := x.b;
		end
end

class TEST
feature
	Create is
		local x:SPAM; y:PLAP; z:FOO
		do
			y.Create;
			z.Create;
			x := y;
			io.putint(x.f(z))
		end
end

Tony Clark