## First-order, deBruijn Index Based Interpreter

This section is my own presentation, and explanation, of Oleg's LLC interpreter. First, I will change the presentation of the language to use deBruijn indices:

```
-- show Grammar for LLC with deBruijn Indices
m ::= z | s m | llam m | m ^ m
```

and slightly modify the algorithmic typing rules above to use an
ordered list for the linear context (actually an ordered list of `Maybe`

types, where `Just`

is implicit and `_`

is `Nothing`

), instead of a
set:

```
------------------------ (lvar-z)
A, D \ _, D |- z :: A
Di \ Do |- m :: A
--------------------------- (lvar-s)
B, Di \ B, Do |- s m :: A
A, Di \ _, Do |- m :: B
----------------------------- (-<>I)
Di \ Do |- lam m :: A -<> B
Di \ D |- m :: A -<> B D \ Do |- n :: A
----------------------------------------------- (-<>E)
Di \ Do |- m ^ n :: B
```

Note that in rule `lvar-s`

, `B`

can be either `_`

or some type `A`

.

I will use well-typed haskell terms:

`m :: repr hi ho a`

to represent the judgement:

`Di \ Do |- m :: A`

The following is a direct transcription of the above typing rules into Haskell types.

```
-- /show
{-# LANGUAGE
NoMonomorphismRestriction,
FlexibleInstances,
MultiParamTypeClasses,
TypeOperators
#-}
-- show
-- type level Maybe for representing elements of the linear context
newtype F a = F a
data U = Used
class Linear repr where
z :: repr (F a, h) (U, h) a
s :: repr hi ho a -> repr (any, hi) (any, ho) a
llam :: repr (F a, hi) (U, ho) b -> repr hi ho (a -> b)
(<^>) :: repr hi h (a -> b) -> repr h ho a -> repr hi ho b
t0 = llam $ llam $ s z <^> z
-- inferred type of t0 :: Linear repr => repr h h ((a -> b) -> a -> b)
-- following won't type check
-- t1 = llam $ llam $ s z <^> z <^> z
main = putStrLn "ok"
```

Note that the return type of `llam`

contains a Haskell function. Although the syntax uses deBruijn notation, linear functions are being represented by Haskell functions; so the `llam`

method of any instance of `Linear`

will have to create a Haskell function.
Another interesting observation about the code above is that *Haskell's type checker is enforcing linearity* for us; as of yet, there is no instance for the class `Linear`

.

In order to have an instance for `Linear`

which lets us
evaluate LLC expressions, we need a suitable type, call it
`R`

, to concretely represent our LLC terms. Since the language uses deBruijn indices, we will need to have an
explicit representation of the linear context around at runtime.

```
-- /show
{-# LANGUAGE
NoMonomorphismRestriction,
FlexibleInstances,
MultiParamTypeClasses,
TypeOperators
#-}
-- type level Maybe for representing elements of the linear context
newtype F a = F a
data U = Used
class Linear repr where
z :: repr (F a, h) (U, h) a
s :: repr hi ho a -> repr (x, hi) (x, ho) a
llam :: repr (F a, hi) (U, ho) b -> repr hi ho (a -> b)
(<^>) :: repr hi h (a -> b) -> repr h ho a -> repr hi ho b
-- show
-- Typed and tagless evaluator
-- object term ==> metalanguage value
newtype R hi ho a = R {unR :: hi -> (a, ho)}
instance Linear R where
z = R $ \(F x, h) -> (x, (Used, h))
s v = R $ \(any, hi) ->
let (x, ho) = unR v hi
in (x, (any, ho))
-- !!! Following does not work since vo is not in scope !!!
--
llam e = R $ \hi -> (f hi, vo)
where f hi x = let (v, vo) = unR e (F x,hi)
in v
m1 <^> m2 = R $ \hi -> let (v1, h) = unR m1 hi
(v2, ho) = unR m2 h
in (v1 v2, ho)
```

As noted above, this code doesn't type check since the output linear
context needed by `llam`

is unknown; it won't be computed until the
function is actually applied. However, there is a
way to get around this problem; the input context and the type of the
output context (which is statically determined) are enough to generate
the actual output context. A type class can
be used to generate an output context from an input context and the known output context type.

```
class HiHo hi ho where
hiho :: hi -> ho
instance HiHo () () where
hiho = id
instance HiHo hi ho => HiHo (F a , hi) (F a , ho) where
hiho (x, hi) = (x, hiho hi)
instance HiHo hi ho => HiHo (U , hi) (U , ho) where
hiho (x, hi) = (x, hiho hi)
instance HiHo hi ho => HiHo (F a, hi) (U, ho) where
hiho (x, hi) = (Used, hiho hi)
```

In order to let `llam`

use `hiho`

, its type-level linear contexts must be exposed. However, I don't want to add these to `Linear`

since neither `z`

nor `<^>`

mention exactly two type-level linear contexts; therefore, I will add another class, `LinearLam`

,
just for `llam`

.

```
class Linear repr where
z :: repr (F a , h) (U , h) a
s :: repr hi ho a -> repr (x , hi) (x , ho) a
(<^>) :: repr hi h (a -> b) -> repr h ho a -> repr hi ho b
class LinearLam repr hi ho where
llam :: repr (F a , hi) (U , ho) b -> repr hi ho (a -> b)
```

I can now write correct instances of `Linear`

and `LinearLam`

for `R`

as well as an evaluator for terms of type `R`

:

```
-- /show
{-# LANGUAGE
NoMonomorphismRestriction,
FlexibleInstances,
MultiParamTypeClasses,
TypeOperators
#-}
-- type level Maybe for representing elements of the linear context
newtype F a = F a
data U = Used
class HiHo hi ho where
hiho :: hi -> ho
instance HiHo () () where
hiho = id
instance HiHo hi ho => HiHo (F a , hi) (F a , ho) where
hiho (x, hi) = (x, hiho hi)
instance HiHo hi ho => HiHo (U , hi) (U , ho) where
hiho (x, hi) = (x, hiho hi)
instance HiHo hi ho => HiHo (F a, hi) (U, ho) where
hiho (x, hi) = (Used, hiho hi)
class Linear repr where
z :: repr (F a , h) (U , h) a
s :: repr hi ho a -> repr (x , hi) (x , ho) a
(<^>) :: repr hi h (a -> b) -> repr h ho a -> repr hi ho b
class LinearLam repr hi ho where
llam :: repr (F a , hi) (U , ho) b -> repr hi ho (a -> b)
-- show
-- Typed and tagless evaluator
-- object term ==> metalanguage value
newtype R hi ho a = R {unR :: hi -> (a, ho)}
instance Linear R where
z = R $ \(F x, h) -> (x, (Used, h))
s v = R $ \(any, hi) ->
let (x, ho) = unR v hi
in (x, (any, ho))
m1 <^> m2 = R $ \hi -> let (v1, h) = unR m1 hi
(v2, ho) = unR m2 h
in (v1 v2, ho)
instance HiHo hi ho => LinearLam R hi ho where
llam e = R $ \hi -> (f hi, hiho hi)
where f hi x = let (v, _) = unR e (F x, hi)
in v
-- The implementation of lam shows that the value of lam, which is
-- f hi, is the closure of the (input) environment in which
-- lam was produced.
eval :: R () () a -> a
eval e = fst $ unR e () -- Eval in the empty environment
t = llam $ llam $ s z <^> z
main = do
putStrLn $ eval (t <^> llam z) "I was passed to a real function."
putStrLn "ok"
```