{- 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 http://www.cs.cmu.edu/~fp/papers/erm97.pdf for details). An explicit presentation of LLC using these ideas can be found here http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linfp.pdf [0]. 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)" -}