System F and its variants are used frequently in the study of typed computation and an extended form, System FC, plays an important role in GHC's compilation process [1]. This post will attempt to translate the grammars of the Lambda Calculus, Simply Typed Lambda Calculus, and finally System F into a small subset of CoffeeScript while covering the basics of application and abstraction in each. Hopefully, through studying the basics here, readers who are interested in learning more about type theory and the lambda calculi will feel a little less intimidated by the notation and concepts.

## Lambda Calculus

Representing the Lambda Calculus only requires a small subset of CoffeeScript's total syntax. Let's define both grammars side by side.

In both cases `x` represents a variable and `t t` represents application of one term to another. The only real difference is the lambda abstraction syntax (red).

In the Lambda Calculus, abstraction involves preceding or wrapping a term `t` with `λx.t` which captures or binds the variable `x` inside the term `t`. In the example `t` is `λx.y`, using the abstraction `λy.t` creates a new term `λy.λx.y` (otherwise known as the K-combinator). Note that the `x` in `λx.t` shown in the grammar could be any variable like `y` or `z`.

In CoffeeScript we can do that same thing with the term `(x) -> y` by applying the CoffeeScript version of abstraction, yielding `(y) -> (x) -> y`.

The application of a term that shows two abstractions (`y` and `x`) to a single argument results in another term. The translation to JavaScript shows that a function object is returned ready for application. The concept of application in the Lambda Calculus is really the idea of substitution. You can see that the `z` is substituted for the instances of `y` in the body of the inner lambda term. Similarly in CoffeeScript the outer lambda puts `y` in scope and now all occurrences in the body of the lambda term will behave as `z`.

The notion of closed terms in the Lambda Calculus is a point of departure with CoffeeScript. A closed term has no free variables. For example, in `λx.y` the `y` variable is called free because it hasn't been bound by an enclosing abstractions. Adding an additional abstraction to get `λy.λx.y` captures the `y`. The JavaScript generated by the CoffeeScript `(x) -> y` will throw a reference error without a definition for `y` in scope, in contrast to the lambda term which will simply discard its argument and produce the `y`.

## Simply Typed Lambda Calculus

The Simply Typed Lambda Calculus expands on the Lambda Calculus with type information in abstractions.

It adds a type requirement to the argument of abstractions. The CoffeeScript equivalent adds a function that compares a type argument to the argument term. To keep things simple, `ifft` will throw an exception when the types don't line up.

``````# If and only if (iff) the type (t) is correct
ifft = (type, obj) ->
if !(obj instanceof type)
throw "Type mismatch"
``````

This definition assumes that the browser's `instanceof` implementation is behaving properly but certainly serves the purpose of illustration here. Assuming the type `Foo` is defined for the calculus and with `class Foo` in the CoffeeScript, we can add types to a simple example.

The types `τ` can represent are an important part of the Simply Typed Lambda Calculus. Some definitions provide a set of base types like natural numbers or booleans. Along with that comes a set of base constant values that can represent those types. For natural numbers a base constant of `0` and church numerals allows users to represent all the natural numbers. Here we've assumed the simple case allowing only the function type `τ → τ`, meaning every argument must be a lambda term.

Unfortunately even the simple case throws a rather large monkey wrench into the works. That's because there's no way to write `ifft` such that it can know or inspect the arguments type and return type of a lambda term (JavaScript function). In spite of that let's proceed to see what we can learn about System F.

## System F

System F adds the notion of polymorphic types to the Simply Typed Lambda Calculus. The term polymorphic carries a lot of baggage, but here it is parametric polymorphism [3]. That is, the type of a term can change depending on the setting.

System F makes two extensions. `Λα.e` is a type abstraction on the type variables in terms and `e [τ]` is the application of a type to a term that has been wrapped by a type abstraction. Note that the abstraction uses `α` to represent a type variable and `τ` to represent types that may or may not contain type variables. Since CoffeeScript's "types" are really constructor functions, all that's needed is an enclosing lambda to pull the type argument to `ifft` into scope and an application to a constructor function at runtime.

For System F the type abstraction is very specific. It works at the type level [4]. In CoffeeScript, on the other hand, it's just another lambda abstraction that puts the constructor function in scope as a lambda argument. In both cases when the term is applied to a type a substitution of the type for the type variable `α` takes place, just like regular (term) abstractions.

Again there is an important exception with regards to the types permitted in System F that makes the `ifft` even more inadequate than it was with the Simply Typed Lambda Calculus. Not only is there no way to write `ifft` so that it can properly check against lambda types but in addition System F defines universally quantified types. This means that a lambda can be polymorphic and operate without knowing anything about the type of its argument.

For example the identity combinator `Λα.λx:α.x`, or in CoffeeScript `(α) -> (x) -> ifft(α, x); x`, has the polymorphic type `∀α.α → α`. That is, its type isn't determined until a type application takes place or it "works" for all types. The issue arises when a combinator like identity is passed as an argument to another lambda term that expects a polymorphic function. Again, `ifft` can't check the types of a combinator if a type has been applied and it certainly can't check that the combinator is type agnostic in its dealings (polymorphic).

## Strong and Normal

System F has some really neat properties. Most importantly System F is strongly normalizing. That means that it always terminates and always reduces to a normal form when the terms are well typed (the types line up properly). That alone makes it worth studying.

It's also possible to make the type abstraction a bit more robust in the CoffeeScript by verifying that the argument is at least a function. A more adventuresome individual might alter CoffeeScript to annotate constructor function objects with a property that could be used to set them apart and compare them [5].

Even if we came up short of a really meaningful translation, hopefully it has demystified parts of how these calculi work. If you want to learn more I suggest reading Types and Programming Languages by Pierce (not an affiliate link).

### Footnotes

1. There are some interesting papers to read from Microsoft Research this particular extension of System F.
2. This is a more intrinsic approach to the translation as we aren't attempting to use types to reason about the terms/grammars.
3. Specifically rank-n polymorphism since the type variable `α` can be replaced by a quantified type.
4. This is actually captured in the reduction rules for System F.
5. Gasp! types in CoffeeScript.

15 Jan 2013