## Adding Recursive Types

Up to this point, the language is neat-- at least there are some interesting types to play with-- but it is difficult to use for computation since there is no way to define recursive data types. Although recursive types are relatively straightforward, it is an interesting exercise to add them to a typed tagless-final interpreter; it also results in a language rich enough to write toy programs. This section is mostly an adaption of section 6.4 of Frank Pfenning's [notes](http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linfp.pdf).

The goal is to be able to define, and use, types such as
```
MyNat = One :+: MyNat

MyList a = One :+: (a :*: MyList a)
```
but even Haskell can't deal with such unrestricted recursion at the type level. Instead, I have to use an explicit type-level fixpoint, and include terms for manipulating such types:
```haskell
-- show Type-level fixpoint
newtype Mu a = Mu {unMu :: a (Mu a)}
-- show Terms for manipulating Mu types
class LinRec (repr :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where

    wrap :: repr vid tf i o (a (Mu a)) -> repr vid tf i o (Mu a)

    unwrap :: repr vid tf i o (Mu a) -> repr vid tf i o (a (Mu a))
```
I have introduced a new class, `LinRec`, in order to show off the extensibility of tagless-final encodings.

I can then represent my recursive type via `Mu`
```haskell
type MyNat = Mu ((:+:) One)

zero :: DefnRec False MyNat
zero = wrap (inl one)

succ :: DefnRec False (MyNat :-<>: MyNat)
succ = llam $ \x -> wrap (inr x)
```
The fact that GHC accepts the `MyNat` declaration is a bit of an anomaly since Haskell disallows partially applied type synonyms; so a similar trick can't be employed for `MyList a`.

In order to implement `MyList a`, I am forced to use a newtype to untie the knot:
```haskell
newtype MyListF a lst = MLF {unMLF :: One :+: (a :*: lst)}

type MyList a = Mu (MyListF a)
```
However, this is problematic since my language constructs, `wrap` and `unwrap`, only have one wrapper/unwrapper (`Mu`/`unMu`), but I now need to stick another wrapper/unwrapper inside the `repr` type, i.e. I need to use `MLF` to get from `One :+: (a :*: lst)` to `MyListF a lst` before I can use `Mu` to get `MyList a`. I could reflect `MLF` and `unMLF` into the object language:
```haskell
class LinRec (repr :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    wrap :: repr vid tf i o (a (Mu a)) -> repr vid tf i o (Mu a)
    unwrap :: repr vid tf i o (Mu a) -> repr vid tf i o (a (Mu a))
    
    wrapMLF :: repr vid tf i o (One :+: (a :*: lst)) -> repr vid tf i o (MyListF a lst)
    unwrapMLF :: repr vid tf i o (MyListF a lst) -> repr vid tf i o (One :+: (a :*: lst))
    
nil :: DefnRec False (MyList a)
nil = wrap $ wrapMLF $ inl one

cons :: DefnRec False (a :-<>: (MyList a :-<>: MyList a))
cons = llam (\x -> llam (\xs -> wrap $ wrapMLF $ inr $ x <*> xs))
```
But this is a poor solution as it requires adding an extra wrap/unwrap for (almost) every recursive type I wish to define; which means I have effectively lost my general recursive type. 
Though I can't get around the need for newtypes to declare my recursive types, I can get by with one wrap (unwrap) by generalizing the type to take the extra wrapper/unwrapper.
```haskell
wrap :: (b -> a (Mu a)) -> repr vid tf i o b -> repr vid tf i o (Mu a)
unwrap :: (a (Mu a) -> b) -> repr vid tf i o (Mu a) -> repr vid tf i o b

nil = wrap MLF $ inl one
```

Finally, I will add a term-level fixpoint construction so that I can write recursive functions to compute with recursive types; this is not really necessary as I could just use Haskell's own built-in term level fixpoints, but I will include it for completeness.
```haskell
class LinRec (repr :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    wrap :: (b -> a (Mu a)) -> repr vid tf i o b -> repr vid tf i o (Mu a)

    unwrap :: (a (Mu a) -> b) -> repr vid tf i o (Mu a) -> repr vid tf i o b

    fix :: ((forall vid h . repr vid False h h a) -> repr vid tf h h a) -> repr vid tf h h a 
```
Note that recursive functions cannot depend upon linear variables.

As with all the constructs in this interpreter, a concrete instance for evaluation of the terms is trivial:
```haskell
instance LinRec (R :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    wrap f = R . Mu . f . unR 
    unwrap f = R . f . unMu . unR 
    fix f = f (R $ unR $ fix f)
```

Also, as before, I will add a type synonym, `DefnRec`, to give the type checker some hints to allow better type inference. `DefnRec` will be identical to the previous `Defn` except that it will require an additional `LinRec` constraint.
```active haskell
-- /show
{-# LANGUAGE 
  DataKinds,
  FlexibleContexts,
  FlexibleInstances,
  FunctionalDependencies,
  KindSignatures,
  MultiParamTypeClasses,
  NoMonomorphismRestriction,
  OverlappingInstances,
  RankNTypes, 
  TypeFamilies,
  TypeOperators,
  UndecidableInstances
 #-}

import Prelude hiding(succ)

{---------------------------------------------------------------------

Type level machinery

---------------------------------------------------------------------}

--
-- Type level Or
--
type family Or (x::Bool) (y::Bool) :: Bool
type instance Or False False = False
type instance Or True False = True
type instance Or False True = True
type instance Or True True = True

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

--
-- Type level Nat equality
--
class EQ (x::Nat) (y::Nat) (b::Bool) | x y -> b
instance EQ x x True
instance (b ~ False) => EQ x y b

--
-- Type level machinery for consuming a variable in a list of variables.
--
class Consume (v::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) | v i -> o
class Consume1 (b::Bool) (v::Nat) (x::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) | b v x i -> o
instance (Consume v i o) => Consume v (Nothing ': i) (Nothing ': o)
instance (EQ v x b, Consume1 b v x i o) => Consume v (Just x ': i) o
instance Consume1 True v x i (Nothing ': i)
instance (Consume v i o) => Consume1 False v x i (Just x ': o)

--
-- Machinery needed to check/enforce conditions for additive conjunction/disjunction to correctly deal with Top.
--
class VarOk (tf :: Bool) (v :: Maybe Nat)
instance VarOk True (Just v)
instance VarOk True Nothing 
instance VarOk False Nothing

type family (:<:) (x::[Maybe Nat]) (y::[Maybe Nat]) :: Bool 
type instance '[] :<: '[] = True
type instance (Nothing ': xs) :<: (Nothing ': ys) = xs :<: ys
type instance (Nothing ': xs) :<: (Just y ': ys) = xs :<: ys
type instance (Just x ': xs) :<: (Nothing ': ys) =  False
type instance (Just x ': xs) :<: (Just x ': ys) =  xs :<: ys

type family Intersect (xs::[Maybe Nat]) (ys::[Maybe Nat]) :: [Maybe Nat]
type instance Intersect '[] '[] = '[]
type instance Intersect (Nothing ': xs) (Nothing ': ys) = (Nothing ': Intersect xs ys)
type instance Intersect (Nothing ': xs) (Just y ': ys) = (Nothing ': Intersect xs ys)
type instance Intersect (Just x ': xs) (Nothing ': ys) = (Nothing ': Intersect xs ys)
type instance Intersect (Just x ': xs) (Just x ': ys) = (Just x ': Intersect xs ys)

type family When (x::Bool) (y::Bool) :: Bool
type instance When True y = y

type family AdditiveAnd (tf0::Bool) (tf1::Bool) (h0::[Maybe Nat]) (h1::[Maybe Nat]) :: Bool
type instance AdditiveAnd False False h h = False 
type instance AdditiveAnd False True h0 h1 = When (h0 :<: h1) False
type instance AdditiveAnd True False h0 h1 = When (h1 :<: h0) False 
type instance AdditiveAnd True True h0 h1 = True 


{---------------------------------------------------------------------

Final tagless HOAS linear lambda calculus.

---------------------------------------------------------------------}

--
-- Linear types
--
newtype a :-<>: b = Lolli {unLolli :: a -> b}
data a :*: b = Tensor a b
data One = One
type a :&: b = (a, b)
type Top = ()
data a :+: b = Inl a | Inr b
data Zero 
newtype Bang a = Bang {unBang :: a}


type LinVar repr (vid::Nat) a = 
     forall (v::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) . (Consume vid i o) => 
     repr v False i o a

type RegVar repr a = 
     forall (v::Nat) (i::[Maybe Nat]) . repr v False i i a

class Lin (repr :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    llam :: (VarOk tf var) => 
            (LinVar repr vid a -> repr (S vid) tf (Just vid ': hi) (var ': ho) b) -> 
            repr vid tf hi ho (a :-<>: b)
    (<^>) :: repr vid tf0 hi h (a :-<>: b) -> repr vid tf1 h ho a -> 
             repr vid (Or tf0 tf1) hi ho b

    (!) :: repr vid tf h h a -> repr vid False h h (Bang a)
    letBang :: repr vid tf0 hi h (Bang a) -> 
               (RegVar repr a -> repr vid tf1 h ho b) -> 
               repr vid (Or tf0 tf1) hi ho b

    lam :: (RegVar repr a -> repr vid tf hi ho b) -> repr vid tf hi ho (a -> b)
    (<$>) :: repr vid tf0 hi ho (a -> b) -> repr vid tf1 ho ho a -> repr vid tf0 hi ho b

    one :: repr vid False h h One
    letOne :: repr vid tf0 hi h One -> repr vid tf1 h ho a -> 
              repr vid (Or tf0 tf1) hi ho a

    (<*>) :: repr vid tf0 hi h a -> repr vid tf1 h ho b -> 
             repr vid (Or tf0 tf1) hi ho (a :*: b)
    letStar :: (VarOk tf1 var0, VarOk tf1 var1) => 
               repr vid tf0 hi h (a :*: b) -> 
               (LinVar repr vid a -> 
                  LinVar repr (S vid) b -> 
                    repr (S (S vid)) 
                         tf1 
                         (Just vid ': Just (S vid) ': h) 
                         (var0 ': var1 ': ho) c
               ) -> 
               repr vid (Or tf0 tf1) hi ho c
                    
    top :: repr vid True h h Top

    (<&>) :: repr vid tf0 hi h0 a -> repr vid tf1 hi h1 b -> 
             repr vid (AdditiveAnd tf0 tf1 h0 h1) hi (Intersect h0 h1) (a :&: b)
    pi1 :: repr vid tf hi ho (a :&: b) -> repr vid tf hi ho a 
    pi2 :: repr vid tf hi ho (a :&: b) -> repr vid tf hi ho b 

    inl :: repr vid tf hi ho a -> repr vid tf hi ho (a :+: b)
    inr :: repr vid tf hi ho b -> repr vid tf hi ho (a :+: b)
    letPlus :: (VarOk tf1 var1, VarOk tf2 var2) => 
               repr vid tf0 hi h (a :+: b) ->
               (LinVar repr vid a -> repr (S vid) tf1 (Just vid ': h) (var1 ': ho1) c) ->
               (LinVar repr vid b -> repr (S vid) tf2 (Just vid ': h) (var2 ': ho2) c) ->
               repr vid (Or tf0 (AdditiveAnd tf1 tf2 ho1 ho2)) hi (Intersect ho1 ho2) c

    abort :: repr vid tf hi ho Zero -> repr vid True hi ho a


type Defn tf a = forall repr vid h . 
                 (Lin repr, Intersect h h ~ h, (h :<: h) ~ True) => 
                 repr vid tf h h a
defn :: Defn tf a -> Defn tf a
defn x = x


newtype R (vid::Nat) (tf::Bool) (hi::[Maybe Nat]) (ho::[Maybe Nat]) a = R {unR :: a}

instance Lin (R :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    llam f = R $ Lolli $ \x -> unR (f (R x))
    f <^> x = R $ unLolli (unR f) (unR x)

    (!) = R . Bang . unR
    letBang x f = R $ unR $ f' (unR x)
      where f' (Bang x) = f (R x)

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

    x <*> y = R $ Tensor (unR x) (unR y)
    letStar xy f = R $ unR $ f' (unR xy)
      where f' (Tensor x y) = f (R x) (R y)

    one = R One
    letOne x y = R $ unR $ (\One -> y) $ unR x

    top = R ()

    x <&> y = R $ (unR x, unR y)
    pi1 = R . fst . unR
    pi2 = R . snd . unR

    inl = R . Inl . unR
    inr = R . Inr . unR
    letPlus xy fInl fInr = case unR xy of
                             Inl x -> R $ unR $ fInl (R x)
                             Inr y -> R $ unR $ fInr (R y)

    abort x = R $ error "abort"


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


newtype Mu a = Mu {unMu :: a (Mu a)}

class LinRec (repr :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    wrap :: (b -> a (Mu a)) -> repr vid tf i o b -> repr vid tf i o (Mu a)
    unwrap :: (a (Mu a) -> b) -> repr vid tf i o (Mu a) -> repr vid tf i o b
    fix :: ((forall vid h . repr vid False h h a) -> repr vid tf h h a) -> repr vid tf h h a 

instance LinRec (R :: Nat -> Bool -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where
    wrap f = R . Mu . f . unR 
    unwrap f = R . f . unMu . unR 
    fix f = f (R $ unR $ fix f)

-- show Hints for the type checker.
type DefnRec tf a = 
    forall repr vid h . 
    (Lin repr, LinRec repr, Intersect h h ~ h, (h :<: h) ~ True) => 
    repr vid tf h h a
defnRec :: DefnRec tf a -> DefnRec tf a
defnRec x = x


-- show Nat examples
type MyNat = Mu ((:+:) One)

instance Show MyNat where
    show (Mu (Inl _)) = "z"
    show (Mu (Inr n)) = "s "++show n

zero :: DefnRec False MyNat
zero = wrap id (inl one)

succ :: DefnRec False (MyNat :-<>: MyNat)
succ = llam $ \x -> wrap id (inr x)

nat1 = succ <^> zero
nat2 = succ <^> nat1
nat3 = succ <^> nat2
nat4 = succ <^> nat3

plus :: DefnRec False (MyNat :-<>: (MyNat :-<>: MyNat))
plus = fix $ \p -> llam $ \x -> llam $ \y -> 
       letPlus (unwrap id x) 
               (\x -> letOne x y) 
               (\x -> succ <^> (p <^> x <^> y))

mult :: DefnRec False (MyNat :-<>: (MyNat -> MyNat))
mult = fix $ \m -> llam $ \x -> lam $ \y -> 
       letPlus (unwrap id x) 
               (\x -> letOne x zero) 
               (\x -> plus <^> (m <^> x <$> y) <^> y)


-- show List examples
newtype MyListF a lst = MLF {unMLF :: One :+: (a :*: lst)}
type MyList a = Mu (MyListF a)

instance Show a => Show (MyList a) where
    show (Mu (MLF (Inl _))) = "nil"
    show (Mu (MLF (Inr (Tensor x xs)))) = show x ++ ":" ++ show xs

nil :: DefnRec False (MyList a)
nil = wrap MLF (inl one)

cons :: DefnRec False (a :-<>: (MyList a :-<>: MyList a))
cons = llam $ \x -> llam $ \xs -> wrap MLF (inr (x <*> xs))

rev :: DefnRec False (MyList a :-<>: (MyList a :-<>: MyList a))
rev = fix $ \r -> llam $ \l -> llam $ \k -> 
      letPlus (unwrap unMLF l) 
              (\x -> letOne x k) 
              (\xs -> letStar xs (\x xs -> r <^> xs <^> (cons <^> x <^> k)))

-- Example using Haskell's recursion.
rev' :: DefnRec False (MyList a :-<>: (MyList a :-<>: MyList a))
rev' = llam $ \l -> llam $ \k -> 
       letPlus (unwrap unMLF l) 
              (\x -> letOne x k) 
              (\xs -> letStar xs (\x xs -> rev' <^> xs <^> (cons <^> x <^> k)))

l0 :: DefnRec False (MyList MyNat)
l0 = cons <^> zero <^> (cons <^> nat1 <^> (cons <^> nat2 <^> nil))


main = do
  putStrLn $ show $ eval $ mult <^> nat2 <$> (plus <^> nat3 <^> nat4)
  putStrLn $ show $ eval $ rev <^> l0 <^> nil
  putStrLn $ show $ eval $ rev' <^> (cons <^> nat3 <^> l0) <^> nil
  putStrLn "ok"
```