TOLK lang: “The Hindley-Milner type system, and Why Tolk decided to avoid it You k…”

The Hindley-Milner type system, and Why Tolk decided to avoid it

You know, that FunC is "functional C". But do you know, what makes it "functional"? Not its low-level nature. Not its peculiar syntax. And even not the ~ tilda. "Functional" is mostly about the Hindley-Milner type system.

The Hindley-Milner type system is a common approach for functional languages, where types are inferred from usage through unification. As a result, type declarations are not necessary:


() f(a, b) {
    return a + b;   // a and b now int, since `+` (int, int)
}

For example,


() f(slice s) {} 

var s = null;
f(s);  // infer s as slice, since f accepts slice

For example,


int f(x) {
    (a, b) = (0, x);
    return a + b;   // x becomes int, since x and b edge
}

This "unification", looking pretty at first glance, arises problems, if we actually do not want types to unify. Imagine, we want to have nullable types: int (not nullable) and int? (nullable), so that we can assign null only to int?. What would Hindley-Milner think about this?


var x = 0;   // unify(Hole, Int) = Int
...
x = null;    // unify(Int, Nullable<Hole>) = Nullable<Int>

Instead of an error, Hindley-Milner would perform unification and result in x: int?. Not as we wanted to, right? (while it can be "fixed", it would step away from HM's nature)

A fun fact: you don't notice these problems in FunC. Because FunC's type system is very limited. But Tolk will have bool, fixed-width integers, nullability, smart casts, structures, and generics — these problems will become significant. Hindley-Milner will clash with structure methods, struggle with proper generics, and become entirely impractical for union types (despite theoretical claims that it was "designed for union types").

The goal is to have predictable, explicit, and positionally-checked static typing. While Hindley-Milner is powerful, it's actually "type inference for the poor" — simple to implement when there's no time to fundamentally design the language.

By the way, unreadable type errors also stem from Hindley-Milner:


error: function return type (int, int) cannot be unified with implicit end-of-block return type (int, ()): cannot unify type () with int

What the programmer actually wants to see is:


1) can not assign `(int, slice)` to variable of type `(int, int)`
2) can not call method for `builder` with object of type `int`
3) missing `return`

That's why Tolk v0.7 contains a fully rewritten type system, encoupled with clear error messages and an IDE plugin with type inference included. It's the groundwork for future enhancements.