Tag Archives: environments

Languages, Technology

The Hindley-Milner Algorithm

Leave a comment

The Hindley-Milner Algorithm is an algorithm for determining the types of expressions. Basically it’s a formalisation of this earlier post. There’s an article on Wikipedia which is frustratingly terse and mathematical. This is my attempt to explain some of that article to myself, and to anyone else who may be interested.

Background

The Hindley-Milner algorithm is concerned with type checking the lambda calculus, not any arbitrary programming language. However most (all?) programming language constructs can be transformed into lambda calculus. For example the lambda calculus only allows variables as formal arguments to functions, but the declaration of a temp variable:

can be replaced by an anonymous function call with argument:

Similarily the lambda calculus only treats on functions of one argument, but a function of more than one argument can be curried, etc.

Expressions

We start by defining the expressions (e) we will be type-checking:

[bnf lhs=”e”]
[rhs val=”E” desc=”A primitive expression, i.e. 3.”/]
[rhs val=”s” desc=”A symbol.”/]
[rhs val=”λs.e” desc=”A function definition. s is the formal argument symbol and e is the function body (expression).”/]
[rhs val=”(e e)” desc=”The application of an expression to an expression (a function call).”/]
[/bnf]

Types

Next we define our types (τ):

[bnf lhs=”τ”]
[rhs val=”T” desc=”A primitive type, i.e. int.”/]
[rhs val=”τ0 → τ1” desc=”A function of one argument taking type τ0 and returning type τ1“/]
[/bnf]

Requirement

We need a function:

[logic_equation num=1]
[statement lhs=”f(ε, e)” rhs=”τ”/]
[/logic_equation]

where:

[logic_table]
[logic_table_row lhs=”ε” desc=”A type environment.”/]
[logic_table_row lhs=”e” desc=”An expression.”/]
[logic_table_row lhs=”τ” desc=”A type”/]
[/logic_table]

Assumptions

We assume we already have:

[logic_equation num=2]
[statement lhs=”f(ε, E)” rhs=”T” desc=”A set of mappings from primitive expressions to their primitive types (from 3 to int, for example.)”/]
[/logic_equation]

The following equations are logic equations. They are easy enough to read, Everything above the line are assumptions. The statement below the line should follow if the assumptions are true.

Our second assumption is:

[logic_equation num=3]
[assumption lhs=”(s, τ)” op=”∈” rhs=”ε” desc=”If (s, τ) is in ε (i.e. if ε has a mapping from s to τ)”/]
[conclusion lhs=”f(ε, s)” rhs=”τ” desc=”Then in the context of ε, s is a τ”/]
[/logic_equation]

Informally symbols are looked up in the type environment.

Deductions

[logic_equation num=4]
[assumption lhs=”f(ε, g)” rhs=”τ1 → τ” desc=”If g is a function mapping a τ1 to a τ”/]
[assumption lhs=”f(ε, e)” rhs=”τ1” desc=”and e is a τ1“/]
[conclusion lhs=”f(ε, (g e))” rhs=”τ” desc=”Then the application of g to e is a τ”/]
[/logic_equation]

That is just common sense.

[logic_equation num=5]
[assumption lhs=”ε1” rhs=”ε ∪ (s, τ)” desc=”If ε1 is ε extended by (s, τ), e.g. if s is a τ”/]
[conclusion lhs=”f(ε, λs.e)” rhs=”τ → f(ε1, e)” desc=”Then the output type of a function with argument s of type τ, and body e, is the type of the body e in the context of ε1“/]
[/logic_equation]

This is just a bit tricky. We don’t necessarily know the value of τ when evaluating this expression, but that’s what logic variables are for.

Algorithm

  • We extend the set T of primitive types with an infinite set of type variables α1, α2 etc.
  • We have a function new which returns a fresh type variable each time it is called.
  • We have a function eq which unifies two equations.

We modify our function, part [4] (function application) as follows:

[logic_equation num=6]
[assumption lhs=”τ0” rhs=”f(ε, e0)” desc=”If τ0 is the type of e0“/]
[assumption lhs=”τ1” rhs=”f(ε, e1)” desc=”and τ1 is the type of e1“/]
[assumption lhs=”τ” rhs=”new” desc=”and τ is a fresh type variable”/]
[conclusion lhs=”f(ε, (e0 e1))” rhs=”eq(τ0, τ1 → τ); τ” desc=”Then after unifying τ0 with τ1 → τ, the type of (e0 e1) is τ.”/]
[/logic_equation]

That deserves a bit of discussion. We know e0 is a function, so it must have a type τa → τb for some types τa and τb. We calculate τ0 as the provisional type of e0 and τ1 as the type of e1, then create a new type variable τ to hold the type of (e0 e1).

Problem

Suppose e0 is the function length (the length of a list of some unspecified type τ2), then τ0 should come out as [τ2] → int (using [x] to mean list of x.)

Suppose further that τ1 is char.

We therefore unify:

[logic_equation]
[statement lhs=”{{{τ2}}}” op=”→” rhs=”int“/]
[statement lhs=”{{{char}}}” op=”→” rhs=”τ”/]
[/logic_equation]

Which correctly infers that the type of (length [‘c’]) is int. Unfortunately, in doing so, we permanently unify τ2 with char, forcing length to have permanent type [char] → int so this algorithm does not cope with polymorphic functions such as length.

Languages, Technology

Types, Type Checking, Type Variables and Type Environments

Leave a comment

This was the bit of Comp. Sci. I always thought looked uninteresting, but in fact when you delve in to it it’s really fascinating and dynamic. What we’re actually talking about here is implicit, strong type checking. Implicit means there is not (usually) any need to declare the type of a variable or function, and strong means that there is no possibility of a run-time type error (so there is no need for run-time type checking.)

Take a look at the following code snippet:

You and I can both infer a lot of information about double, x, y and z from that piece of code, if we just assume the normal meaning for +. If we assume that + is an operator on two integers, then we can infer that x is an integer, and therefore the argument to doublemust be an integer, and therefore y must be an integer. Likewise since + returns an integer, double must return an integer, and therefore z must be an integer (in most languages + etc. are overloaded to operate on either ints or floats, but we’ll ignore that for now.)

Before diving in to how we might implement our intuition, we need a formal way of describing types. For simple types like integers we can just say int, but functions and operators are just a bit more tricky. All we’re interested in are the argument types and the return type, so we can describe the type of + as:

I’m flying in the face of convention here, as most text books would write that as (int * int) → int. No, that * isn’t a typo, it is meant to be some cartesian operator for tuples of types, but I think it’s just confusing so I’ll stick with commas.

To pursue a more complex example, let’s take that adder function from a previous post:

So adder is a function that takes an integer x and returns another function that takes an integer y and adds x to it, returning the result. We can infer that x and y are integers because of + just like above. We’re only interested for the moment in the formal type ofadder, which we can write as:

We’ll adopt the convention that → is right associative, so we don’t need parentheses.

Now for something much more tricky, the famous map function. Here it is again in F♮:

map takes a function and a list, applies the function to each element of the list, and returns a list of the results. Let’s assume as an example, that the function being passed to map is some sort of strlen. strlen‘s type is obviously:

so we can infer that in this case the argument list given to map must be a list of string, and that map must return a list of int:

(using [x] as shorthand for list of x). But what about mapping square over a list of int? In that case map would seem to have a different type signature:

In fact, map doesn’t care that much about the types of its argument function and list, or the type of its return list, as long as the function and the lists themselves agree. map is said to be polymorphic. To properly describe the type of map we need to introducetype variables which can stand for some unspecified type. Then we can describe map verbally as taking as arguments a function that takes some type a and produces some type b, and a list of a, producing a list of b. Formally this can be written:

where <a> and <b> are type variables.

So, armed with our formalisms, how do we go about type checking the original example:

Part of the trick is to emulate evaluation of the code, but only a static evaluation (we don’t follow function calls). Assume that all we know initially is the type of +. We set up a global type environment, completely analogous to a normal interpreter environment, but mapping symbols to their types rather than to their values. So our type environment would look like:

On seeing the function declaration, before we even begin to inspect the function body, we can add another entry to our global environment, analogous to the def of double (we do this first in case the function is recursive):

Note that we are using type variables already, to stand for types we don’t know yet. Now the second part of the trick is that these type variables are actually logic variables that can unify with other data.

As we descend into the body of the function, we do something else analogous to evaluation: we extend the environment with a binding for x. But what do we bind x to? Well, we don’t know the value of x, but we do have a placeholder fot its type, namely the type variable <a>. We have a tiny choice to make here. Either we bind x to a new type variable and then unify that type variable with <a>, or we bind x directly to <a>. Since unifying two unassigned logic variables makes them the same logic variable, the outcome is the same:

With this extended type environment we descend into the body and come across the application of + to x and x.

Pursuing the analogy with evaluation further, we evaluate the symbol x to get <a>. We know also that all operations return a value, so we can create another type variable <c> and build the structure (<a>, <a>) → <c>. We can now look up the type of + andunify the two types:

In case you’re not familiar with unification, we’ll step through it. Firstly <a> gets the value int:

Next, because <a> is int, the second comparison succeeds:

Finally, <c> is also unified with int:

So <a> has taken on the value (and is now indistinguishable from) int. This means that our environment has changed:

Now we know <c> (now int) is the result type of double, so on leaving double we unify that with <b>, and discard the extended environment. Our global environment now contains:

We have inferred the type of double!

Proceeding, we next encounter def y = 10;. That rather uninterestingly extends our global environment to:

Lastly we see the line def z = double(y);. Because of the def we immediately extend our environment with a binding of z to a new placeholder <d>:

We see the form of a function application, so we look up the value of the arguments and result and create the structure:

Next we look up the value of double and unify the two:

<d> gets the value int and our job is done, the code type checks successfully.

What if the types were wrong? suppose the code had said def y = "hello"? That would have resulted in the attempted unification:

That unification would fail and we would report a type error, without having even run the program!

Languages, Technology

Purely Functional Environments

Leave a comment

Here’s a different take on environments. In a pure functional language all data is immutable, end of story, and that would apply to any environments implemented in such a paradigm too. Operators like define would not be allowed to modify an environment, instead such operators would have to return a copy of the environment with the modified value. This has some interesting implications for any language using such an environment. For example:

So each fn captures the current environment, and since nothing is allowed to change, the environment captured is precisely as it was when it was captured.

So how can we make a functional environment that is even remotely efficient? A standard technique is to implement it as a binary tree. Let’s assume symbols have unique numeric identifiers, so that symbol lookup can be reduced to numeric lookup. Then our environment can be a tree who’s left nodes all have indexes less than the current node, and who’s right nodes all have indexes greater than the current node. Here’s a pair of classes that implement such a tree:

So far so good, but what about extension?

extend() only makes a copy of the path through the tree that was traversed in order to find the node to add or replace. this means that for a balanced tree, extend() is O(log n) of the number of items in the environment, which is not too bad.

Note also how the EmptyNode behaves as a singleton without explicitly requiring a static instance variable. This makes the implementation quite space efficient too.

The implementation does not support deletion of values, but that is ok since only a non-functional language with backtracking would require it, in order to undo side-effects.

Lastly, note that because these environments are immutable, we do not need any notion of an environment frame to encapsulate local changes, the old environment is still present and will be reverted to outside of a closure just as if we were using environment frames.

Of course this completely ignores the issues of maintaining balanced binary trees, for the sake of simplicity.

Languages, Technology

A Bit More on Compiler Environments

Leave a comment

Rather than a single “Environment” type, a compiler distinguishes between compile-time and run-time environments.

In an interpreter, the value of a symbol is the result of looking it up in the current environment. That lookup process involves traversing the environment, frame by frame, until the symbol is found and the associated value is retrieved. The interpreter’s environment is constructed at run-time by closures extending a previous environment with bindings of formal to actual arguments.

A compiler can’t know the values of variables at compile time. It can however, determine the location those variables will have in the environment at run-time. A compiler will perform lexical analysis of code analagous to evaluation. It passes and (when entering a closure) extends a compile-time environment that contains only the symbols, not their values. When it comes across a variable access it looks up the symbol in the compile time environment and replaces the variable with its address in the environment (i.e.three frames back, two variables in).

At run time that data can rapidly be retrieved from the run-time environment (which contains only the data) without any laborious traversal and comparison.

That gives us three classes and a dumb data object for the location (all of this is pseudocode)

  1. A compile-time environment
  2. A run-time environment:
  3. And of course a terminating Null object for the CTE

Extenders for the CTE and RTE take arrays of symbols and values respectively, otherwise they are just the same as interpreter extend() methods.