Re: [Caml-list] -principal

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

On 2013/05/03, at 6:16, Yaron Minsky <yminsky@gmail.com> wrote:

> Can anyone describe the pluses and minuses of turning on -principal?
> Is it considered to be good practice for codebases that are compatible
> with it?  Can it change behavior of currently working code?

Turning on -principal allows detecting "risky" uses of type information to
help type inference.
By risky I mean that success or failure of type inference may depend
on the order in which subexpressions are typed.
This kind of type information is only used by a limited number of features:
* polymorphic methods
* using different order of labeled arguments in a function
* some discarding of optional arguments
* choice of the source type in a coercion (i.e. automatic upgrading of
   (expr :> t2) into (expr : t1 :> t2) when the type of expr is closed).
  This is particularly useful for private type abbreviations.
* GADTs
* disambiguation of record field and constructor names (new in trunk)

The technical definition is based on polymorphism, but the intuition
is that type information follows the (functional) flow of data, even going
through polymorphic functions (being conservative when merging flows).
So a simple way to understand is: supposing that type annotation physically
adds type information to the expression they decorate, will all values
reaching the use point be decorated?
It also flows backward (the expected type is propagated), but does not
go through functions in that case.

# type t = < id: 'a. 'a -> 'a >;;
type t = < id : 'a. 'a -> 'a >
# let f (x : t) = x, x#id;;     (* safe code: the type of x is known at all its use points *)
val f : t -> t * ('a -> 'a) = <fun>
# let f x = (x : t), x#id;;     (* unsafe code: the type is only known because typing goes from left to right *)
Warning 18: this use of a polymorphic method is not principal.
val f : t -> t * ('a -> 'a) = <fun>
# let f x = x#id, (x : t);;    (* just exchanging the members of the pair causes a failure *)
Error: This expression has type < id : 'a; .. >
       but an expression was expected of type t
       The universal variable 'a0 would escape its scope

In an ideal world, I would suggest systematically using -principal, as it makes
the notion of "known type" well-defined.
However, there are drawbacks to -principal
* type inference is slower (more copying occurs)
* cmi's become bigger
The first point is mainly a problem if you use objects.
The second one if you have already problems with cmi size (again, mostly objects)

As a result the suggested approach is to only compile with -principal once in a while.
This is reasonable because if compiling with -principal works, in theory it is guaranteed
that the program will be accepted without -principal too. Of course the semantics do
not change.

However there is a difficulty: since the generated cmi's may differ, in general one
has to maintain completely separate builds.
If you have a complete set of mli's, then a solution is to always compile mli's with
(or without) -principal. (Compiling the mli without principal may in theory cause
propagation to fail in some cases, but you are on the safe side, and I have
never observed it)

So yes, it is good practice. But I'm afraid few invested the effort in doing it.
Looking at the features you use in Core, this may be a good idea to try.
(My understanding is that Lexifi tried, but they had problems because they
use big object types).
By the way, the ocaml compiler itself doesn't use any of the above features,
so it is not directly concerned.

Jacques Garrigue