OOP (was Re: Extensible records)

[Jaroslav Tulach]

Hello,

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

Maybe. But what about uniquiness? For example this is not valid:

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

So by introducing inheritance difference between unique and non-unique
types can occur. So you are right that there is difference between 
"a | a => Int" and "Int". But I do not know any example where a
function could not take greater argument (a => Int) when it expects Int
if we do not allow modification to objects (arrays). Does anybody know?

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

Seems to be reasonable. But as I asked before: Is it only because of
unique arrays?

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

Hard to think it out, but here it is:

  GenR :: Real -> a | Real is a; // a <= Real 
  AddI :: Int a -> a | a >= Int; // Int <= a

  u = AddI 10 (GenR 1.0)

So if type of u is t, then    Int <= t <= Real
  
That is why I think that in a typing theory that allows subclass
restrictions (... | a is Point) you can get into problems with type
variables bounded from top and also from bottom.

I have saw such a theory I do not think I like it. If you are
interested, see:

http://cs-tr.cs.cornell.edu/TR/CORNELLCS:TR91-1230

This is the most complex work I've ever see. But the theory is a little
bit complicated...

Jarda

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