Subtype problem

Subtype problem

[Hendrik Tews]

Hi,

could somebody tell me, why

-------------------------Version 1---------------------------
class point x = 
  val mutable x = (x : int)
  method x = x
  method move (i : int) =  {< x = x + i >} 
end;;

class colored_point x c =
  val mutable x = (x : int)
  val color = (c : int)
  method x = x
  method move (i : int) = {< x = x + i >} 
  method color = color 
end;;

let p = ((new colored_point 2 1 :> point) : point)
-------------------------Version 1---------------------------

compiles without problem, while

-------------------------Version 2---------------------------
class point x = 
  val mutable x = (x : int)
  method x = x
  method move (i : int) =  Some {< x = x + i >} 
end;;

class colored_point x c =
  val mutable x = (x : int)
  val color = (c : int)
  method x = x
  method move (i : int) = Some {< x = x + i >} 
  method color = color 
end;;

let p = ((new colored_point 2 1 :> point) : point)
-------------------------Version 2---------------------------

produces an error? (The only difference is the move method, which
delivers an option in version 2). The error message is 

-------------------------Error-------------------------------
This expression cannot be coerced to type
  point = < x : int; move : int -> point option >;
it has type
  colored_point =
    < x : int; move : int -> colored_point option; color : int >
but is here used with type
  < x : int; move : int -> point option; color : int >
Type
  colored_point =
    < x : int; move : int -> colored_point option; color : int >
is not compatible with type point = < x : int; move : int -> point option >
-------------------------Error-------------------------------


Bye,

Hendrik

Re: Subtype problem

[Jacques GARRIGUE]

From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>

> Hi,
> 
> could somebody tell me, why
> 
> -------------------------Version 1---------------------------
> class point x = 
>   val mutable x = (x : int)
>   method x = x
>   method move (i : int) =  {< x = x + i >} 
> end;;
> 
> class colored_point x c =
>   val mutable x = (x : int)
>   val color = (c : int)
>   method x = x
>   method move (i : int) = {< x = x + i >} 
>   method color = color 
> end;;
> 
> let p = ((new colored_point 2 1 :> point) : point)
> -------------------------Version 1---------------------------
> 
> compiles without problem, while
> 
> -------------------------Version 2---------------------------
> class point x = 
>   val mutable x = (x : int)
>   method x = x
>   method move (i : int) =  Some {< x = x + i >} 
> end;;
> 
> class colored_point x c =
>   val mutable x = (x : int)
>   val color = (c : int)
>   method x = x
>   method move (i : int) = Some {< x = x + i >} 
>   method color = color 
> end;;
> 
> let p = ((new colored_point 2 1 :> point) : point)
> -------------------------Version 2---------------------------
> 
> produces an error? (The only difference is the move method, which
> delivers an option in version 2). The error message is 

Objective Caml's subtyping algorithm does not subtype under type
constructors (but it does it under abbreviations), for the sake of
efficiency. That is, eventhough colored_point :> point, you don't have
colored_point option :> point option. This equation would be needed to
check the subtyping in method move of example 2.

By the way, Objective Label does it, so that

	let p = (new colored_point 2 1 : colored_point :> point)

would work for the second example. You need to write a complete
coercion (with both types), since doing this for partial coercions
would lead to huge types, and very slow inference.

	Jacques

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

co(ntra)-variant subtyping

[Hendrik Tews]

Hi,
   
   Objective Caml's subtyping algorithm does not subtype under type
   constructors (but it does it under abbreviations), for the sake of
   efficiency. That is, eventhough colored_point :> point, you don't have
   colored_point option :> point option. This equation would be needed to
   check the subtyping in method move of example 2.
   
I must say I am really surprised.  

How about object types? Do they support co(ntra)-variant
subtype rules?

I would suggest to include a section about the subtype relation
in the ocaml documentation. Because IMHO anybody how knows
something about formal models for oo languages would expect
co(ntra)-variant subtype rules. 

In summary I think the lack of these subtype rules are a major
restriction of the ocaml language. Now it is not possible to mix
class types and (algebraic) data types in an application. Instead
a user has to decide beforehand what is more important for him:
algebraic data types and parametric polymorphism or object types
with code reuse and stepwise refinement.

Are there any plans to add the missing subtype rules to the type
system of ocaml?

Bye,

Hendrik

Re: co(ntra)-variant subtyping

[Didier Remy]

>    Objective Caml's subtyping algorithm does not subtype under type
>    constructors (but it does it under abbreviations), for the sake of
>    efficiency. That is, eventhough colored_point :> point, you don't have
>    colored_point option :> point option. This equation would be needed to
>    check the subtyping in method move of example 2.
>    
> I must say I am really surprised.  
> 
> How about object types? Do they support co(ntra)-variant
> subtype rules?

As Jacques said, subtyping sees through abbreviations.
Object types are abbreviations. 
They are covariant except when self-type occurs negatively, in
which case they are non-variant.

> I would suggest to include a section about the subtype relation
> in the ocaml documentation. 

We are aware that the documentation is too succinct. 
We will keep improving it. 

> Because IMHO anybody how knows
> something about formal models for oo languages would expect
> co(ntra)-variant subtype rules. 

I leave you this opinion.

Traditionally, people have heavily relied on subtyping polymorphism; they
run into serious difficulties because of the bad interaction between
recursion, late-binding and contra-variance. This lead to some mistakes
(some languages got it wrong). Moreover they still have difficulties with
binary methods.  For instance, even though Java is explicitly typed, it
fails to type binary methods: the type of self is weakened to the current
type of the class, which forces later useless and unsafe coercions (they may
fail, dynamically).

Instead, Objective Caml relies on parametric polymorphism.  This is easier to
explain, often more powerful (here, binary methods are not a problem) and
allows simple type inference. This is really what makes Objective Caml work.
Actually, Objective Caml does work with no subtyping at all, i.e.  polymorphic
message invocation, inheritance, binary methods, etc. all work without
subtyping.  Indeed, many examples do not use subtyping at all.

Still, Objective Caml allows subtyping because they are a few situations
when it is  convenient. Typically, when storing a collection of
objects of different subclasses of a common parent class into a bag.  Then,
only the operations of the parent class can be directly invoked on the
objects of the collection. (Actually, subtyping is independent from the
class hierarchy and objects do not need to be in an inheritance relation to
be put in the same collection.)

> In summary I think the lack of these subtype rules are a major
> restriction of the ocaml language. 

I am not convinced that the current restriction is such a burden. 
You are one of the first person to complain...

> Now it is not possible to mix
> class types and (algebraic) data types in an application. Instead
> a user has to decide beforehand what is more important for him:
> algebraic data types and parametric polymorphism or object types
> with code reuse and stepwise refinement.

Maybe you could detail your examples.

> Are there any plans to add the missing subtype rules to the type
> system of ocaml?

In fact, there is no real difficulty to allow subtyping through
user-declared type constructors.  However, when types are abstract (e.g. in
module interfaces) the user would need to declare the variances of the
constructors in their arguments.

We did not want to add yet another notion in the language, and therefore 
we prefered to make all non-primitive type constructors non variant.

   Didier

Re: co(ntra)-variant subtyping

[Hendrik Tews]

Hi,

Didier Remy asked me for examples where the missing subtype rule
for Adt's is a problem ...

1. Assume you have windows, which allow you to ask for their
children:

class window : 'a =
  ...
  method children : 'a list
end

Now you can have a special kind of windows, which have special
children as well:

class transient_window : 'a =
  ...
  method children : 'a list
end

Now transient_window is not a subtype of window.

2. You can implement an automaton by modeling the states as
objects :

class automaton : 'a = 
  ...
  method successor_state : 'a option
end

Again it is not possible to built a subtype of an automaton. 

Didier Remy writes:

   Still, Objective Caml allows subtyping because they are a few situations
   when it is  convenient. Typically, when storing a collection of
   objects of different subclasses of a common parent class into a bag.  Then,
   only the operations of the parent class can be directly invoked on the
   objects of the collection. 

Right. And you might use an Adt like the builtin lists for this
bag. But then a list of colored points can not be appended to a
list of points. 
   
   In fact, there is no real difficulty to allow subtyping through
   user-declared type constructors.  However, when types are abstract (e.g. in
   module interfaces) the user would need to declare the variances of the
   constructors in their arguments.
   
This is actually more than I asked. For my application if would
suffice if subtyping rules exist only for non-abstract types ie.
variant and record types. There is no new syntax necessary for
this, only a variance checker.

   We did not want to add yet another notion in the language, and therefore 
   we prefered to make all non-primitive type constructors non variant.
   
I see. And what about an optional variance syntax, just for those
how want covariant lists? 

Bye,

Hendrik

Re: co(ntra)-variant subtyping

[Didier Remy]

> 1. Assume you have windows, which allow you to ask for their
> children:
> ...
> Now transient_window is not a subtype of window.
>
> 2. You can implement an automaton by modeling the states as
> objects :
> ...
> Again it is not possible to built a subtype of an automaton. 

This is right.  You could only get deep subtyping if list and option
data-structures were implemented as objects (since then their types would be
abbreviations to objects types instead of data-types).

It is clear that the use of concrete data-types is better than objects here.
Concrete data-types are one of the nice features of ML, and we certainly do
not want to discourage (or limit) their use.

>    In fact, there is no real difficulty to allow subtyping through
>    user-declared type constructors.  However, when types are abstract
>    (e.g. in 
>    module interfaces) the user would need to declare the variances of the
>    constructors in their arguments.
>    
> This is actually more than I asked. For my application if would
> suffice if subtyping rules exist only for non-abstract types ie.
> variant and record types. There is no new syntax necessary for
> this, only a variance checker.

Your demand for covariant type-constructors is fair.

However, it is clear to me that restricting variances to concrete data-types
is just one small step forward and would not be  that satisfactory.

Today you only need covariance for non-abstract types, because you use lists
to collect windows.  But tomorrow, you'll create thousands of windows, and
you'll want to replace lists by sets or maps. Then you will need covariant
*abstract* type constructors.

The good solution is certainly to have variances, and explain them to the
user. We might consider such an extension in the future.

Thanks for you input.

Regards,

    -Didier

Re: co(ntra)-variant subtyping

[Jacques GARRIGUE]

From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>

> Didier Remy asked me for examples where the missing subtype rule
> for Adt's is a problem ...

> 1. Assume you have windows, which allow you to ask for their
> children:
[..]
> Now transient_window is not a subtype of window.

Probably not a very good example: I do not see here why children of
a transient window shall also be transient windows...

> 2. You can implement an automaton by modeling the states as
> objects :
> 
> class automaton : 'a = 
>   ...
>   method successor_state : 'a option
> end
> 
> Again it is not possible to built a subtype of an automaton. 

Better. There is still a way around, by raising an exception rather
than returning None, but agreedly this would not be very nice.

> This is actually more than I asked. For my application if would
> suffice if subtyping rules exist only for non-abstract types ie.
> variant and record types. There is no new syntax necessary for
> this, only a variance checker.

And this variance checker is included in O'Labl. So your examples
would work.

>    We did not want to add yet another notion in the language, and therefore 
>    we prefered to make all non-primitive type constructors non variant.
>    
> I see. And what about an optional variance syntax, just for those
> how want covariant lists? 

This is a possibility. In fact I proposed such a syntax to Didier a
while ago. It would be needed only for abstract types, and one might
also ommit it when not interested in a type's variance: since most
O'Caml libraries are anyway compiled from source, you can always add
this information later if you need it.

However, I shall add that for me, the true problem with subtyping
under constructors is the complexity of the subtyping algorithm. The
current algorithm can easily explode, and subtyping under constructors
makes it even easier. So the real question might be: is it reasonable
to have the typability of a program depend on its size ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>