Generalize/Instantiate/Fixpoint/Traits for MLsub

In my last study of subtyped ML there was some details that I didn't understand well.

Generalize & Instantiate

Generalize and instantiate originates from the algorithm W. The type environment is polymorphic in ML-style languages. Generalize occurs when something gets bound into the type environment. Instantiate occurs when something gets retrieved from a type environment.

The purpose of generalize and instantiate is to provide parametric polymorphism. It allows the user of the language to call a function with different but incompatible arguments.

MLsub does the type inference in a state machine. Therefore the type environment consists of a graph.

Every layer of scope has a subgraph that contains free nodes. Every node reachable from free node is free.

Generalize does a subset construction from every node that is not free in the type environment. Instantiate copies every node that is not free in the type environment.

What's the effect of these routines? To show that lets take a small example program with select:

select(a,b,c) = if a(b) then b else c
select :: (a -> bool, a, b) -> a|b

test1(p) = select(p, X, Y)
test2(g) = select(g, Z, W)

Without polymorphism, the type annotations of test1/test2 would end up as:

test1 :: (X|Z -> bool) -> X|Y|Z|W
test2 :: (X|Z -> bool) -> X|Y|Z|W

With polymorphism, we get these annotations:

test1 :: (X -> bool) -> X|Y
test2 :: (Z -> bool) -> Z|W

Subtyping variants of ML have more tolerance for lack of polymorphism. For example, print(test1(), test2()) would succeed in any case, as long as all X,Y,Z,W can be printed.

Fixed point

The understanding of fixed-point is required to correctly handle mutually recursive declarations, repetition or phi-nodes in SSA form.

The fixed-point can be constructed through the usual means of deriving it from the following clause:

fix(f) = letrec x = f x in x

We extract the following subtyping relations:

f <: a -> b
b <: x
x <: a

They form the following bisubstitutions:

f- = f- & (a+ -> b-)
b- = b- & x-
a+ = a+ | x+

After simplifying, we get the type:

fix :: (x -> x) -> x

Now lets get the following recursive sum -clause:

type list(a) = cons(a, list(a)) | nil

sum(sum)(l) = case l of
    cons(a,w) -> sum(w) + a
    nil       -> 0
sum :: (a -> add_l(c, _)) -> a&list(add_r(c, _)) -> int | c

I already supplied the type annotation, because I thought it doesn't add anything here.

Next we can feed sum to itself with the expression fix(sum). This results in three relations, one of them trivial:

x <: j
(a&list(add_r(c, _)) -> int | c) <: x
x <: (a -> add_l(c, _))

The trivial relation x <: j tells only that the result is flowing from x variable. The two other relations propose that:

(a&list(add_r(c, _)) -> int | c) <: (a -> add_l(c, _))

This results in:

a <: a&list(add_r(c, _))
int <: add_l(c, _)
c <: add_l(c, _)

The int <: add_l(c, _) ends up being satisfied, it substitutes to add_l(int, int_add) <: add_l(c, _). Now I can already roughly see the full type signature.

fix(sum) :: list(rec k.add_r(c&add_r(k, int_add), int_add)) -> int | c

This treatment proposes that the fixed-point can be solved with the following routine on strongly connected components:

  1. Create free variables for each recursive declaration and bind them into a new scope.
  2. Feed each definition of a declaration into its variable.
  3. Generalize each variable, yielding the type signature of each declaration as a result.

It looks a lot like that these requirements arise from the need to limit polymorphism under recursion.

Traits

MLsub appears to have natural representation for traits or typeclasses, but the rules are difficult to derive due to how differently subtyping inference works in comparison to traditional ML.

The simplest trait to derive is likely for the getattr and after that, setattr.

getattr x :: get:x(a) -> a
setattr x :: (set:x(a), a) -> unit

The operations like getattr and setattr describe things that can be done to specific objects. They can be trivially implemented by sourcing the appropriate methods from the object that is passed into them.

Some traits associate with binary operations. Binary operations are harder because the objects used have to agree on the operation. This effect can be achieved through bivariance.

(+) :: (plus:l(a, fn), plus:r(a, fn)) -> a

The fn parameter gets the implementing function as a bivariant reference. Therefore the operation may only be satisfied if the both sides in the expression agree on the function.

The side on operation is reported because when the type is finally resolved, we may provide additional details on how the operation is implemented.

Type-indeterminate based approach I am planning to try on operations will be slightly different and require additional machinery to work, but it is still nice to know how the inference algorithm would be working as-it.

Similar posts