Version française
Home     About     Download     Resources     Contact us    
Browse thread
[Caml-list] set of sets ...
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John Prevost <j.prevost@g...>
Subject: Re: [Caml-list] set of sets ...
In short, your problem is this:

Say you have two types, t1 and t2, and t1 is a subtype of t2. 
Therefore, you can do (x : t1 :> t2) and coerce a value of type t1 to
a value of type t2.  You cannot do (x : t2 :> t1).  That's pretty
basic.  Let's make an example:

type t1 = [ `A ]
type t2 = [ `A | `B ]
let t1_to_t2 (x : t1) = (x :> t2)

let x1 = `A
let x2 = `B
let x3 = t1_to_t2 x1

There.  That's easy.  It all works and types okay.  The problem is at
the next level.  Let's look at the type of your "store" class:

class virtual ['a] store :
  object ('b)
    method virtual access : 'a ext_rep
    method virtual add : 'a -> unit
    method virtual assign : 'b -> unit
    method virtual copy : 'b
    method virtual del : 'a -> unit
  end

To see what the problem is, let's make some smaller examples with
similar features:

class ['a] c1 (v : 'a) =
  let x = ref v in
  object
    method get = !x
    method put v = x := v
  end

let o1t1 = new c1 x1
let o1t2 = new c1 x2
let o1t3 = new c1 x3

val o1t1 : t1 c1 = <obj>
val o1t2 : t2 c1 = <obj>
val o1t3 : t2 c1 = <obj>

Okay.  So that's working well.  Now--we know we can cast t1 to t2. 
Can we cast (t1 c1) to (t2 c2)?  Let's see:

# let o1t1_t2 = (o1t1 :> t2 c1);;
This expression cannot be coerced to type
  t2 c1 = < get : t2; put : t2 -> unit >;
it has type t1 c1 = < get : t1; put : t1 -> unit > but is here used with type
  < get : t1; put : ([> t2 ] as 'a) -> unit; .. >
Type t1 = [ `A ] is not compatible with type 'a = [> `A | `B ]
The first variant type does not allow tag(s) `B

Looks like no.  Why not?  Well, let's think about it.  What happens if
we get a value out of this object?  The value is going to be `A,
because the initial object contains type t1.  That's fine--if we give
`A to something that expects `A or `B, it can handle it.  What happens
if we put a value into this object?  Well, we can only put `A into it.
 Aha!  Here is the problem!

You can't use the value `B in a spot where only `A is expected to be! 
Because the "put" method of o2 c1 takes `A|`B, and the "put" method of
o1 c1 only takes `A, we cannot cast a value of type (o1 c1) to (o2
c1)--if we did, we could give the object to code that wants to put `B
into it.  This is called "contravariance", and you can identify it by
looking at the type signature.  If a type argument appears on the
right side of the arrow (or there is no arrow), that type is
"covariant", and behaves as you were expecting.  But if the type
argument appears on the left side of an arrow, it is
"contravariant"--it works the opposite way from what you were
expecting.  If in a single type it is on *both* sides of the arrow,
then it is *invariant*.  That is the case here.

With c1, look at the type:

class ['a] c1 : 'a -> object
  method get : 'a
             (* ^^ this indicates covariance, 'a is on the right *)
  method put : 'a -> unit
             (* ^^ this indicates contracariance, 'a is on the left *)
end

Because c1 is invariant in the type argument 'a, it doesn't matter
that t1 is a subtype of t2.  The rules are like this:

If 'a is covariant in class c, then (t1 <: t2) implies (t1 c <: t2 c)
If 'a is contravariant in class c, then (t1 <: t2) implies (t2 c <: t1 c)
If 'a is invariant in class c, then neither holds, unless t1 = t2.

To make things a little more clear, let's break that down:

class ['a] covariant (x : 'a) = object  method get = x  end
class ['a] contravariant = object  method put (x : 'a) = ()  end

class ['a] covariant : 'a -> object method get : 'a end
class ['a] contravariant : object method put : 'a -> unit end

Let's make some covariant objects and cast them:

let covariant_t1 = new covariant x1 (* OK *)
let covariant_t2 = new covariant x2 (* OK *)
let covariant_t1_as_t2 = (covariant_t1 :> t2 covariant) (* OK *)
let covariant_t2_as_t1 = (covariant_t2 :> t1 covariant) (* Error *)

t2 covariant is not a subtype of t1 covariant, so that last is an
error.  Now we look at contravariant:

let contravariant_t1 = (new contravariant : t1 contravariant) (* OK *)
let contravariant_t2 = (new contravariant : t2 contravariant) (* OK *)
let contravariant_t1_as_t2 = (contravariant_t1 :> t2 contravariant) (* Error *)
let contravariant_t2_as_t1 = (contravariant_t2 :> t1 contravariant) (* OK *)

So here, the other case holds.  And above, in the sample class c1,
both constraints were there, and things didn't work out.

As a final note, you can cast out the offending methods to get around
this.  For example, if you use casting to remove the contravariant
methods from an object of your store class, you can then use the
resulting object covariantly (only reading data out of the object.) 
If you use casting to remove the covariant methods from an object of
your store class, you can then use the resulting object
contravariantly (only writing data into the object.)

John.

-------------------
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