Re: [Caml-list] type checking divergence for coercion

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

From: zze-MARCHEGAY Michael stagiaire FTRD/DTL/LAN <michael.marchegay@rd.francetelecom.com>

> In the following exemple:
> 
> class x = object
>   method bar (x0:a0) (x1:a1) (x2:a2) (x3:a3) (x4:a4) (x5:a5) (x6:a6) (x7:a7)
> = 
>     (x0, x1, x2, x3, x4, x5, x6, x7)
> end        
> 
> and a0 = object inherit x end 
> and a1 = object inherit x end 
> and a2 = object inherit x end 
> and a3 = object inherit x end 
> and a4 = object inherit x end 
> and a5 = object inherit x end
> and a6 = object inherit x end
> and a7 = object inherit x end
> 
> let _ = (new x :> x)
> 
> the computation time required to evaluate the type of the expression 
> "let _ = (new x :> x)" diverges when paramters are added to the method bar.
> 
> Do you have any idea on the origin of this divergence?

I already answered to your (identical) bug report.
This is related to the way the type checker computes the type of
     let f o = (o :> x)
Here is the type if you stop at a1:
val f :
  < bar : a0 ->
          a1 ->
          < bar : a0 -> a1 -> a0 * < bar : a0 -> a1 -> a0 * a1; .. >; .. > *
          < bar : a0 -> a1 -> < bar : a0 -> a1 -> a0 * a1; .. > * a1; .. >;
    .. > ->
  x = <fun>
Clearly, the size is exponential in the number of a's. Try with a2 :-)
This is not a bug, but the specification of simple coercions.

The workaround is clear: use a double coercion.
  let f o = (o : a1 :> x);;
  val f : a1 -> x = <fun>
Here computation time should be at most quadratic, I believe.

Regards,

Jacques Garrigue

P.S. Could you deselect the "send also HTML" in your mailer.
This makes your mails hard to read.
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners