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)"

-}