Re: [Caml-list] Equality between abstract type definitions

[Didier Remy <Didier.Remy@inria.fr>]

>> When you annotate a program with types, you are just adding more
>> type equations to the unification problem, and you may of
>> course get at the end a type that is less generic than the one
>> you gave in the annotation (that's the key rule of the game
>> in unification).

> Aren't you conflating two different universes here? Namely, the
> declarative type system and the type inference algorithm? The ML type
> system semantics as such, at least in most formalisations I can remember,
> knows nothing about unification variables -- that's an implementation
> detail of algorithm W. And the user interface of a language is the
> declarative system, not the underlying implementation. Making unification
> variables user-visible is an extension to the basic ML type system that I
> have rarely seen made precise

Andreas, I am not sure what point you are trying to make.

Sure, the name "unification variable" is misleading and should not be used
here, as it refers to the algorithm. Instead, one should call them flexible
type variable or whatever that refers to the specification.

Still, flexible variables make a lot of sense in the specification (even
if not often done in formal presentations).

A language that does type inference should allow the user to say that two
arguments have the same type without telling what these types are, using a
flexible type variable.  (It should also allow the user to tell the type
checker that some expression whould have exactly this type scheme, using a
rigid type variable.

For this reason, the language should expose to the user the both notions of
rigid and flexible bindings.

One can easily specify the introduction of a flexible variable 'a in some
program M as the following typing rule and without reference to the
implementation:

                           G |- M ['a <- t] : s
                           -----------------------
                           G |- for some 'a. M : s

François and I discuss this and formalize it in our chapter "The Essence of
ML Type Inference" in "Advanced Topics in Types and Programming".

----------------

> (I seem to remember that the Didiers did that in the context of MLF).

Yes, since we needed more annotations in MLF because all function paramters
that are used polymorphically must be annotated, we wanted to be able to
only annoatte specify parts of the parameter that had to be used
polymorphically.  We could give type annotations of the form:

         for some 'u, for all 'a, 'b, ('a -> 'b) -> 'a * 'u -> 'b * 'v

When used as the annotation of a function parameter, 'u could be freely
instantiated, even to a polymorphic type, as long as this part of the
argument was not used polymorphically.

We found this necessary in MLF, but it would also be quite useful in OCaml.

         Didier