## Introduction

This tutorial is inspired by Oleg Kiselyov's typed tagless-final
[linear lambda calculus
interpreter](http://http://okmij.org/ftp/tagless-final/course/LinearLC.hs). In
particular, I will explain how to extend Oleg's interpreter, which
uses a first-order ([deBruijn
index](http://en.wikipedia.org/wiki/De_Bruijn_index)) representation of LLC,
to an interpreter which uses a higher-order ([higher-order abstract syntax](http://en.wikipedia.org/wiki/Higher-order_abstract_syntax)) representation of LLC. 
In order to accomplish this, I will make use of several advanced Haskell
features including _higher-rank polymorphism_, _type families_, and
_promoted data kinds_.  After showing the representation for a minimal
linear lambda calculus (LLC), just lambdas and applications, I will
extend the interpreter to a full LLC (including additive and unit
types); and finally, I will add recursive types to allow standard
programming examples to be written.

## Linear Lambda Calculus

Before diving in, I will attempt to give a brief summary of LLC; a
more thorough summary can be found in Frank Pfenning's [online
notes](http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linlam.pdf).

A linear lambda is a function which must use its argument exactly
once. I use `-<>` as concrete syntax for a linear function type, `\x
-<> e` as concrete syntax for a linear lambda with argument `x` and
body `e`, and `f ^ x` as concrete syntax for linear application.
```haskell
-- show Grammar for LLC
m ::= x | \x -<> m | m ^ m
```
Thus the following is a valid linear lambda:

``` haskell
\f -<> \x -<> f ^ x
```
with type
``` haskell
(a -<> b) -<> a -<> b
```
while the following are not:
``` haskell
\f -<> \x -<> f ^ x ^ x  -- uses linear variable x twice

\f -<> \x -<> x  -- doesn't use linear variable f
```

### Some Type Theory

The linearity of linear lambdas is syntactically expressed in their
typing rules, which are built on the following judgement

```
D  |-  m :: A
```

denoting that term `m` has type `A` in linear context `D`, where
`D` is a set of typed variables-- so we assume all variables have
unique names, which can always be achieved via alpha conversion.

The typing rules for (minimal) LLC are as follows:
```
-------------- (lvar)     
x::A  |-  x :: A            


   D, x::A  |-  m :: B
-------------------------- (-<>I)
D  |-  \x -<> m :: A -<> B


D  |-  m :: A -<> B     D'  |-  n :: A
-------------------------------------- (-<>E)
      D union D'  |-  m ^ n :: B
```

Linearity is the consequence of the `lvar` rule requiring that only
one variable be in the linear context (thus no variables can be
ignored); and of the `-<>E` rule splitting the linear context beween
it's two subtrees (thus no variable can be used more than once). For the curious: the `I` and `E` stand for introduction and elimination since when read from premise to conclusion, `I` rules introduce (show how to construct) a type, while `E` rules eliminate (show how to use) a type.

Here is a complete typing derivation for `\f -<> \x -<> f ^ x`:

```
---------------------------- (lvar)      ---------------- (lvar)
f::A -<> B  |-  f :: A -<> B             x::A  |-  x :: A
--------------------------------------------------------- (-<>E)
f::A -<> B, x::A  |-  f ^ x :: B
--------------------------------------- (-<>I)
f::A -<> B  |-  \x -<> f ^ x :: A -<> B
-------------------------------------------------- (-<>I)
  |-  \f -<> \x -<> f ^ x :: (A -<> B) -<> A -<> B
```

Type checkers generally follow the structure of the term they are checking and thus, in the context of type checking, typing rules are usually read from conclusion to premise.
Therefore, the typing rules above are not suitable for implementing a type
checking (or inference) algorithm for LLC due to the need to split the
linear context in the `-<>E` rule-- it would not be feasible
to try every possible splitting until one succeeds. 

### Algorithmic type checking

LLC typing rules can be recast in a more
algorithmic fashion by lazily splitting the linear context,
i.e. passing everything to the first branch and then giving the
leftovers to the second branch; this technique comes from [linear logic programming](http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-158/index.html). To this end, we change our typing judgement to have the form:

```
Di \ Do  |-  m :: A
```
where `Di` is the input linear context and `Do` is the output linear
context and `Di - Do` is the actual linear context used in the
derivation; the derivations must maintain the constraint that `Di` is
a superset of `Do`. Here are the typing rules:

```
--------------------- (lvar)     
D, x::A \ D  |-  x :: A            


Di, x::A \ Do  |-  m :: B   (x not in Do)
----------------------------------------- (-<>I)
Di \ Do  |-  \x -<> m :: A -<> B


Di \ D  |-  m :: A -<> B     D \ Do  |-  n :: A
----------------------------------------------- (-<>E)
            Di \ Do  |-  m ^ n :: B
```
These rules can be easily implemented. 

## Typed Tagless-Final Interpreters

Writing a typed tagless-final interpreter for a language can be
thought of as an exercise in transcribing the typing rules of the
language into Haskell types. A much more comprehensive (and perhaps
comprehensible) presentation of the typed tagless-final approach can be
found in [Oleg's
notes](http://okmij.org/ftp/tagless-final/course/lecture.pdf).

The preceding algorithmic typing rules are so easy to implement that
they can be directly encoded as Haskell types. I will present two such
encodings. The first encoding will show how a presentation of the
preceding rules, modified to work with a deBruijn index based calculus
(rather than explicit named variables), can be directly, and simply,
encoded in Haskell types. The second encoding will keep the explicitly
named variables (and use HOAS) and directly model the rules above at
the cost of slightly more complicated Haskell types.