OOP (was Re: Extensible records)

[Jaroslav Tulach]

On Mon, 10 Nov 1997 jan@chipnet.cz wrote:

Hello,
here is my reaction.

#>   :: OneWay a b = { oneWay :: a -> b }
#>   :: RoundTrip a b = { OneWay a b & backWay :: b -> a }
#> 
#
#Yes I see the problem though I do not know how to solve it.
#All I'm able to think up is another restriction,
#"the subtype's typevariables must have the same properties 
#as are the supertype's". It seems as a rather cruel restriction
#but currently it seems to me it's the only posible solution.
#
#BUT, we HAVE TO BE ABLE TO explicitly STATE the requested properties.
#Say
#  +a  = covariant variable
#  -a  = contravariant variable
#  ^a  = both
#
#so
#  :: OneWay a b = { oneWay :: a -> b }
#
#leads to
#
# :: OneWay +a -b
#
#and
#
# :: RoundTrip a b = { OneWay a b & backWay :: b -> a }
#
#
#would lead to
#
# :: RoundTrip ^a ^b

Good idea to explicitly mark type variables. Moreover it is not as hard
to determine these marks by the compiler. By the way the +, - and ^
signs are nice :-) 

#
#which will be refused by the typechecker.
#If we would want to be able to extend the OneWay
#as in RoundTrip we would have to define it as 
#  :: OneWay ^a ^b = { oneWay :: a -> b }
#



But I am not sure if this is necessary. I have read one interesting
article:
  Title Inheritance is not subtyping
  Authors William R. Cook, Wlter L. Hill, Peter S. Canning
  Source Proceedings of Principles of Programming Languages, 1990, pages 125 - 135

And the authors claim that it is not neccessary that subclass must be
subtype. It is a little strange when one works with C++, Java, ... but
only for the first sight. It is not a bad idea that you create subclass
and use a lot of code it provides but you are not able to pass it to
functions that need the super class because you did not create
subtype...




#>   Is Circle Int subclass of Point Int Int?
#It should be if we think of the way it was constructed, but it cannot
#be.
#Just think about the type of functions. Say the old move.
#
#move :: (a,b) (obj a b) -> (obj a b) | obj is Point
#
#Now how does "Circle a" fit in there? 
#"Circle a" simply doesn't match (obj a b).
#I think that we would have to restricts
#extensions to the same or greater numer of type variables.

This restriction is a good idea but I would like to handle the
previously mentioned example too.

You are right that
#"Circle a" simply doesn't match (obj a b).
but it does not match it only simply. When I create the hierarchy of
types I used graphs to describe it:

    Point (|) (|) >>> Object
           |   |    so point is something that take two variables
           |   |    and extends the base Object
           a   b

But circle is something that takes only one variable but extends Point
by sharing this variable. Then also it extends the base Object

   Circle (|)  >>> Point (|) (|) >>> Object
           |--------------|   |
           |------------------|
           |
           a

When one thinks about types as graphs it is not too hard to find if two
graphs maps if Circle a >= Point a a. The example of the move function
I would like to write as

  move :: (a, b) obj -> obj | obj is Point a b;

And circle would satisfy it. Because it is realy point.


#:: Circle a = { Point a a & r :: a}
#would raise an error. This may seem overly restrictive, but seems
#necessary.

I hope that it is not necessary.

#So the proper extension would be :
#
#:: Circle c a b = { Point a b & r :: c}
#
#If we apply move to (x :: Circle Real Int Int) we map the variables in
#move's type 
#as follows :
#  a = Int
#  b = Int
#  obj = Circle Real
#
#which means Circle Real is Point.
#That is subtype of "Point" is not "Circle", but "Circle a" !

Nice. But if we could write the move function like
  move :: (a, b) obj -> obj | obj is Point a b;
not necessary. At least I hope.

#>   When a is subclass of b is Circle a subclass of Point b?
#> 
#
#To tell the truth I didn't think about such affairs much.
#

What about default clean's structures?
It is obviouse that Int <= Real. Is it true that [Int] <= [Real]? I
think so. But it can be more complicated with uniqueness typing and
possiblity that the structure can be modified:

   {Int} <= {Real}  // true, if only reading is allowed
  *{Int} <= *{Real} // false, you cannot treat array of Real as array
										// of Int because you could try to write class
                    // that extends Int but not Real to it and it would
                    // raise in runtime exception
(btw. this problem can occur in Java too)

#
#
#> The a is Point is good construct but because of covarince we need also
#> another. I have found out that sometimes it is needed to restrict the
#> variable from up and also from down.
#> 
#> Example:
#> 
#>    move :: .... | a is Point & Circle is a
#
#I don't think this is reasonable. The type Circle may have been
#unknown in time of move's definition.

I am sorry, but I did not express quite sharply.

When I am typing an expression I create list of inequalities (in
opposite to typing without subtypes where list of equelities is
constructed).

Example:
  expression: 5 + 10.3
  where: 5 :: Int, 10.3 :: Real, (+) :: a a -> a | + a
  inequalities:
    Int <= a (because 5 is applied as first arg)
    Real <= a (because 10.3 is applied as second)
  because Int <= Real <= a then a can be anytype that subclasses Reals

But suppose that they can occur two restrictions for the same variable
but one from about and one from down. This could occur when the result
of previous expresion is used in another computation then

  Real <= a <= sometype

That is what I wanted to say. Sometimes you do not need subclass, but
sometimes you need superclass and sometimes something between.

At least I think. If someone could me show that I am not right, I would
be very pleased because this is the problem that does not allow me to
finish my thesis.


Jarda

/**
* @author   Jaroslav Tulach
* @see      http://www.kolej.mff.cuni.cz/~tulach
*/