Xref: utzoo comp.object:3403 comp.lang.misc:7672 comp.lang.eiffel:1552
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1146@tetrauk.UUCP>
Date: 29 Apr 91 10:01:22 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU> <556@eiffel.UUCP>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 169

In article <556@eiffel.UUCP> bertrand@eiffel.UUCP (Bertrand Meyer) writes:
BM>In <554@eiffel.UUCP> I offered a straightforward Eiffel solution to
BM>Craig Chambers's problem, supposedly intractable by typed languages.
BM>
BM>Here now is the response by Craig Chambers:

CC> Eiffel's rules allow this to be type checked by having broken type
CC> checking rules, in my opinion.  Covariant type-checking rules do not
CC> enure type safety statically (you mention this towards the end of your
CC> message).  The newer proposed rules (as yet unimplemented, I believe)
CC> do ensure type safety statically, but by effectively enforcing a
CC> contravariant typing discipline which then prevents this example from
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ !?!
CC> being type checked.  I suspect that the new type checking rules will
CC> never actually be implemented and widely adopted since they will
CC> disallow many existing Eiffel programs which have relied on the
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ !?!
CC> covariant type checking rule.
CC> 
CC> The main purpose of my example was to convince fans of static type
CC> checking as done in most existing OO languages that these type systems
CC> are not powerful enough to describe relatively simple, useful programs
CC> (and preserve static type safety), and that OO language designers
CC> should incorporate more powerful type systems if they really want to
CC> claim that their type systems do not reduce expressive power over what
CC> exists naturally in dynamically-typed OO languages.

BM>I have quoted this text in full because I can't repress a feeling of
BM>admiration for the skill it takes to accumulate so many
BM>misrepresentations in so few lines. To call Eiffel's rules
BM>``contravariant'', for example, is a quite remarkable achievement.
BM>
BM>Not having the infinite amount of both time and patience which
BM>it would take to continue, I quit, declaring total rhetorical
BM>defeat.

I have avoided getting embroiled in this debate as I feel it has been rather
academic, and, like Bertrand, I don't have infinite time & patience.

However, the above attack on Eiffel's new type-checking system embodies so many
misunderstandings I feel compelled to take up the cause.  There have been a
number of passing criticisms of the concept, all of which have shown a lack of
understanding, but failed to discuss the issue in any depth.

Although I am usually averse to acronymns, I don't want to write "extended type
checking" or the like any more than I have to, so for now I shall christen it
"Global Type Analysis", or GTA for short (ETC sounds too trivial :-).  The
following explains why it can in fact work.


Fact:	A program is type-safe if no feature is ever called on an object which
	does not support that feature.

The problem is how to establish the truth of this.  The extremes are either a
completely unbreakable, simple static type system, or dynamic typing.  The
former is so strict it is unusable for non-trivial applications.  The latter
requires 100% branch coverage testing, or total static data-flow analysis, both
of which are either impossible or impractical.  They also require an embedded
run-time error trap system.  The compromise is GTA.

To understand what GTA does, it is useful to consider the idea of a partial
type.  Static type systems are always discussed in terms of complete types -
i.e. the type of an object is defined by the total set of features which it
supports.  However, an object can also be considered as having a number of
partial types, represented by all the possible subsets of its features.  Each
of these partial types is clearly a supertype of the complete type, or if you
prefer the other way, the complete type conforms to each of the partial types.

E.g. if object A supports features F, G, & H, then we can draw an implicit
partial type tree as follows:

		F         G         H
		|\       /|\       /|
		| \     / | \     / |
		|   F,G   |   G,H   |
		|    |    |    |    |
		|____|____|____|____|
			  |
			F,G,H

The total number of partial types is a function of the total number of
features, using the formulae from combination theory (which off the top of my
head I forget :-).

If we now consider a class variable in a program (i.e. one which can refer to
an object, whose actual type is dynamic), that variable has an IMPLICIT type.
The implicit type is defined by the set of features which are actually coded as
called from that variable.  This is true regardless of whether the language is
statically or dynamically typed.  If the language is statically typed, then the
variable also has an EXPLICIT type;  this is the complete type of the class for
which it is declared.  Simple static type checking will guarantee that the
implicit type is a supertype of the explicit type.

E.g.	if class A exports the features F, G, & H, then the declaration
	(Eiffel style):

	var: A

	defines var with an explicit type F,G,H.  If the only code which uses
	var if of the form:

	var.F; var.G;

	i.e. there is no occurrence of var.H, then the implicit type of var is
	F,G.

By contrast, the whole basis of a dynamically typed language is that all
variables are implicitly typed by their usage - there are no explicit types.

The "holes" in Eiffel's current type system, pricipally resulting from
covariance, are that it may allow var to refer to an object which is a
supertype of A.  However, var's implicit type is also a supertype of A.
Provided no object is ever attached to var which is a supertype of var's
IMPLICIT type, then the system is type-safe.  This analysis is statically
feasible, and is what GTA sets out to do.

The total effect is not a lot different from running a test with 100% branch
coverage.  Suppose in the above example, as part of a complete program, GTA
detected that an object could be assigned to var which did not support feature
G - it would generate a compile-time error.  The same scenario would only be
safe in a dynamically typed language if the code guaranteed never to call G at
the times when var referred to the offending object.  This implies that there
would be code which tested that object's actual type, and behaved accordingly.
This is contrary to all the principles of object oriented design, and suggests
that the program should be re-written.

Note that it does NOT mean that feature G can never be called on any object
which may at some time be attached to var.  It simply means that feature G must
be applied to those objects which support it via some other variable which
never references objects which don't support G.

It should also be noted that GTA resolves the infamous polygon/rectangle
problem.  Here we have a class POLYGON, whose number of vertices can be
altered.  A descendant of POLYGON is RECTANGLE, which is intuitively a
sub-type, but clearly must have a fixed number of vertices.  Thus RECTANGLE
inherits POLYGON, but does not export the add_vertex feature (and probably some
other non-applicable ones as well).  The effect in terms of types is that
RECTANGLE is not a subtype of POLYGON is terms of complete types, but it is a
subtype of a particular set of POLYGON partial types - those which exclude the
features inapplicable to rectangles.  Thus a variable of type POLYGON may
safely have a RECTANGLE object assigned to it provided the implicit type of the
variable is a supertype of RECTANGLE.  A program which includes an assignment
of a RECTANGLE object to a POLYGON variable of an invalid implicit type will be
caught be the GTA system.

This quite clearly does not "reduce Eiffel's type system to contravariance",
but allows covariance to be used completely safely.  It is worth noting that
Craig Chambers' "hard problem" is only irresolvable in a static type system if
you demand contravariance (which he did in his initial posting) - but then most
problems are irresolvable in a useful way with contravariance.  His point
really seems to be that static type checking with covariance isn't type
checking at all, so dynamic typing is better.  However, GTA allows covariant
flexibility combined with static checking, which in fact checks exactly the
same things that a dynamically typed language checks at run-time.

I do not wish to claim that "static typing is better than dynamic typing",
since such wars are futile - both forms have a useful place.  However, such
debate should focus on useful differences, not on prejudice and dogma.

As a footnote, I have written a lot of code in Eiffel over the last year or so,
with extensive use of genericity and polymorphism, and I have NEVER encountered
a covariance-induced type failure.  I would be extremely surprised if GTA
objected to any existing, reliably working Eiffel programs - if it did, they
would have shown up run-time failures by now.
-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK
rick@tetrauk.uucp

Any fool can provide a solution - the problem is to understand the problem