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

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

Le Monday 28 Mar 2011 à 12:11:47 (+0000), David Allsopp a écrit :
> Guillaume Yziquel wrote:
> > Le Monday 28 Mar 2011 à 11:29:51 (+0000), David Allsopp a écrit :
> > > Guillaume Yziquel wrote:
> > > > 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.
> 
> There's nothing special needed to do this - the type of `A is [> `A ] so that unifies with type X.t without any special handling at all.

OK, there's no special handling.

Type of `A is [> `A] and type of X.x is t = private [< `A ].

But that's hardly different from:

Type of 1 is int and type of X.x is t = private int.

What I meant is that the fact that 'function `A -> ()' gets properly
unified with X.x which is of type 't = private [< `A]' is a solved type
inference issue. Because of what private row types mean: you can feed a
private row type to a function accepting the correct polymorphic variant
types.

It isn't the case for private ints. It's not a private row type, but
while I understand why type inference is screened by the private
keyword, I do not really understand why we couldn't pattern-match it as
an int. Except for the fact that you cannot feed a private int to a
function accepting an int for type inference reasons (opposite behaviour
than for private row types).

> > 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.
> 
> There's no extra work been done here - it's just normal type inference (i.e. there are no special cases that have been added for this to work). I'm not completely convinced by the argument against inferring coercions in the type checker, but arguing with Jacques is usually a route to being proven comprehensively wrong :o)

I wouldn't complain about that. I like the type hackery flexibility this
distinction brings.

> > 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.
> 
> There's nothing special going on for private row types - it's simply that the constants (variant or polymorphic variants) can only have only one type where integer constants can have more than one type (sort of - it's the wrong terminology really but from the type inference perspective, it's what's happening).

I do not understand the 'integer constants can have more than one type'
part of your sentence.

> David

-- 
     Guillaume Yziquel