Re: [Caml-list] bizarre type

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

From: Julien Verlaguet <Julien.Verlaguet@pps.jussieu.fr>
> 
> > Well, since '_a t = int t the compiler can freely choose either for
> > printing. Or bool t, for that matter.
> 
> agreed.

Nice to see that everybody agrees that the current behaviour is
reasonable :-)
And thanks to Andreas for explaining things so well.

Yet, these useless parameters are a rather weak part of the compiler,
so there may be some bugs left there. I.e. it is hard to guarantee
that "a t" will alway be equivalent to "b t" for any use, while they
should be so in the intended semantics. Bugs report are welcome.

In general, I would suggest avoiding non-abstract phantom types, as
they are useless... except when you're going to abstract them at the
next module boundary.

> In fact it prevents me from writting this :
> 
> type 'a marshalled=string
> 
> let make (x : 'a)=(Marshal.to_string x [] : 'a marshalled);;
> 
> And then do all type of operations in a type safe way on strings.

What you want seems to be the Graal: a type that is more than a
string, but can be implicitly coerced to one. Of course the opposite
direction would not be allowed.
A standard way to do that is to make [marshalled] abstract, and provide
a function [to_string] when you need to recover the string.
In ocaml 3.09, you will have another possibility: using a private type
for that, with the extra advantage of having pattern-matching (this
doesn't work with private types in 3.08, as they are not handled as
abstract.)
But not yet the Graal, which requires to combine implicit subtyping
with type inference in a non-trivial way...

> The only tiny thing that disturbs me is that in my previous example :
> 
> let g (x : 'a t) (y : 'a)
> 
> the type of y depends on the 'a present in 'a t.
> It is odd. But I have to admit it's correct.

The point here is that ['a t] is not the type of [x] itself, but a
type that can be unified with it. And useless parameters are discarded
during unification. At a more theoretical level, ['a t] is only
required to be equivalent to the type of [x], not identical.

Jacques Garrigue