[prev in list] [next in list] [prev in thread] [next in thread]
List: haskell-cafe
Subject: [Haskell-cafe] typed final-tagless HOAS interpreter for linear lambda calculus
From: jeff p <mutjida () gmail ! com>
Date: 2013-03-26 8:15:04
Message-ID: CAJDEow03Zs3gMiDSDOS2yNO2hJ-7OR6Ctm7zkWbGtBBS=ccn7A () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
{-
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)"
-}
[Attachment #5 (text/html)]
<font face="courier new, monospace">{-<br><br>This message presents a typed \
final-tagless HOAS interpreter for<br>linear lambda calculus (LLC), which makes use \
of type families and<br>datatype promotion. This code is inspired by Oleg's LLC \
interpreter<br> using deBruijn indices<br>(<a \
href="http://okmij.org/ftp/tagless-final/course/LinearLC.hs">http://okmij.org/ftp/tagless-final/course/LinearLC.hs</a>). \
</font><div><font face="courier new, monospace"><br></font></div><div> <div><font \
face="courier new, monospace">The basic technique used here, and in Oleg's \
representation, comes</font></div><div><font face="courier new, monospace">from work \
on linear logic programming (see</font></div><div> <font face="courier new, \
monospace"><a href="http://www.cs.cmu.edu/~fp/papers/erm97.pdf">http://www.cs.cmu.edu/~fp/papers/erm97.pdf</a> \
for details). An explicit</font></div><div><font face="courier new, \
monospace">presentation of LLC using these ideas can be found here</font></div> \
<div><font face="courier new, monospace"><a \
href="http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linfp.pdf">http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linfp.pdf</a> \
[0].</font></div><div><font face="courier new, monospace"><br> </font></div><font \
face="courier new, monospace">While only the two arrow types and ints are included in \
this message;<br>it is straightforward to extend this interpreter to cover all types \
of<br>LLC. Attached to this message is an interpreter for full LLC<br> (including \
additives and units) which is a direct transcription of the<br>typing rules \
previously mentioned in [0]. The code for full LLC is<br>written using MPTC and \
functional dependencies, instead of type<br>families, but it is easily translatable \
to type families.<br> <br>-}<br><br>{-# LANGUAGE<br> DataKinds,<br> \
KindSignatures,<br> RankNTypes, <br> TypeFamilies,<br> TypeOperators,<br> \
UndecidableInstances<br> #-}<br><br>{-<br><br>The basic idea is to label each linear \
variable with a number and keep<br> track of the linear context in the type of the \
representation. Thus<br>our representation type looks like:<br><br> repr :: Nat \
-> [Maybe Nat] -> [Maybe Nat] -> * -> *<br> repr vid hi ho \
a<br><br>where vid is the next variable label to use, hi is the input linear<br> \
hypotheses, ho is the output linear hypotheses, and a is the type of<br>the \
term.<br><br>-}<br><br>-- Type-level Nat<br>--<br>data Nat = Z | S Nat<br><br>-- \
Type-level equality for Nat<br>--<br>type family EqNat (x::Nat) (y::Nat) :: Bool<br> \
type instance EqNat Z Z = True<br>type instance EqNat (S x) (S y) = EqNat x y<br>type \
instance EqNat Z (S y) = False<br>type instance EqNat (S x) Z = \
False<br><br>{-<br><br>The key to enforcing linearity, is to have the type system \
consume<br> (mark as used) linear variables as they are used. We use \
promoted<br>[Maybe Nat] to represent a linear context.<br><br>-}<br><br>-- Type-level \
function to consume a given resource (a Maybe Nat) form a list.<br>--<br>type family \
Consume (vid::Nat) (i::[Maybe Nat]) :: [Maybe Nat]<br> type family Consume1 (b::Bool) \
(vid::Nat) (v::Nat) (vs::[Maybe Nat]) :: [Maybe Nat]<br>type instance Consume vid \
(Nothing ': vs) = (Nothing ': Consume vid vs)<br>type instance Consume vid \
(Just v ': vs) = Consume1 (EqNat vid v) vid v vs<br> type instance Consume1 True \
vid v vs = Nothing ': vs<br>type instance Consume1 False vid v vs = Just v ': \
Consume vid vs<br><br>{-<br><br>HOAS boils down to having the obect langauge (LLC) \
directly use the<br>meta language (Haskell) variable and substitution machinery. So \
a<br> typical HOAS representation of an object level function looks<br>something \
like:<br><br> lam :: (repr a -> repr b) -> repr (a -> b)<br><br>The key \
to making HOAS work with our representation, is to have our<br> object level \
variables make use of the Consume function above. Toward<br>this end, we can create a \
general linear variable type.<br><br>-}<br><br>type VarTp (repr :: Nat -> [Maybe \
Nat] -> [Maybe Nat] -> * -> *) vid a = forall v i o . repr v i (Consume vid \
i) a<br> <br>{-<br><br>We can now write the representation of the LLC terms. Note \
that the<br>type of each LLC term constructor (each member of class Lin) is \
a<br>transcription of a typing rule for LLC. <br><br>-}<br><br>-- a type to \
distinguish linear functions from regular functions<br>
--<br>newtype a -<> b = Lolli {unLolli :: a -> b}<br><br>-- the \
"Symantics" of LLC<br>--<br>class Lin (repr :: Nat -> [Maybe Nat] -> \
[Maybe Nat] -> * -> *) where<br> -- a base type<br> int :: Int -> repr \
vid hi hi Int<br> add :: repr vid hi h Int -> repr vid h ho Int -> repr vid hi \
ho Int<br><br> -- linear lambda<br> llam :: (VarTp repr vid a -> repr (S \
vid) (Just vid ': hi) (Nothing ': ho) b) -> repr vid hi ho (a -<> \
b)<br> (<^>) :: repr vid hi h (a -<> b) -> repr vid h ho a -> repr \
vid hi ho b<br><br> -- non-linear lambda<br> lam :: ((forall v h . repr v h h \
a) -> repr vid hi ho b) -> repr vid hi ho (a -> b)<br> (<$>) :: repr \
vid hi ho (a -> b) -> repr vid ho ho a -> repr vid hi ho \
b<br><br>{-<br><br>An evaluator which takes a LLC term of type a to a Haskell value \
of<br>type a.<br><br>-}<br>newtype R (vid::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) a = \
R {unR :: a}<br> <br>instance Lin R where<br> int = R <br> add x y = R $ unR x \
+ unR y<br><br> llam f = R $ Lolli $ \x -> unR (f (R x))<br> f <^> x = \
R $ unLolli (unR f) (unR x)<br><br> lam f = R $ \x -> unR (f (R x))<br> f \
<$> x = R $ unR f (unR x)<br><br>eval :: R Z '[] '[] a -> a<br>eval \
= unR<br><br>{-<br><br>Some examples:<br><br> *Main> :t eval $ llam $ \x -> \
x<br> eval $ llam $ \x -> x :: b -<> b<br> <br> *Main> :t eval $ \
llam $ \x -> add x (int 1)<br> eval $ llam $ \x -> add x (int 1) :: Int \
-<> Int<br><br> *Main> eval $ (llam $ \x -> add x (int 1)) <^> \
int 2<br> 3<br><br>A non-linear uses of linear variables fail to type check:<br> \
<br> *Main> :t eval $ llam $ \x -> add x x<br><br> \
<interactive>:1:27:<br> Couldn't match type `Consume 'Z ('[] \
(Maybe Nat))'<br> with '[] (Maybe Nat)<br> \
Expected type: R ('S 'Z)<br> ((':) (Maybe Nat) ('Nothing Nat) \
('[] (Maybe Nat)))<br> ((':) (Maybe Nat) \
('Nothing Nat) ('[] (Maybe Nat)))<br> Int<br> \
Actual type: R ('S 'Z)<br> ((':) (Maybe Nat) ('Nothing Nat) ('[] \
(Maybe Nat)))<br> (Consume 'Z ((':) (Maybe Nat) \
('Nothing Nat) ('[] (Maybe Nat))))<br> Int<br> In \
the second argument of `add', namely `x'<br> In the expression: add x \
x<br> In the second argument of `($)', namely `\ x -> add x \
x'<br><br> *Main> :t eval $ llam $ \x -> llam $ \y -> add x (int \
1)<br> <br> <interactive>:1:38:<br> Couldn't match type 'Just \
Nat ('S 'Z) with 'Nothing Nat<br> Expected type: R ('S ('S \
'Z))<br> ((':)<br> (Maybe \
Nat)<br> ('Just Nat ('S 'Z))<br> ((':) \
(Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat))))<br> \
((':)<br> (Maybe Nat)<br> ('Nothing Nat)<br> \
((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))))<br> \
Int<br> Actual type: R ('S ('S 'Z))<br> ((':)<br> \
(Maybe Nat)<br> ('Just Nat ('S 'Z))<br> \
((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat))))<br> \
(Consume<br> 'Z<br> \
((':)<br> (Maybe Nat)<br> \
('Just Nat ('S 'Z))<br> ((':) (Maybe Nat) ('Just Nat 'Z) \
('[] (Maybe Nat)))))<br> Int<br> In the first \
argument of `add', namely `x'<br> In the expression: add x (int 1)<br> \
In the second argument of `($)', namely `\ y -> add x (int 1)'<br><br>But \
non-linear uses of regular variables are fine:<br><br> *Main> :t eval $ lam $ \
\x -> add x x<br> eval $ lam $ \x -> add x x :: Int -> Int<br> <br> \
*Main> eval $ (lam $ \x -> add x x) <$> int 1<br> 2<br><br> \
*Main> :t eval $ lam $ \x -> lam $ \y -> add x (int 1)<br> eval $ lam $ \
\x -> lam $ \y -> add x (int 1) :: Int -> a -> Int<br> <br> *Main> \
eval $ (lam $ \x -> lam $ \y -> add x (int 1)) <$> int 1 <$> int \
2<br> 2<br><br>-}<br><br>{-<br><br>We can also easily have an evaluator which \
produces a String.<br><br>-}<br><br>-- For convenience, we name linear variables x0, \
x1, ... and regular variables y0, y1, ...<br>
--<br>newtype Str (vid::Nat) (gi::[Maybe Nat]) (go::[Maybe Nat]) a = Str {unStr :: \
Int -> Int -> String}<br><br>instance Lin Str where<br> int x = Str $ \_ _ \
-> show x<br> add x y = Str $ \uv lv -> "(" ++ unStr x uv lv ++ \
" + " ++ unStr y uv lv ++ ")"<br> <br> llam f = Str $ \uv lv \
-> let v = "x"++show lv in <br> "\\" \
++ v ++ " -<> " ++ unStr (f $ Str (\_ _ -> v)) uv (lv + 1)<br> \
f <^> x = Str $ \uv lv -> "(" ++ unStr f uv lv ++ " ^ " \
++ unStr x uv lv ++ ")"<br> <br> lam f = Str $ \uv lv -> let v = \
"y"++show uv in <br> "\\" ++ v ++ \
" -> " ++ unStr (f $ Str (\_ _ -> v)) (uv + 1) lv<br> f <$> \
x = Str $ \uv lv -> "(" ++ unStr f uv lv ++ " " ++ unStr x uv \
lv ++ ")"<br> <br>showLin :: Str Z '[] '[] a -> \
String<br>showLin x = unStr x 0 0<br><br>{-<br><br>An example:<br><br> *Main> \
showLin $ (llam $ \x -> llam $ \y -> add x y) <^> int 1<br> \
"(\\x0 -<> \\x1 -<> (x0 + x1) ^ 1)"<br> <br>-}</font><br></div>
--14dae9399607cee7d904d8cf84cc--
["linear.hs" (application/octet-stream)]
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic