Re: [Caml-list] Re: module typing issue

[Guillaume Yziquel <guillaume.yziquel@citycable.ch>]

Le Monday 28 Mar 2011 à 11:29:51 (+0000), David Allsopp a écrit :
> Guillaume Yziquel wrote:
> > Le Monday 28 Mar 2011 à 09:53:52 (+0200), Alain Frisch a écrit :
> > > On 03/25/2011 08:01 PM, Guillaume Yziquel wrote:
> > > >type error = private int
> > > >
> > > >external get_error : unit ->  error = "zzz"
> > > >
> > > >You get some error level that you can pattern match as an int, and
> > > >this also enforces that all values of type error come from a call to
> > > >get_error.
> > >
> > > You need to coerce explicitly from type error to type int (... :>
> > > int), so this is not really different from defining error as an
> > > abstract type and exposing a function error->int.
> > >
> > > -- Alain
> > 
> > Yes, doesn't work for private ints. However, it works for stuff like that,
> > though it's not exactly the same thing as a 'private int':
> > 
> > # type t = private A | B;;
> > type t = private A | B
> > # let x : t = Obj.magic 0;;
> > val x : t = A
> > # match x with A -> true | _ -> false;;
> > - : bool = true
> > # A;;
> > Error: Cannot create values of the private type t
> > 
> > I thought it also worked on for ints, and in a sense, I'm surprised that
> > you cannot pattern match private ints as ints without a coercion.
> 
> I asked a similar question when private ints were introduced in OCaml 3.11 - full explanation from Jacques as to why in: https://sympa-roc.inria.fr/wws/arc/caml-list/2008-10/msg00375.html

Yes an no. From a type inference perspective, that's right. However, you
can already do such pattern matching on private row types for variant
types.

module X : sig
	type t = private [< `A ]
	val x : t
end = struct
	type t = [ `A ]
	let x = `A
end

match X.x with `A -> ()

and the X.x is correctly unified with `A. So the type inference issue is
solved in this case.

What I'm wondering is why, when there is a known way to pattern match on
a given base type (like ints or strings), could this behaviour not be
extended. The work seems to have already been done for variant types.

While making type inference implicitly cross the border of type
coercion (as in your post) seems excessive, pattern-matching private
ints as you would for private row types seems OK to me.

Moreover, I somehow disagree with Jacques when he says:

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

There is a point:

The first 'private int' would simply be a way to forbid construction,
while allowing type-inference to go beyond the :> barrier.

The second 'very_private int' would be a way to block type inference.

Both would have their use cases.

-- 
     Guillaume Yziquel