{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
-- | Example implementation of untyped \(\lambda\)-calculus with the foil.
module Control.Monad.Foil.Example where

import           Control.DeepSeq
import           Control.Monad.Foil
import           Control.Monad.Foil.Relative

-- $setup
-- >>> import Control.Monad.Foil

-- | Untyped \(\lambda\)-terms in scope @n@.
data Expr n where
  -- | Variables are names in scope @n@: \(x\)
  VarE :: Name n -> Expr n
  -- | Application of one term to another: \((t_1, t_2)\)
  AppE :: Expr n -> Expr n -> Expr n
  -- | \(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\)
  LamE :: NameBinder n l -> Expr l -> Expr n

-- | Use 'ppExpr' to show \(\lambda\)-terms.
instance Show (Expr n) where
  show :: Expr n -> String
show = Expr n -> String
forall (n :: S). Expr n -> String
ppExpr

instance NFData (Expr l) where
  rnf :: Expr l -> ()
rnf (LamE NameBinder l l
binder Expr l
body) = NameBinder l l -> ()
forall a. NFData a => a -> ()
rnf NameBinder l l
binder () -> () -> ()
forall a b. a -> b -> b
`seq` Expr l -> ()
forall a. NFData a => a -> ()
rnf Expr l
body
  rnf (AppE Expr l
fun Expr l
arg)     = Expr l -> ()
forall a. NFData a => a -> ()
rnf Expr l
fun () -> () -> ()
forall a b. a -> b -> b
`seq` Expr l -> ()
forall a. NFData a => a -> ()
rnf Expr l
arg
  rnf (VarE Name l
name)        = Name l -> ()
forall a. NFData a => a -> ()
rnf Name l
name

-- | This instance serves as a proof
-- that sinking of 'Expr' is safe.
instance Sinkable Expr where
  sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
sinkabilityProof Name n -> Name l
rename (VarE Name n
v) = Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (Name n -> Name l
rename Name n
v)
  sinkabilityProof Name n -> Name l
rename (AppE Expr n
f Expr n
e) = Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
AppE ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
f) ((Name n -> Name l) -> Expr n -> Expr l
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename Expr n
e)
  sinkabilityProof Name n -> Name l
rename (LamE NameBinder n l
binder Expr l
body) = (Name n -> Name l)
-> NameBinder n l
-> (forall {l' :: S}.
    (Name l -> Name l') -> NameBinder l l' -> Expr l)
-> Expr l
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
extendRenaming Name n -> Name l
rename NameBinder n l
binder ((forall {l' :: S}.
  (Name l -> Name l') -> NameBinder l l' -> Expr l)
 -> Expr l)
-> (forall {l' :: S}.
    (Name l -> Name l') -> NameBinder l l' -> Expr l)
-> Expr l
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' NameBinder l l'
binder' ->
    NameBinder l l' -> Expr l' -> Expr l
forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
LamE NameBinder l l'
binder' ((Name l -> Name l') -> Expr l -> Expr l'
forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name l -> Name l'
rename' Expr l
body)

instance InjectName Expr where
  injectName :: forall (n :: S). Name n -> Expr n
injectName = Name n -> Expr n
forall (n :: S). Name n -> Expr n
VarE

-- | 'Expr' is a monad relative to 'Name'.
instance RelMonad Name Expr where
  rreturn :: forall (n :: S). Name n -> Expr n
rreturn = Name a -> Expr a
forall (n :: S). Name n -> Expr n
VarE
  rbind :: forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
rbind Scope b
scope Expr a
term Name a -> Expr b
subst =
    case Expr a
term of
      VarE Name a
name -> Name a -> Expr b
subst Name a
name
      AppE Expr a
x Expr a
y  -> Expr b -> Expr b -> Expr b
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
x Name a -> Expr b
subst) (Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope b
scope Expr a
y Name a -> Expr b
subst)
      LamE NameBinder a l
binder Expr l
body ->
        Scope b
-> Name l
-> (forall {o' :: S}. DExt b o' => NameBinder b o' -> Expr b)
-> Expr b
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
withRefreshed Scope b
scope (NameBinder a l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder a l
binder) ((forall {o' :: S}. DExt b o' => NameBinder b o' -> Expr b)
 -> Expr b)
-> (forall {o' :: S}. DExt b o' => NameBinder b o' -> Expr b)
-> Expr b
forall a b. (a -> b) -> a -> b
$ \NameBinder b o'
binder' ->
          let scope' :: Scope o'
scope' = NameBinder b o' -> Scope b -> Scope o'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder b o'
binder' Scope b
scope
              subst' :: Name l -> Expr o'
subst' Name l
name = case NameBinder a l -> Name l -> Maybe (Name a)
forall (n :: S) (l :: S).
NameBinder n l -> Name l -> Maybe (Name n)
unsinkName NameBinder a l
binder Name l
name of
                          Maybe (Name a)
Nothing -> Name o' -> Expr o'
forall (n :: S). Name n -> Expr n
forall (f :: S -> *) (m :: S -> *) (a :: S).
RelMonad f m =>
f a -> m a
rreturn (NameBinder b o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder b o'
binder')
                          Just Name a
n  -> Expr b -> Expr o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name a -> Expr b
subst Name a
n)
           in NameBinder b o' -> Expr o' -> Expr b
forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
LamE NameBinder b o'
binder' (Scope o' -> Expr l -> (Name l -> Expr o') -> Expr o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> Expr a -> (Name a -> Expr b) -> Expr b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
rbind Scope o'
scope' Expr l
body Name l -> Expr o'
subst')

-- | Substitution for untyped \(\lambda\)-terms.
-- The foil helps implement this function without forgetting scope extensions and renaming.
substitute :: Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute :: forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst = \case
    VarE Name i
name -> Substitution Expr i o -> Name i -> Expr o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
lookupSubst Substitution Expr i o
subst Name i
name
    AppE Expr i
f Expr i
x -> Expr o -> Expr o -> Expr o
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
f) (Scope o -> Substitution Expr i o -> Expr i -> Expr o
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o
scope Substitution Expr i o
subst Expr i
x)
    LamE NameBinder i l
binder Expr l
body -> Scope o
-> Name l
-> (forall {o' :: S}. DExt o o' => NameBinder o o' -> Expr o)
-> Expr o
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
withRefreshed Scope o
scope (NameBinder i l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder i l
binder) ((forall {o' :: S}. DExt o o' => NameBinder o o' -> Expr o)
 -> Expr o)
-> (forall {o' :: S}. DExt o o' => NameBinder o o' -> Expr o)
-> Expr o
forall a b. (a -> b) -> a -> b
$ \NameBinder o o'
binder' ->
      let subst' :: Substitution Expr l o'
subst' = Substitution Expr i o'
-> NameBinder i l -> Name o' -> Substitution Expr l o'
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
addRename (Substitution Expr i o -> Substitution Expr i o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink Substitution Expr i o
subst) NameBinder i l
binder (NameBinder o o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder o o'
binder')
          scope' :: Scope o'
scope' = NameBinder o o' -> Scope o -> Scope o'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder o o'
binder' Scope o
scope
          body' :: Expr o'
body' = Scope o' -> Substitution Expr l o' -> Expr l -> Expr o'
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope o'
scope' Substitution Expr l o'
subst' Expr l
body
       in NameBinder o o' -> Expr o' -> Expr o
forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
LamE NameBinder o o'
binder' Expr o'
body'

-- | Compute weak head normal form (WHNF) of a \(\lambda\)-term.
--
-- >>> whnf emptyScope (AppE (churchN 2) (churchN 2))
-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))
whnf :: Distinct n => Scope n -> Expr n -> Expr n
whnf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope = \case
  AppE Expr n
fun Expr n
arg ->
    case Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
fun of
      LamE NameBinder n l
binder Expr l
body ->
        let subst :: Substitution Expr l n
subst = Substitution Expr n n
-> NameBinder n l -> Expr n -> Substitution Expr l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubst Substitution Expr n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst NameBinder n l
binder Expr n
arg
        in Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope (Scope n -> Substitution Expr l n -> Expr l -> Expr n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope n
scope Substitution Expr l n
subst Expr l
body)
      Expr n
fun' -> Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
AppE Expr n
fun' Expr n
arg
  Expr n
t -> Expr n
t

-- | Compute weak head normal form (WHNF) of a __closed__ \(\lambda\)-term.
--
-- >>> whnf' (AppE (churchN 2) (churchN 2))
-- λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))
whnf' :: Expr VoidS -> Expr VoidS
whnf' :: Expr 'VoidS -> Expr 'VoidS
whnf' = Scope 'VoidS -> Expr 'VoidS -> Expr 'VoidS
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope 'VoidS
emptyScope

-- | Compute normal form (NF) of a \(\lambda\)-term.
--
-- >>> nf emptyScope (AppE (churchN 2) (churchN 2))
-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))
nf :: Distinct n => Scope n -> Expr n -> Expr n
nf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope n
scope Expr n
expr = case Expr n
expr of
  LamE NameBinder n l
binder Expr l
body ->
    -- Instead of using 'assertDistinct',
    -- another option is to add 'Distinct l' constraint
    -- to the definition of 'LamE'.
    case NameBinder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinder n l
binder of
      DistinctEvidence l
Distinct ->
        let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder n l
binder Scope n
scope
        in NameBinder n l -> Expr l -> Expr n
forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
LamE NameBinder n l
binder (Scope l -> Expr l -> Expr l
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope l
scope' Expr l
body)
  AppE Expr n
fun Expr n
arg ->
    case Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf Scope n
scope Expr n
fun of
      LamE NameBinder n l
binder Expr l
body ->
        let subst :: Substitution Expr l n
subst = Substitution Expr n n
-> NameBinder n l -> Expr n -> Substitution Expr l n
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubst Substitution Expr n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst NameBinder n l
binder Expr n
arg
        in Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope n
scope (Scope n -> Substitution Expr l n -> Expr l -> Expr n
forall (o :: S) (i :: S).
Distinct o =>
Scope o -> Substitution Expr i o -> Expr i -> Expr o
substitute Scope n
scope Substitution Expr l n
subst Expr l
body)
      Expr n
fun' -> Expr n -> Expr n -> Expr n
forall (n :: S). Expr n -> Expr n -> Expr n
AppE (Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope n
scope Expr n
fun') (Scope n -> Expr n -> Expr n
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope n
scope Expr n
arg)
  Expr n
t -> Expr n
t

-- | Compute normal form (NF) of a __closed__ \(\lambda\)-term.
--
-- >>> nf' (AppE (churchN 2) (churchN 2))
-- λx1. λx2. (x1 (x1 (x1 (x1 x2))))
nf' :: Expr VoidS -> Expr VoidS
nf' :: Expr 'VoidS -> Expr 'VoidS
nf' = Scope 'VoidS -> Expr 'VoidS -> Expr 'VoidS
forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf Scope 'VoidS
emptyScope

-- | Pretty print a name.
ppName :: Name n -> String
ppName :: forall (n :: S). Name n -> String
ppName Name n
name = String
"x" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Name n -> Int
forall (l :: S). Name l -> Int
nameId Name n
name)

-- | Pretty-print a \(\lambda\)-term.
--
-- >>> ppExpr (churchN 3)
-- "\955x0. \955x1. (x0 (x0 (x0 x1)))"
ppExpr :: Expr n -> String
ppExpr :: forall (n :: S). Expr n -> String
ppExpr = \case
  VarE Name n
name -> Name n -> String
forall (n :: S). Name n -> String
ppName Name n
name
  AppE Expr n
x Expr n
y -> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
x String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr n -> String
forall (n :: S). Expr n -> String
ppExpr Expr n
y String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  LamE NameBinder n l
binder Expr l
body -> String
"λ" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Name l -> String
forall (n :: S). Name n -> String
ppName (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
binder) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
". " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Expr l -> String
forall (n :: S). Expr n -> String
ppExpr Expr l
body

-- | A helper for constructing \(\lambda\)-abstractions.
lam :: Distinct n => Scope n -> (forall l. DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n
lam :: forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope n
scope forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l
mkBody = Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> Expr n)
-> Expr n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> Expr n) -> Expr n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> Expr n)
-> Expr n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
x ->
  let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder n l
x Scope n
scope
   in NameBinder n l -> Expr l -> Expr n
forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
LamE NameBinder n l
x (Scope l -> NameBinder n l -> Expr l
forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l
mkBody Scope l
scope' NameBinder n l
x)

-- | Church-encoding of a natural number \(n\).
--
-- >>> churchN 0
-- λx0. λx1. x1
--
-- >>> churchN 3
-- λx0. λx1. (x0 (x0 (x0 x1)))
churchN :: Int -> Expr VoidS
churchN :: Int -> Expr 'VoidS
churchN Int
n =
  Scope 'VoidS
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope 'VoidS
emptyScope ((forall {l :: S}.
  DExt 'VoidS l =>
  Scope l -> NameBinder 'VoidS l -> Expr l)
 -> Expr 'VoidS)
-> (forall {l :: S}.
    DExt 'VoidS l =>
    Scope l -> NameBinder 'VoidS l -> Expr l)
-> Expr 'VoidS
forall a b. (a -> b) -> a -> b
$ \Scope l
sx NameBinder 'VoidS l
nx ->
    Scope l
-> (forall {l :: S}.
    DExt l l =>
    Scope l -> NameBinder l l -> Expr l)
-> Expr l
forall (n :: S).
Distinct n =>
Scope n
-> (forall (l :: S).
    DExt n l =>
    Scope l -> NameBinder n l -> Expr l)
-> Expr n
lam Scope l
sx ((forall {l :: S}. DExt l l => Scope l -> NameBinder l l -> Expr l)
 -> Expr l)
-> (forall {l :: S}.
    DExt l l =>
    Scope l -> NameBinder l l -> Expr l)
-> Expr l
forall a b. (a -> b) -> a -> b
$ \Scope l
_sxy NameBinder l l
ny ->
      let x :: Expr l
x = Expr l -> Expr l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (NameBinder 'VoidS l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder 'VoidS l
nx))
          y :: Expr l
y = Name l -> Expr l
forall (n :: S). Name n -> Expr n
VarE (NameBinder l l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder l l
ny)
       in (Expr l -> Expr l) -> Expr l -> [Expr l]
forall a. (a -> a) -> a -> [a]
iterate (Expr l -> Expr l -> Expr l
forall (n :: S). Expr n -> Expr n -> Expr n
AppE Expr l
x) Expr l
y [Expr l] -> Int -> Expr l
forall a. HasCallStack => [a] -> Int -> a
!! Int
n