OOP (was Re: Extensible records)

jan@chipnet.cz jan@chipnet.cz
Tue, 11 Nov 1997 10:43:59 +0100


Jaroslav Tulach wrote:
> 
> On Mon, 10 Nov 1997 jan@chipnet.cz wrote:
> 
> Hello,
> here is my reaction.
> 
> #
> #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...

I see. So RoundTrip ^a ^b would be a subclass of OneWay +a -b, but not a
subtype.
Well why not, but the compiler should at least give a warning, since
usually you do not think about the subclass/subtype difference and then
you 
could have a very hard time to find why doesn't it work.

> #>   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.
> 

:: Circle1 a :== Circle a a  ?

> 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:
>
> <snipped> 
>
> 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.
> 

Very nice, thanks.

> 
> #>   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)

Well, I think this only shows the difference between
"a | a => Int" and "Int".

setI :: a Int {Int} -> {Int} | a => Int

 X

getI :: Int {a} -> Int | a => Int

arr={3.5,6.7}

getI 1 arr   -->  3
set 1.2 1 arr  -->  type error, arr is not of type {Int}

So the question is not whether {Int} <= {Real}, but
what exactly is the type of a function. We may not allow implicit
subtyping,
we must be able to differ Type from (a | a => Type)!

Simply if I say I want Int, I must get an Int. If I say I want anything
=> Int, I get any subclass of Int.

> 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

Could you give me an example? Thanks.

> 
> Jarda
> 
Jenda