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

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

On 10/25/2013 10:29 AM, Roberto Di Cosmo wrote:
>       let me offer a comment on terminology here: 'a, 'b and the
> like have always been used to denote polymorphism in a type, and
> hence used as unification variables since the beginning of the ML
> language history, to infer the type of a program.

I believe you are mistaken. At least in Standard ML, explicit type 
variables have always been interpreted as quantified variables, not 
unification variables. If you try to write

   fun f(x : 'a) = x + 1

or

   fun g(x : 'a) = x : 'b

that's an error.


> 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 (I seem to remember 
that the Didiers did that in the context of MLF).

/Andreas