I make some interpretations of statements by Shapiro, if those interpretations are faulty I apologize, that is not my intention.
> On Fri, 2005-02-11 at 09:01 -0500, Swaroop Sridhar wrote:
> > Let me illustrate the example by Cook, Hill and Canning:
> >
> > If the base class has type:
> > t1 = mu t. {eq: t->bool} // binary operator that compares
> > another object to self
> >
> > and the inhetited class has type:
> > t2 = mu t. {eq: t -> bool ; abc: someotherthing} // In t ->bool, t HAS
> > to be the child type
> >
> > Obviously, t2 not <: t1 (because of the t in function argument position).
>
> I think this mis-diagnoses the problem. The issue here is not subtyping
> with subclassing. The issue is how these interact with overloading.
> There is no plan at the present time to allow a subclass to alter the
> signature of a method defined in a superclass.
>
I agree that without signature refinement the type problem goes away,
but would like I remind you that programmers in object oriented languages
such as Java, C# and C++ use downcasting to work around the lack of
expressiveness in the type system.
If BitC programs use run-time downcasting rather than static type analysis by
the compiler, wouldn't that make program analysis harder? As well as
slow down programs due to the run-time checking?
It is my opinion that this is the case, but maybe you know something I don't.
On Fri, Feb 11, 2005 at 12:38:14PM -0500, Jonathan S. Shapiro wrote:
> In a polymorphic language, the issue above indicates that the programmer
> failed to implement eq correctly. The correct signature for
> extensibility purposes would be
>
> eq : 'a -> bool
>
> with a distinct implementation supplied by the subclass, but having
> precisely the same signature as the original.
>
I would like a precise notion of this polymorphism, but since 'a can
never be refined, eq can never use more information than was originally
available by type 'a, unless a dynamic cast is used to get the real
type of that argument.
With a row polymorphic type system one would have the precise definition
mu 'a . {eq: 'a -> bool,..}
Which states that any object with a eq method can be compared to itself,
and the object may have a bunch of methods, but that is unimportant for
the type of eq.
The other choice, which it appears that Shapiro as arguing for,
is to define a type comp that is comparable:
comp = mu comp . { eq : comp -> bool }
Now the object o would like to implement the method eq, and inherits
from comp, but provides a new implementation.
The problem is that inside this implementation the parameter only
supports the method eq, and a run-time cast must be deployed to recover
the actual type of the parameter.
What I suspect that Shapiro really want is a way to compare objects
from different classes, but then you are headed towards multi-methods.
An approach to this is described [1] by Chambers and Leavens.
Multi-methods either need to insert run-time checks to avoid illegal
combinations of objects, as well as recheck all inherited code,
or you get a complicated type system [1].
Matching is a more conservative approach.
For the sake of eq, either an object can only be compared to it's own
type, or there is a eq algorithm that uses a finite set of methods to
compute equality between any two kinds of objects.
Both these can be expressed with matching.
If you want an eq that can compare any types of objects, for which
there exists an implemented comparison method for just that
combination, then one requires multi-methods to do that without
run-time checks.
On Fri, Feb 11, 2005 at 12:38:14PM -0500, Jonathan S. Shapiro wrote:
> The real problem here is the introduction of contravariance and
> covariance, which was a mistake.
>
In light of my other comments, this statement does longer seem
reasonable, and I wonder if it is still valid?
If it is, can you please demonstrate the type system, because then I'm
quite curious!
One kind of polymorphism that solves these problems, without resorting
to objects, is extensional polymorphism, where eq can be overloaded
with different signatures.
With extensional polymorphism one could write eq as
type a = ...
type b = ...
type c = ...
generic rec eq =
int->int->bool => int_int_eq
a->b->bool =>...
b->a->bool => fun x y -> eq y x
a->a->bool =>...
b->a->bool =>...
c->c->bool =>...
With this type scheme one can control the overloading, such that one
can compare type a with type b, but one can only compare type c with
itself. With this kind of type system and expressibility I do not think
objects would be that useful, and extensional polymorphism is designed
to fit with the non-object oriented part of O'Caml.
On Fri, Feb 11, 2005 at 12:38:14PM -0500, Jonathan S. Shapiro wrote:
> In a polymorphic language, the issue above indicates that the programmer
> failed to implement eq correctly. The correct signature for
> extensibility purposes would be
>
> eq : 'a -> bool
>
To simply make eq universally quantified, polymorphic, would not permit
anything more
than matching, so this is clearly not what you mean.
As far as I understand you require either multi-methods or extensional
polymorphism, or something similarly expressive to capture what I
understand by your use of polymorphism.
Matching and type classes does not appear expressive enough.
[1] Craig Chambers and Gary T. Leavens, 1995
Typechecking and Modules for Multimethods
http://citeseer.ist.psu.edu/chambers95typechecking.html
--
Sincerely | Homepage:
J�rgen | http://www.hex.no/jhf
| Public GPG key:
| http://www.hex.no/jhf/key.txt
signature.asc
Description: Digital signature
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
