26 Mar 2013 09:15

## typed final-tagless HOAS interpreter for linear lambda calculus

{-

This message presents a typed final-tagless HOAS interpreter for
linear lambda calculus (LLC), which makes use of type families and
datatype promotion. This code is inspired by Oleg's LLC interpreter
using deBruijn indices
(http://okmij.org/ftp/tagless-final/course/LinearLC.hs).

The basic technique used here, and in Oleg's representation, comes
from work on linear logic programming (see
presentation of LLC using these ideas can be found here

While only the two arrow types and ints are included in this message;
it is straightforward to extend this interpreter to cover all types of
LLC. Attached to this message is an interpreter for full LLC
(including additives and units) which is a direct transcription of the
typing rules previously mentioned in [0]. The code for full LLC is
written using MPTC and functional dependencies, instead of type
families, but it is easily translatable to type families.

-}

{-# LANGUAGE
DataKinds,
KindSignatures,
RankNTypes,
TypeFamilies,
TypeOperators,
UndecidableInstances
#-}

{-

The basic idea is to label each linear variable with a number and keep
track of the linear context in the type of the representation. Thus
our representation type looks like:

repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> *
repr vid hi ho a

where vid is the next variable label to use, hi is the input linear
hypotheses, ho is the output linear hypotheses, and a is the type of
the term.

-}

-- Type-level Nat
--
data Nat = Z | S Nat

-- Type-level equality for Nat
--
type family EqNat (x::Nat) (y::Nat) :: Bool
type instance EqNat Z Z = True
type instance EqNat (S x) (S y) = EqNat x y
type instance EqNat Z (S y) = False
type instance EqNat (S x) Z = False

{-

The key to enforcing linearity, is to have the type system consume
(mark as used) linear variables as they are used. We use promoted
[Maybe Nat] to represent a linear context.

-}

-- Type-level function to consume a given resource (a Maybe Nat) form a list.
--
type family Consume (vid::Nat) (i::[Maybe Nat]) :: [Maybe Nat]
type family Consume1 (b::Bool) (vid::Nat) (v::Nat) (vs::[Maybe Nat]) :: [Maybe Nat]
type instance Consume vid (Nothing ': vs) = (Nothing ': Consume vid vs)
type instance Consume vid (Just v ': vs) = Consume1 (EqNat vid v) vid v vs
type instance Consume1 True vid v vs = Nothing ': vs
type instance Consume1 False vid v vs = Just v ': Consume vid vs

{-

HOAS boils down to having the obect langauge (LLC) directly use the
meta language (Haskell) variable and substitution machinery. So a
typical HOAS representation of an object level function looks
something like:

lam :: (repr a -> repr b) -> repr (a -> b)

The key to making HOAS work with our representation, is to have our
object level variables make use of the Consume function above. Toward
this end, we can create a general linear variable type.

-}

type VarTp (repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> *) vid a = forall v i o . repr v i (Consume vid i) a

{-

We can now write the representation of the LLC terms. Note that the
type of each LLC term constructor (each member of class Lin) is a
transcription of a typing rule for LLC.

-}

-- a type to distinguish linear functions from regular functions
--
newtype a -<> b = Lolli {unLolli :: a -> b}

-- the "Symantics" of LLC
--
class Lin (repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
-- a base type
int :: Int -> repr vid hi hi Int
add :: repr vid hi h Int -> repr vid h ho Int -> repr vid hi ho Int

-- linear lambda
llam :: (VarTp repr vid a -> repr (S vid) (Just vid ': hi) (Nothing ': ho) b) -> repr vid hi ho (a -<> b)
(<^>) :: repr vid hi h (a -<> b) -> repr vid h ho a -> repr vid hi ho b

-- non-linear lambda
lam :: ((forall v h . repr v h h a) -> repr vid hi ho b) -> repr vid hi ho (a -> b)
(<\$>) :: repr vid hi ho (a -> b) -> repr vid ho ho a -> repr vid hi ho b

{-

An evaluator which takes a LLC term of type a to a Haskell value of
type a.

-}
newtype R (vid::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) a = R {unR :: a}

instance Lin R where
int = R
add x y = R \$ unR x + unR y

llam f = R \$ Lolli \$ \x -> unR (f (R x))
f <^> x = R \$ unLolli (unR f) (unR x)

lam f = R \$ \x -> unR (f (R x))
f <\$> x = R \$ unR f (unR x)

eval :: R Z '[] '[] a -> a
eval = unR

{-

Some examples:

*Main> :t eval \$ llam \$ \x -> x
eval \$ llam \$ \x -> x :: b -<> b

*Main> :t eval \$ llam \$ \x -> add x (int 1)
eval \$ llam \$ \x -> add x (int 1) :: Int -<> Int

*Main> eval \$ (llam \$ \x -> add x (int 1)) <^> int 2
3

A non-linear uses of linear variables fail to type check:

*Main> :t eval \$ llam \$ \x -> add x x

<interactive>:1:27:
Couldn't match type `Consume 'Z ('[] (Maybe Nat))'
with '[] (Maybe Nat)
Expected type: R ('S 'Z)
((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat)))
((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat)))
Int
Actual type: R ('S 'Z)
((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat)))
(Consume 'Z ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))))
Int
In the second argument of `add', namely `x'
In the expression: add x x
In the second argument of `(\$)', namely `\ x -> add x x'

*Main> :t eval \$ llam \$ \x -> llam \$ \y -> add x (int 1)

<interactive>:1:38:
Couldn't match type 'Just Nat ('S 'Z) with 'Nothing Nat
Expected type: R ('S ('S 'Z))
((':)
(Maybe Nat)
('Just Nat ('S 'Z))
((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat))))
((':)
(Maybe Nat)
('Nothing Nat)
((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))))
Int
Actual type: R ('S ('S 'Z))
((':)
(Maybe Nat)
('Just Nat ('S 'Z))
((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat))))
(Consume
'Z
((':)
(Maybe Nat)
('Just Nat ('S 'Z))
((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat)))))
Int
In the first argument of `add', namely `x'
In the expression: add x (int 1)
In the second argument of `(\$)', namely `\ y -> add x (int 1)'

But non-linear uses of regular variables are fine:

*Main> :t eval \$ lam \$ \x -> add x x
eval \$ lam \$ \x -> add x x :: Int -> Int

*Main> eval \$ (lam \$ \x -> add x x) <\$> int 1
2

*Main> :t eval \$ lam \$ \x -> lam \$ \y -> add x (int 1)
eval \$ lam \$ \x -> lam \$ \y -> add x (int 1) :: Int -> a -> Int

*Main> eval \$ (lam \$ \x -> lam \$ \y -> add x (int 1)) <\$> int 1 <\$> int 2
2

-}

{-

We can also easily have an evaluator which produces a String.

-}

-- For convenience, we name linear variables x0, x1, ... and regular variables y0, y1, ...
--
newtype Str (vid::Nat) (gi::[Maybe Nat]) (go::[Maybe Nat]) a = Str {unStr :: Int -> Int -> String}

instance Lin Str where
int x = Str \$ \_ _ -> show x
add x y = Str \$ \uv lv -> "(" ++ unStr x uv lv ++ " + " ++ unStr y uv lv ++ ")"

llam f = Str \$ \uv lv -> let v = "x"++show lv in
"\\" ++ v ++ " -<> " ++ unStr (f \$ Str (\_ _ -> v)) uv (lv + 1)
f <^> x = Str \$ \uv lv -> "(" ++ unStr f uv lv ++ " ^ " ++ unStr x uv lv ++ ")"

lam f = Str \$ \uv lv -> let v = "y"++show uv in
"\\" ++ v ++ " -> " ++ unStr (f \$ Str (\_ _ -> v)) (uv + 1) lv
f <\$> x = Str \$ \uv lv -> "(" ++ unStr f uv lv ++ " " ++ unStr x uv lv ++ ")"

showLin :: Str Z '[] '[] a -> String
showLin x = unStr x 0 0

{-

An example:

*Main> showLin \$ (llam \$ \x -> llam \$ \y -> add x y) <^> int 1
"(\\x0 -<> \\x1 -<> (x0 + x1) ^ 1)"

-}
Attachment (linear.hs): application/octet-stream, 8 KiB
```_______________________________________________