<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&#39;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&#39;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 -&gt; [Maybe Nat] -&gt; [Maybe Nat] -&gt; * -&gt; *<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 &#39;: vs) = (Nothing &#39;: Consume vid vs)<br>type instance Consume vid (Just v &#39;: vs) = Consume1 (EqNat vid v) vid v vs<br>
type instance Consume1 True vid v vs = Nothing &#39;: vs<br>type instance Consume1 False vid v vs = Just v &#39;: 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 -&gt; repr b) -&gt; repr (a -&gt; 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 -&gt; [Maybe Nat] -&gt; [Maybe Nat] -&gt; * -&gt; *) 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 -&lt;&gt; b = Lolli {unLolli :: a -&gt; b}<br><br>-- the &quot;Symantics&quot; of LLC<br>--<br>class Lin (repr :: Nat -&gt; [Maybe Nat] -&gt; [Maybe Nat] -&gt; * -&gt; *) where<br>    -- a base type<br>    int :: Int -&gt; repr vid hi hi Int<br>
    add :: repr vid hi h Int -&gt; repr vid h ho Int -&gt; repr vid hi ho Int<br><br>    -- linear lambda<br>    llam :: (VarTp repr vid a -&gt; repr (S vid) (Just vid &#39;: hi) (Nothing &#39;: ho) b) -&gt; repr vid hi ho (a -&lt;&gt; b)<br>
    (&lt;^&gt;) :: repr vid hi h (a -&lt;&gt; b) -&gt; repr vid h ho a -&gt; repr vid hi ho b<br><br>    -- non-linear lambda<br>    lam :: ((forall v h . repr v h h a) -&gt; repr vid hi ho b) -&gt; repr vid hi ho (a -&gt; b)<br>
    (&lt;$&gt;) :: repr vid hi ho (a -&gt; b) -&gt; repr vid ho ho a -&gt; 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 -&gt; unR (f (R x))<br>    f &lt;^&gt; x = R $ unLolli (unR f) (unR x)<br><br>    lam f = R $ \x -&gt; unR (f (R x))<br>
    f &lt;$&gt; x = R $ unR f (unR x)<br><br>eval :: R Z &#39;[] &#39;[] a -&gt; a<br>eval = unR<br><br>{-<br><br>Some examples:<br><br>    *Main&gt; :t eval $ llam $ \x -&gt; x<br>    eval $ llam $ \x -&gt; x :: b -&lt;&gt; b<br>
<br>    *Main&gt; :t eval $ llam $ \x -&gt; add x (int 1)<br>    eval $ llam $ \x -&gt; add x (int 1) :: Int -&lt;&gt; Int<br><br>    *Main&gt; eval $ (llam $ \x -&gt; add x (int 1)) &lt;^&gt; int 2<br>    3<br><br>A non-linear uses of linear variables fail to type check:<br>
<br>    *Main&gt; :t eval $ llam $ \x -&gt; add x x<br><br>    &lt;interactive&gt;:1:27:<br>        Couldn&#39;t match type `Consume &#39;Z (&#39;[] (Maybe Nat))&#39;<br>                      with &#39;[] (Maybe Nat)<br>        Expected type: R (&#39;S &#39;Z)<br>
                         ((&#39;:) (Maybe Nat) (&#39;Nothing Nat) (&#39;[] (Maybe Nat)))<br>                         ((&#39;:) (Maybe Nat) (&#39;Nothing Nat) (&#39;[] (Maybe Nat)))<br>                         Int<br>          Actual type: R (&#39;S &#39;Z)<br>
                         ((&#39;:) (Maybe Nat) (&#39;Nothing Nat) (&#39;[] (Maybe Nat)))<br>                         (Consume &#39;Z ((&#39;:) (Maybe Nat) (&#39;Nothing Nat) (&#39;[] (Maybe Nat))))<br>                         Int<br>
        In the second argument of `add&#39;, namely `x&#39;<br>        In the expression: add x x<br>        In the second argument of `($)&#39;, namely `\ x -&gt; add x x&#39;<br><br>    *Main&gt; :t eval $ llam $ \x -&gt; llam $ \y -&gt; add x (int 1)<br>
<br>    &lt;interactive&gt;:1:38:<br>        Couldn&#39;t match type &#39;Just Nat (&#39;S &#39;Z) with &#39;Nothing Nat<br>        Expected type: R (&#39;S (&#39;S &#39;Z))<br>                         ((&#39;:)<br>                            (Maybe Nat)<br>
                            (&#39;Just Nat (&#39;S &#39;Z))<br>                            ((&#39;:) (Maybe Nat) (&#39;Just Nat &#39;Z) (&#39;[] (Maybe Nat))))<br>                         ((&#39;:)<br>                            (Maybe Nat)<br>
                            (&#39;Nothing Nat)<br>                            ((&#39;:) (Maybe Nat) (&#39;Nothing Nat) (&#39;[] (Maybe Nat))))<br>                         Int<br>          Actual type: R (&#39;S (&#39;S &#39;Z))<br>
                         ((&#39;:)<br>                            (Maybe Nat)<br>                            (&#39;Just Nat (&#39;S &#39;Z))<br>                            ((&#39;:) (Maybe Nat) (&#39;Just Nat &#39;Z) (&#39;[] (Maybe Nat))))<br>
                         (Consume<br>                            &#39;Z<br>                            ((&#39;:)<br>                               (Maybe Nat)<br>                               (&#39;Just Nat (&#39;S &#39;Z))<br>
                               ((&#39;:) (Maybe Nat) (&#39;Just Nat &#39;Z) (&#39;[] (Maybe Nat)))))<br>                         Int<br>        In the first argument of `add&#39;, namely `x&#39;<br>        In the expression: add x (int 1)<br>
        In the second argument of `($)&#39;, namely `\ y -&gt; add x (int 1)&#39;<br><br>But non-linear uses of regular variables are fine:<br><br>    *Main&gt; :t eval $ lam $ \x -&gt; add x x<br>    eval $ lam $ \x -&gt; add x x :: Int -&gt; Int<br>
<br>    *Main&gt; eval $ (lam $ \x -&gt; add x x) &lt;$&gt; int 1<br>    2<br><br>    *Main&gt; :t eval $ lam $ \x -&gt; lam $ \y -&gt; add x (int 1)<br>    eval $ lam $ \x -&gt; lam $ \y -&gt; add x (int 1) :: Int -&gt; a -&gt; Int<br>
<br>    *Main&gt; eval $ (lam $ \x -&gt; lam $ \y -&gt; add x (int 1)) &lt;$&gt; int 1 &lt;$&gt; 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 -&gt; Int -&gt; String}<br><br>instance Lin Str where<br>    int x = Str $ \_ _ -&gt; show x<br>    add x y = Str $ \uv lv -&gt; &quot;(&quot; ++ unStr x uv lv ++ &quot; + &quot; ++ unStr y uv lv ++ &quot;)&quot;<br>
<br>    llam f = Str $ \uv lv -&gt; let v = &quot;x&quot;++show lv in <br>                           &quot;\\&quot; ++ v ++ &quot; -&lt;&gt; &quot; ++ unStr (f $ Str (\_ _ -&gt; v)) uv (lv + 1)<br>    f &lt;^&gt; x = Str $ \uv lv -&gt; &quot;(&quot; ++ unStr f uv lv ++ &quot; ^ &quot; ++ unStr x uv lv ++ &quot;)&quot;<br>
<br>    lam f = Str $ \uv lv -&gt; let v = &quot;y&quot;++show uv in <br>                           &quot;\\&quot; ++ v ++ &quot; -&gt; &quot; ++ unStr (f $ Str (\_ _ -&gt; v)) (uv + 1) lv<br>    f &lt;$&gt; x = Str $ \uv lv -&gt; &quot;(&quot; ++ unStr f uv lv ++ &quot; &quot; ++ unStr x uv lv ++ &quot;)&quot;<br>
<br>showLin :: Str Z &#39;[] &#39;[] a -&gt; String<br>showLin x = unStr x 0 0<br><br>{-<br><br>An example:<br><br>    *Main&gt; showLin $ (llam $ \x -&gt; llam $ \y -&gt; add x y) &lt;^&gt; int 1<br>    &quot;(\\x0 -&lt;&gt; \\x1 -&lt;&gt; (x0 + x1) ^ 1)&quot;<br>
<br>-}</font><br></div>