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"