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

[Andreas Rossberg <rossberg@mpi-sws.org>]

On Oct 26, 2013, at 19:32 , Didier Remy <Didier.Remy@inria.fr> wrote:
>>> 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).

Oh, I agree. I was merely questioning that all explicit type variables in ML would naturally be flexible variables, which was what I was reading into Roberto's reply (if you take the preceding paragraph from his post as context). Sure, flexible variables are easy (and useful) to add, but technically speaking they are an extension, i.e., require extra rules. Or would you not say so?

And yes, I want to have both forms of variables/bindings, as I suggested in my original post. My main concern with the current state of affairs in OCaml is that implicitly interpreting 'a as the flexible kind obviously is surprising to many people, arguably because it is somewhat inconsistent. Especially when rigid probably is the more common use case.


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

Ah, yes, thanks for the reminder.


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


Yes, makes sense. I suppose the main obstacle is retrofitting a nice syntax into OCaml.

/Andreas