To: tews@tcs.inf.tu-dresden.de
Subject: Re: Subtype problem
In-Reply-To: Your message of "Wed, 20 May 1998 17:00:12 +0200"
<199805201500.RAA19129@ithif18.inf.tu-dresden.de>
Message-Id: <19980522112157L.garrigue@kurims.kyoto-u.ac.jp>
Date: Fri, 22 May 1998 11:21:57 +0900
From: 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>
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:14 MET