OOP (was Re: Extensible records)

[jan@chipnet.cz]

Jaroslav Tulach wrote:

> 

> Hello,

> I tried to study problem of inheritance in typing theory in my master

> thesis. I still not finished it but here I some comments I noticed.

> 

> #I think that to allow true OOP in cleant we should add one more feature

> #:

> #Extensible records. I mean something like

> #

> # :: Point = {x :: Real;y :: Real}

> #

> # :: Circle = { Point & r :: Real}

> 

> Extensible records could solve some problems but the examples are too

> restrictive. 

Well they were such on purpose, I do not know how to treat polymorphic

types.



> Here are some more complex:

> 

>   :: Point a b = { x :: a, y :: b }

>   // point on 2D with coordinates of different types

> 

>   :: Circle a = { Point a a & r :: a }

>   // circle that extends point but with the same type of coordinates

> 

> This examples should illustrate the problems that arrives when one does

> not restrict himself to type without type variables. Because of following

> questions:

> 

>   Is Circle Int subclass of Point Int Real?

Well, I shouldn't be.



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



:: Circle a = { Point a a & r :: a}

would raise an error. This may seem overly restrictive, but seems

necessary.

We are extending the record, so we have to extend or at least leave

intact

also the type constructor.



Now let's think about where should we add the new typevariables.

In front of the old ones or behind them?



If we add them behind we still will not be able to match

the new type to expressions like "(obj p1 p2) | obj is Point".

:: Circle a b c = { Point a b & r :: c}



Leads to

 obj = Circle a

 p1 = b

 p2 = c

 but this is wrong cause the Point in the Circle is of

 type Point a b, not of type Point b c as we say here.



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" !



And it works beautifully, we know the types of fields we work

with (that is all fields present in Point record) and treat the 

rest as a buch of bytes we only have to copy.





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



> Please notice that these are simple questions but they can be complicated

> as I show in following cases:

> 

>   :: OneWay a b = { oneWay :: a -> b }

>   :: RoundTrip a b = { OneWay a b & backWay :: b -> a }

> 

> This example is about variance and covariance of arguments (I will write a

> <= b if b is subclass of a). Here is the major rule for covariance:

> 

>   a => c & b <= d  then  a -> b <= c -> d

> 

> This rule can be obtained when one thinks about how subclassing of

> parameters influence subclassing of whole funcitions.

> 

> >From it we have:

> 

>   a => c & b <= d then (OneWay a b) <= (OneWay c d)

> 

> But we should realize that for RoundTrip the conditions are more

> restrictive.

> 

>   If RoundTrip a b <= RoundTrip c d then the only possible solution for

>   this problem is that a == c and b == d.

> 

> #  move :: (Real,Real) a -> a | a is Point

> 



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

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 }



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


> 

> Jarda


Jenda