Xref: utzoo comp.object:3363 comp.lang.misc:7619 comp.lang.eiffel:1541
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!think.com!snorkelwacker.mit.edu!stanford.edu!agate!ucbvax!dog.ee.lbl.gov!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <554@eiffel.UUCP>
Date: 25 Apr 91 23:13:09 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 110

From <1991Apr20.010347.28984@leland.Stanford.EDU>
by craig@leland.Stanford.EDU (Craig Chambers):
> 
> Here's a simple example that cannot be described by a static type
> system in most statically-typed object-oriented languages.  I'm using
> it to help me make sure that the static type system in my new OO
> language is sufficiently powerful.
> 
> Here's the problem: we'd like to describe the type of the min
> function, so that this one piece of source code can be used to compute
> the minimum of two numbers or of two collections of numbers or of two
> collections of collections of numbers, etc.
> 
> So here are some examples that should type-check:
> 
>     min(3, 4)
>     min(3, 4.5)
>     min({3,4}, {4,5,6})
>     min({{3,4.5},{5},{6,8.9}}, {{1.2,4},{2}})
> 
> And here are some that shouldn't:
> 
>     min(3, {4})
>     min({3,4}, {{4,6},{2,3.4,6}})

I don't know about ``most statically-typed object-oriented
languages'' but in Eiffel this does not appear particularly
difficult. Class COMPARABLE describes order relations;
one could define `min' in that class as

	min (other: like Current): like Current is
			-- Minimum of current element and `other'
		do
			if Current < other then
				Result := Current
			else
				Result := other
			end
		end -- min

In COMPARABLE, the operator "<" means a call to the following
function:

	infix "<" (other: like Current): BOOLEAN is
			-- Is current element less than or equal to `other'?
		deferred
		end -- "<"

Then INT, FLOAT and SORTED_LIST (a generic class) may inherit
from COMPARABLE and provide an effective declaration for infix "<". 

The ``like'' keyword used in these declarations is one of the key parts
of the type system, known as anchored declarations.
What it means is that `other' and the result
of `min' must be of the same type as Current (the current object),
even if redefined in a descendant class. In SORTED_LIST [X], for example,
the actual argument to both of the above functions must also
be of type SORTED_LIST [X], or a conforming (descendant) type.
Anchored declarations of this kind are what makes typing possible and
useful; they directly reflect the covariant rule, without
which typing, in our experience, would not work.


With the proper declarations for arguments a and b, the call
a.min (b) for the six examples given by Mr. Chambers will yield
the desired behavior: acceptance in the first four cases, rejection
in the last two. This assumes the following declarations (respectively):

1	a, b: INT
2	a: INT; b: FLOAT
3	a, b: SORTED_LIST [INT]
4	a, b: SORTED_LIST [SORTED_LIST [INT]]
 
5	a: INT; b: SORTED_LIST [INT]
6	a: SORTED_LIST [INT]; b: SORTED_LIST [SORTED_LIST [INT]]
	

In the last two cases, you can cheat the type system in Eiffel 2.3
by declaring for example a and b as being of type COMPARABLE,
and then assigning to them the values given in the corresponding examples.
This is because the detection of such erroneous cases requires
system-level checking (as opposed to class-level checking), which will
only be provided in Eiffel version 3. However such cases occur rarely except
if specially contrived.

Eiffel 3 will also have two properties which are relevant to this
discussion:
-  

	- It will be possible to anchor a function result to an argument
	of the function. In function `min', for example, it will be possible
	to declare the function result as being of type `like other',
	which provides more flexibility than `like Current'.
	(With the above declaration, if `n' is integer and `r' real,
	you have to write a call as r.min (n) rather than n.min (r);
	with the relaxed rule both are possible.

	- Support for manifest arrays makes it possible to write
	examples  such as min({3,4}, {{4,6},{2,3.4,6}}) in almost
	exactly this syntax, with << for the opening brace and
	>> for the closing brace. The rule is that <<a, b, ...>>
	conforms to ARRAY [T] for any T for which all of a, b, ...
	conform to T. This will mean that even without any
	entity declarations (of the forms numbered 1 to 6 above)
	the type checking will yield the desired effect. 

-- 
-- Bertrand Meyer
Interactive Software Engineering Inc., Santa Barbara
bertrand@eiffel.uucp