The alias problem : Lightweight HK polymorphism

Learning
, ,
1

Hi, i’m currently trying to read the paper “Lightweight higher-kinded polymorphism” by Jeremy Yallop and Leo White, and i don’t really understand the “alias problem” part, for instance :

Since OCaml cannot distinguish between data types and aliases, it must support instantiating type variables with either. This works well for type variables of base kind, but breaks down with the addition of higher-kinded type vari- ables. To see the difficulty, consider the unification of the following pair of type expressions

’a ’f ∼ (int * int) list

where ’f is a higher-kinded type variable. If there are no other definitions in scope then there is an obvious solution, unifying ’a with (int * int) and ’f with list. Now suppose that we also have the following type aliases in scope:

type ’a plist = (’a * ’a) list 
type ’a iplist = (int * int) list

With the addition of plist and iplist there is no longer a most general unifier. Unifying ’f with either plist or iplist gives two new valid solutions, and none of the available solutions is more general than the others.

i don’t really understand why there is no longer a most general unifier in the second example or how this unification is supposed to works anyway, whats the goal we are trying to achieve ?

1 Like
3

In the second example, there are three possible unifications:

  • 'f = list and 'a = 'int * int
  • 'f = plist and 'a = 'int
  • 'f = iplist and 'a = 'b

and none of those choices are compatible with any other choice. So there is no general unifier. In other words, with the type scheme

'a: *,  'f: * -> *: 'a 'f -> 'a option

one cannot infer a concrete type at instantiation time without knowing the concrete 'f type constructor to use during the instantiation.

2 Likes
4

So does “general unifier” mean something like “unique normal form”? I ask because I come across variants of “general” fairly often (e.g. in explanations of -principal) and I can rarely figure out what it means.

5

to be honest, i still don’t understand. I think thats because i know barely nothing about type unification, but i really don’t get whats the problem with type aliases when it comes to unification.

do you have an example where there is several definitions in scope and we can find a general unifier please ?

6

Yes, this the example above. Trying to rephrase it, consider a situation where you have two type definitions in scope

type 'a t
type 'a t2 = ('a * 'a) int

then the minimal complete set of solutions to the equation

'a 'f = (int * int) t

is

{ 
  ['a = int; 'f = t2 ];
  [ 'a = int * int; 'f = t ] 
}

and contrarily to what happens to in the first-order case, the two solutions are independent: one cannot derive the other by introducing more substitutions.

This is distinct to what happens, without type constructor variables, if I have the equation
'a * 'a list = ('b option * 'c) list
the set of minimal complete solution is

{ ['a = 'b option; 'c = 'a] }

where the important part is that all other solutions of the equation can be derived from this most general solution (aka the general unifier) by adding more equations/substitutions.