Re: [Caml-list] When do you need a subtype before :>?

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

From: tim@fungible.com (Tim Freeman)

> It seems that sometimes when I use :> I need to use the form
> 
>    (e :> t)
> 
> and sometimes I need to use this form:
> 
>    (e : t1 :> t2)
> 
> Can anyone tell me how to predict when I need the more complicated
> version?  I needed it in the code below, and that surprised me.

There are now lots of explanations in the tutorial (first part of the
reference manual). The basic has always been: with (e : t1 :> t2), the
system checks wether t1 is a subtype of t2, but with (e :> t) the
system builds a "generic enough" subtype of t (completely
independently of e!), and then unifies this type with the type of e.
Clearly, the first version is going to work more often.

While the above is enough to define (e : t1 :> t2), it is not enough
to define (e :> t); which "generic enough" subtype should be chosen?
To avoid exponential behaviour, the strategy was changed in 3.05,
and the rule is now: expand up to 2 object/variant + type abbreviation
sequences. That is, starting from the root of the type you are going
to subtype, you can only visit a branch which is a prefix of
   S* E* S* E* S*
where S represent subtypable types (objects or variants) and E the
expansion of a type abbreviation.
Additionally, if one of the expanded abbreviations is that of a
recursive class type, the recursion is kept in the newly built type.

Looks confusing? It is, but it happens to solve many cases, and to
produce readable types, which should be helpful whenever the
unification with the so-produced subtype fails.  It is also fast
enough that you shouldn't bother to use (e : t1 :> t2) when (e :> t2)
works. And hopefully we shouldn't have to change the definition
anymore.

Now, what happen in your case: in the first case you need to expand
eventdesc and eventtype, 2 expansions are OK. But in the second case
described_event is expanded first so you won't expand eventtype at all,
so you cannot subtype it. Too bad.
Note that this would be ok if eventdesc and described_event were not
object types, but either datatypes or abstract types: then they would
not be counted as (useless) subtyping themselves.

If you're going to use lots of object types in this way, then expect
to need lots of double coercions.

Cheers,

        Jacques


> module type CONSCIOUS = sig
>   type eventtype = [`VECTOR | `SCALAR | `UNIT]
>   type +'a type_constraint
>   class type [+'a] eventdesc =
>   object
>     method type_constraining_field: 'a type_constraint
>   end
>             
>   class type [+'a] described_event =
>   object
>     method desc: 'a eventdesc
>   end
>                           
> end
> 
> module Foo = functor (C: CONSCIOUS) -> struct
>   let _ =
>     let e: [`SCALAR] C.eventdesc = failwith "x" in
>     let f = (e (* No subtype needed here. *) :> C.eventtype C.eventdesc) in
>       ()
>       
>   let _ =
>     let e: [`SCALAR] C.described_event = failwith "ouch" in
>     (* The : [`SCALAR] C.described_event on the next non-comment line is
>        required, even though the same type appears on the previous
>        non-comment line. *)
>     let f = (e: [`SCALAR] C.described_event :> C.eventtype C.described_event)
>     in
>       ()
> end
-------------------
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