Strong Implicit Type Checking

First off, a big shout out to Rob Smallshire who wrote an implementation of The Hindley-Milner Type System in Python which I've wired in to this little language.

Programs are checked automatically in almost all cases, using a slightly extended version of Algorithm W. That means that

fn add(x, y) {
   x + y
}
add(10, true)

will fail with a type error bool != int. Note especially that this error is detected and reported by a static analysis phase before the code is executed.

Also lists are constrained to be of a specific type, and

[10, true]

will fail with the same error.

As mentioned, the type checking is done in a separate phase after parsing but before execution, so there can be no run-time type errors. There is no need for or even ability to type-hint the code, except in the case of environments. In this case the environment must be declared by name, and the name of the environment must be used to type-hint any function that takes an environment as argument. For example

env env_a {
    define x = 2;
    define y = 5;
}
env env_b {
    define x = 11;
    define y = 12
}
fn (e:env_a) {
   e.x + e.y
}(env_b);

produces 23. Note that the variable e was hinted as an env_a, but the function was passed env_b. It still works because env_a declares the same values, with the same types, as env_b So env_a is acting as a "template".

Implementation Note The existence of first class environments in F♮ is why the type checker was described as a "slightly extended" implementation of the standard algorithm: the "type" of an environment is precisely the type environment constructed while type checking it, so it's not possible to correctly type check a function applied to an environment without declaring which environment.

Explicitly Prototyping an Environment

Rather than using one environment as a template for another, it's possible to explicitly declare a prototype for a set of environments. As an example:

prototype foo {
    map: (#a -> #b) -> list(#a) -> list(#b);
}

env bar {
    fn map {
        (f, []) { [] }
        (f, h @ t) { f(h) @ map(f, t) }
    }
    
    fn other(x) { x }
}

fn x (mapper: foo) {
    mapper.map(1+, [1, 2, 3])
}

x(bar);

The prototype foo declares a prototype environment foo containing a map entry. Rather than writing the body of the function map we supply its type in the standard Type Notation as (#a -> #b) -> list(#a) -> list(#b). Note the hash sigils which identify type variables.

Another important advantage of prototypes over templates is that only the declared types are checked. The extra function other in env bar does not cause a type error when bar is type checked.

Up: Home

Next: Odd Corners