Re: Subtype problem

[Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp>]

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>