From: Damien <Damien.Pous@ens-lyon.fr>
> On Thu, 05 Feb 2004 18:18:45 +0900 Jacques Garrigue wrote:
> 
> > Because instanciation/specialization only works for values, not for
> > types.
> > This is reasonable enough: once you have defined a type, you may use
> > it both in covariant and contravariant positions, so allowing to
> > specialize it would be unsound.
> > (So, yes, in the long run this is a soundness problem.)
> 
> I don't see the point :-(
> 
> module type O = 
> sig
> 	type " t :> o "
> end
> 
> can be read as
> 
> module type O =
> sig
> 	type ellipsis (* abstract *)
> 	type t = " <o; ellipsis> "
> end
> 
> therefore, a functor F(M: O) cannot create objects of type t without the
> help of M. 

I see.
This way you can coerce from t to o, but not the other way round.
The trouble is just that in ocaml, the row variable of an object type
is not a type in itself (even if it uses the same datatype
representation in the compiler).
There are actually three possible row-endings:
  Tvar -> an extensible row, as the one in "#o"
  Tnil -> a closed row, as in "o"
  Tunivar -> an existential row variable, unifies only with itself,
          and must be bound locally. used for polymorphic variables in
          polymorphic methods.
What you are asking for is actually adding a 4th form,
  Tconstr (path, args, memo) ->
      extension through a type (abstract or concrete) 
Not only would this require to extend all existing handling of
row-endings (which occur in many places in the compiler), but this
should also include the possibility that the extension is concrete
(needed as you want to be able to add methods through functor
application), and should be expanded when looking for a method. This
breaks another assumption in the compiler (that no expansion is needed
to access the method types.)

But all this technical part is possible.
The real question is: would it be useful?
Note that compared to a class-based approach, the extensibility would
still be weaker: in declaration
   type ('a1,..,'an) t :> ('a1,..,'an) o
only the type variables 'a1 to 'an can be used in extra methods.
This is a well-known problem with functors, but would be even more
problematic if we allow this kind of semi-abstract types.

For all these reasons, your idea, while theoretically interesting,
does not attract me so much: lots of work for a rather weak result,
while there are already simpler ways to do the same thing.

Jacques Garrigue

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