## First-order, deBruijn Index Based Interpreter

This section is my own presentation, and explanation, of [Oleg's LLC
interpreter](http://okmij.org/ftp/tagless-final/course/LinearLC.hs).
First, I will change the presentation of the language to use deBruijn indices:
```haskell
-- 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:
```haskell
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.

```active haskell
-- /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.

```active haskell
-- /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. 

```haskell
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`.

```haskell
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`:

```active haskell
-- /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"
```