Re: [Caml-list] Private types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Edgar Friendly <thelema314@gmail.com>

> > So the current approach is to completely separate subtyping and type
> > inference, and require coercions everywhere subtyping is needed.
> > 
> Would it be particularly difficult to, in the cases where type [x] is
> found but type [y] is expected, to try a (foo : x :> y) cast?

If we limit ourselves to the case where both [x] and [y] contrain no
type variables, this si not particularly difficult. However whether
they will contain type variables or not depends heavily on how the
type inference algorithm proceeds.

If they contain type variables, then the situation becomes much more
muddled, as these type variables may get instantiated by the subtyping
check, and not necessarily as expected. So typing becomes rather
unpredictable...

> > You can also compare that to the situation between int and float.
> > For most uses, int can be viewed as a subtype of float. However ocaml
> > separates the two, and requires coercion functions whenever you want
> > to use an int as a float.
> > 
> Code isn't produced by a :> cast.  As the internal representation of int
> and float differs, a coercion function isn't required.  The internal
> representation of [private int] and [int] is the same, not to mention
> one is exactly the [private] of the other.

This was not intended as a complete comparison :-)
However, since the coercion function is canonical, I don't think that
this difference matters much here.

     Jacques Garrigue