Re: co(ntra)-variant subtyping

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

From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>

> Didier Remy asked me for examples where the missing subtype rule
> for Adt's is a problem ...

> 1. Assume you have windows, which allow you to ask for their
> children:
[..]
> Now transient_window is not a subtype of window.

Probably not a very good example: I do not see here why children of
a transient window shall also be transient windows...

> 2. You can implement an automaton by modeling the states as
> objects :
> 
> class automaton : 'a = 
>   ...
>   method successor_state : 'a option
> end
> 
> Again it is not possible to built a subtype of an automaton. 

Better. There is still a way around, by raising an exception rather
than returning None, but agreedly this would not be very nice.

> This is actually more than I asked. For my application if would
> suffice if subtyping rules exist only for non-abstract types ie.
> variant and record types. There is no new syntax necessary for
> this, only a variance checker.

And this variance checker is included in O'Labl. So your examples
would work.

>    We did not want to add yet another notion in the language, and therefore 
>    we prefered to make all non-primitive type constructors non variant.
>    
> I see. And what about an optional variance syntax, just for those
> how want covariant lists? 

This is a possibility. In fact I proposed such a syntax to Didier a
while ago. It would be needed only for abstract types, and one might
also ommit it when not interested in a type's variance: since most
O'Caml libraries are anyway compiled from source, you can always add
this information later if you need it.

However, I shall add that for me, the true problem with subtyping
under constructors is the complexity of the subtyping algorithm. The
current algorithm can easily explode, and subtyping under constructors
makes it even easier. So the real question might be: is it reasonable
to have the typability of a program depend on its size ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>