Re: [Caml-list] Private types

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

From: "David Allsopp" <dra-news@metastack.com>

> Thanks for this - although it's a link to an OCaml 3.10 manual so not
> applicable here it did point me to the correct chapter in the OCaml 3.11
> manual (I'd been looking in Part I of the manual and given up). What I
> should have written is
> 
> string_of_int (x :> int)
> 
> Though that does make me wonder why the coercion is mandatory. What happens
> if I *want* to allow the use of M.t values as though they were ints and only
> want to guarantee that they come from a specific sub-set of the integers
> (I'm thinking of database row IDs which is what I want to use them for)?
> Assuming that the type abbreviation doesn't contain type-variables, would
> there be anything theoretically preventing the inclusion of two keywords:
> 
> type t = private int      (* can be used as though it were an int  *)
> type t = very_private int (* requires a coercion to be used an int *)

Explicit coercions in ocaml are completely unrelated to casts in C or
Java, in that they only allow upcast (cast to a supertype). They are
also completely erasable: they do not produce any code after type
checking. So they are not there for any soundness reason, but just for
type inference purposes. There would be no point at all in having two
constructs: if the 1st one were possible, we wouldn't need the second.

As for type inference, (x :> int) is already an abbreviated form of
(x : t :> int), that only works if x is "known" to be of type t.
Since ocaml type inference does not include subtyping, there is no way
to do without coercions. To explain this, you should just see how the
type checker handles
     string_of_int x
It fetches the type of the string_of_int, int -> string, fetches the
type of x, which is t, and tries to unify int and t.
Since there is no direction in unification, this can only fail, as int
and t are not equivalent, just related through subtyping.

Your intuition is correct that it would theoretically be possible to
try subtyping in place of unification in some cases. The trouble is
that thoses cases are not easy to specify (so that it would be hard
for the programmer to known when he can remove a coercion), and that
subtyping is potentially very costly (structural subtyping is much
harder to check than the nominal subtyping you have in Java.)
So the current approach is to completely separate subtyping and type
inference, and require coercions everywhere subtyping is needed.

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.

Cheers,

Jacques Garrigue