Representing a structure/tuple type with Hindley Milner Type Inference

Question

I'm writing a really simple interpreted object oriented programming language with a C-like syntax. I've been looking into type inference and I've found a few implementations of the 'Hindley-Milner Type Inference' system.

Most are in functional languages, which I can't read, but I found this one written in Python that I can make sense of.

One question though is I'm not sure how to represent more complicated types like a Structure or a Tuple.

This implementation represents primitive types like booleans with the TypeOperator (psuedo-y code):

bool = new TypeOperator("bool", [])
int = new TypeOperator("int", [])

type_environment.add TypeOperator("true", [bool])
type_environment.add TypeOperator("false", [bool])

So could I use this type operator to represent a structure?

struct Person {
    int age;
    bool is_dead;
}

Like so:

type_environment.add TypeOperator("Person", [int, bool]);

Answer 1

Hindley-Milner doesn’t much care if your type is a tuple or a struct. Types are types, and the algorithm focuses on the transformations that occur during operations. foo.toString() converts a foo to a string for example. Foo or string could be a tuple or a structure and the algorithm will work fine.

For your library, you’ll need some way to differentiate ordered sequences (tuples) and records/structs (where the order doesn’t matter, but the field labels do... usually). That might be as simple as constructing the typename from its contents - like TypeOperator(“int|bool”,[]) for your tuples.

Answer 2

You have a problem that you haven't recognised yet. Your problem isn't how to declare the types of structures (which is simple: you just add them statically to your environment when you encounter a definition), but how to infer them. Which comes down to: how do you work out the types of arguments in operators that work on structures, which is to say field selection and mutation.

Hindley-Milner (or rather Damas-Hindley-Milner type inference, which is the more correct name for it) works in its context (functional languages that operate primarily on the types of tuples and discriminated unions) because those languages only have types and operations on those types that are well defined under the unification operation used in the inference algorithm. Such languages may have structures, but they are usually opaque ... i.e. there is no defined way within an expression of extracting a value from them (typically the process of defining such a structure will also create a set of functions that extract individual values from the structure, but this is an implementation detail that doesn't need to be known by the type inference engine; a DHM type-inferred language may also use pattern matching, but again this doesn't get seen directly by the inference engine: it's desugared into a series of lambda abstractions that have predeclared types for the variables corresponding to the types of the components of the structure that are matched against).

Unfortunately, typical object-oriented languages usually include operations that don't produce such well defined results for unification.

Here are the operations that are supported in a typical functional language:

• lambda abstraction: \ v -> expr. To unify the types here we find the usages of the variable v inside expr, determine the required type of v given those usages (which we'll call A), determine the type of expr (which we'll call B) and produce the result A -> B.
• binding: let v = e1 in e2 - we determine the required type of v given any occurences of it in e2 and unify that with the type of e1, and yield the result as the type of e2
• application: e1(e2) - we determine the type of e2 as A, create a new type variable B, unify e1 with A -> B, and give the result type B.
• variable dereference: v - type of v is unified with new type variable A and the result is A.

Because we know the types of predefined functions and of literals, we should now be able to determine the type of any expression using these operations, and of any variables that are bound within that expression.

It's useful to look at an example of how this works in practice in order to see what goes wrong when you attempt to apply it to an OO language, so lets do that. For example, given these type definitions:

add : Int -> Int -> Int
succ : Int -> Int
pred : Int -> Int
decimal : Int -> String

we can determine the types of everything in any arbitrary correctly-typed expressions:

let f1 = \ x -> add (x) (3) in
 let f2 = \ x -> succ (f1 (x)) in
  decimal (f2 (4))

To do this, we first build a parse tree, giving each node's type a new type variable (which we'll use "T" to represent). I'll use the following conventions:

let (tv, v, e1, e2)    -- define v with type tv to equal e1 in expression e2
lambda (tv, v, e)      -- produce function with variable v having type tv
                       -- yielding expression e having type te
var (v)                -- dereference variable v having type tv
apply (tf, f, ta, a)   -- apply function returned by expression f having 
                       -- tf to argument a having type ta; tf is required
                       -- to have the form "A -> B".
num (v)                -- literal number (always has type Int)

I haven't used the feature in the example above, but I'll allow "let" to be recursive: the expression "e1" is allowed to refer to variable "v", which will have type "tv" (typically a variable) during evaluation of the expression. The python code you linked to calls this letrec rather than let, and has an alternative simpler let that doesn't allow recursive use, but for demonstration purposes you don't really need both.

Our parse tree therefore looks like:

let (
  "T1", "f1", lambda (
     "T2", "x", apply (
         "T3 -> T4", apply (
             "T5 -> T6", var("add"), 
             "T7", var("x")),
         "T8", literal (3))),
  let (
     "T9", "f2", lambda (
         "T10", "x",
         "T11", apply (
             "T12 -> T13", var ("succ"),
             "T14", apply (
                 "T15 -> T16", var ("f1"), 
                 "T17", var ("x")))),
     apply (
         "T18 -> T19", var("decimal"),
         "T20", apply (
             "T21 -> T22", var ("f2"), 
             "T23", literal (4)))))

Then we intialize a type environment with our default known types and start processing the tree. I'll introduce a series of variables e<number> to describe expressions we're not going to examine until later steps:

• The root node is let ("T1","f1",e1, e2). Add f1 : T1 into the environment, unify "T1" with the type of "e1", then and return the type of "e2".
  • e1 is lambda ("T2", "x", e3), so add x : T2 to the environment, evaluate the type of e3 in this environment, and yield the type T2 -> (typeof e3).
  • e3 is apply ("T3 -> T4", e4, "T8", e5). Evaluate type of e4 and unify with T3 -> T4; then evaluate type of e5 and unify with T8. Then unify T8 and T3. The type of e3 will be T4. [note: this process can be simplified and T8 eliminated, but I think it's clearer this way]
    • e4 is apply ("T5 -> T6", var("add"), "T7", var("x")). "add" has a defined type in the environment, which is Int -> Int -> Int (-> is a right associative operator so this is equivalent to Int -> (Int -> Int)). So unifying T5 -> T6 with this type results in elimination of these variables: T5 is now known to refer to Int and T6 to Int -> Int. "x" also has a type known, but it's another variable rather than a fixed type: T7 is replaced with T2 in future occurences. T2 is now unified with Int, eliminating T2. The environment now contains x : Int and we know that e1's type will be Int -> (something). e4's type was T6, which we now know to be Int->Int. Returning briefly to e3, we know that this needs to be unified with T3 -> T4, so both T3 and T4 become Int.
    • e5 is literal(3). This is defined to have type Int by our language definition, so T8 is unified with Int.
  • we drop back to processing e3: We still needed to unify T8 with T3, but both of these already have firm bindings to Int (if they had been different we would have signalled a type error at this point). The type of e3 was originally defined as T4 but we've already unified that with Int, so we yield Int
  • We can now determine that e1's type is Int -> Int. We return that back up to the top level. At this point, the variable x goes out of scope so is removed from the environment.
• We can now unify T1 with Int -> Int, meaning the environment now contains f1 : Int -> Int instead of f1 : T1 as it did previously, and proceed with evaluating the type of e2.
  • e2 is let("T9", "f2", e6, e7). As before we add f2 : T9 to the environment, and evaluate the type of e6.
  • e6 is lambda("T10", "x", "T11", e8). We already know the type of e6 will beT10 -> T11(if we were implementing a parallel type checker we could return this immediately and spawn a new process to determine what these types will actually be). We addx : T10` to the environment and evaluate the type of e8.
    • e8 is apply("T12 -> T13", var("succ"), "T14", e9) which yields a result of type T13. succ's type is already known: Int -> Int, so we can instantly unify that with T12 -> T13. T14 also gets unified with T12, so all 3 variables are now Ints. We also unify the type of e9 with T14 (which will fail if it isn't Int).
    • e9 is apply ("T15 -> T16", var("f1"), "T17", var("x")). We know both f1 : Int -> Int and x : T10 from the environment, so these get unified (T15 and T16 become Int; T17 becomes T10). T17 (now T10) is unified with T15 (now Int), eliminating another variable. x : Int is now in the environment. Result of e9 would have been T16, but that has already been unified with Int, so return Int.
    • Unifying Int with Int doens't fail. return e8's type of Int.
  • Returning to e6, T11 is unifies with Int, and the expression type Int -> Int is returned. x goes out of scope.
  • T9 is now unified with Int -> Int. Other than the standard functions, our environment now consists of f1 : Int -> Int; f2 : Int -> Int. We're on the home straight now: we only have e7's type left to evaluate.
  • e7 is apply ("T18 -> T19", var("decimal"), "T20", e10). decimal's type is known to be Int -> String, so T18 is unified with Int and T19 with String. T20 gets unified with T18 and the type of e10. The type of e7 is T19 (now String). We now know that the type of the whole expression is String, we just need to finish type checking it to make sure there are no errors.
    • e10 is apply("T21 -> T22", var("f2"), "T23", literal(4)). We're finally at the last expression! f2 has known type Int -> Int so T21 and T22 are eliminated. literal(4) is an Int by definition, so T23 is eliminated. We have no more type variables left. T21 (now Int) is unified with T23 (now Int) so the final expression type-checks. Type of e10 is Int.
  • Int unifies with T18 (now Int). That's the last type check: the whole expression is good. Result of e7 is String.
  • Result of e2 is therefore also String
• And finally, the result of the top level expression is String.

With all variables substituted, the typechecked parse tree is now:

let (
  "Int -> Int", "f1", lambda (
     "Int", "x", apply (
         "Int -> Int", apply (
             "Int -> Int -> Int", var("add"), 
             "Int", var("x")),
         "Int", literal (3))),
  let (
     "Int -> Int", "f2", lambda (
         "Int", "x",
         "Int", apply (
             "Int -> Int", var ("succ"),
             "Int", apply (
                 "Int -> Int", var ("f1"), 
                 "Int", var ("x")))),
     apply (
         "Int -> String", var("decimal"),
         "Int", apply (
             "Int -> Int", var ("f2"), 
             "Int", literal (4)))))

Right: so now we see how it works, how do we handle these expressions that add more typical OO features to the language?:

• let f = \ x -> x.field? Note that (at least using normal OO conventions) there may be many unrelated types that have fields called field, so we can't use that to infer a type for f.
• Given a type C and a subtype of it S, how about var x; x := new S;? Is x's type S, or is it the more general type C?

The only thing we can do in situations like these is build up a list of constraints, and attempt to identify possible types that can satisfy the constraints at the end of checking the module -- or maybe even just declare the constraints as part of the type, so perhaps the type of f is forall T1, T2 where has-property (T1, 'field', T2) . T1 -> T2 and the type of x is forall T where T <- S . T [using the common '<-' symbol to indicate a subtype relationship]. But such type descriptions can end up being very long and complicated, and therefore extremely confusing in error messages. Typescript is an example of a language that does this; I was working in it earlier today, and here's an example of an error that I received:

src/newuserreport.ts(61,21): error TS2345: Argument of type '{ type: string; data: { labels: any[]; datasets: ({ labal: string; backgroundColor: string; data:...' is not assignable to parameter of type 'ChartConfiguration'.
  Types of property 'data' are incompatible.
    Type '{ labels: any[]; datasets: ({ labal: string; backgroundColor: string; data: number[]; xAxisID: st...' is not assignable to type 'ChartData'.
      Types of property 'datasets' are incompatible.
        Type '({ labal: string; backgroundColor: string; data: number[]; xAxisID: string; } | { label: string; ...' is not assignable to type 'ChartDataSets[]'.
          Type '{ labal: string; backgroundColor: string; data: number[]; xAxisID: string; } | { label: string; b...' is not assignable to type 'ChartDataSets'.
            Type '{ labal: string; backgroundColor: string; data: number[]; xAxisID: string; }' is not assignable to type 'ChartDataSets'.
              Object literal may only specify known properties, but 'labal' does not exist in type 'ChartDataSets'. Did you mean to write 'label'?

.... which is the error produced for a single character typo. The fact that DHM inference can produce exact named types for most valid expressions in languages that use it is, in fact, its most important defining characteristic.

Another issue is that recursive type checking can become undecidable. For example, in our functional language (suitably extended), a recursive function can always be type-checked: if an argument to a recursive function is never used or returned, it is irrelevant, and can be left with a polymorphic type variable. If it is returned, that variable can be unified with the return type. If it is used to call another function, it can be unified with that function's type. If it is used in a recursive call, then either (1) there is another control flow path in which it isn't used recursively, and the types for that path can be used, or (2) the function never returns, and non-returning functions all have the same type: * -> bottom (bottom being a predefined type of which no values exist). They can all have the same type because they all have no effect on calculation at all, other than preventing it ever finishing.

In the present of mutation, however, this analysis no longer holds: a non-returning function can have definite side-effects that should be observable, so they do not all have the same type. What type does let f = \ x, y -> { x.a := y; f (y,x.b) } have? It never returns, but it does do something, and yields non-trivial (perhaps even infinite) constraints on its arguments.