Open evaluation with explicit thunking and environment trimming

ReasonableLC.hs

{-# language Strict, LambdaCase #-}

module ReasonableLC where

type Ix  = Int
type Lvl = Int

-- environment trimming, drops some entries
data Trim = Empty | Keep Trim | Drop Trim

data Tm   = Var Ix | Lam Tm | App Tm Tm | Trim Trim Tm | Thunk Tm
data Env  = Nil | Def Env Val
data Val  = VVar Lvl | VApp Val Val | VLam Env Tm | VThunk ~Val

{-
Trimming and thunking should be placed "properly".
- Each sequence of Lam-s should be wrapped in a Trim
- Each thunk should be wrapped in a Trim
- The iterated function applications which are in "unforced" position
  (i.e. in the argument side of a function application) should be thunked.
- If we do this, the thunk creation and the amount of space leaking is *roughly*
  on par with GHC -O0. 
-}

lookupVar :: Env -> Ix -> Val
lookupVar (Def _ v) 0 = v
lookupVar (Def e _) x = lookupVar e (x - 1)
lookupVar _         _ = undefined

trim :: Trim -> Env -> Env
trim Empty     e         = e
trim (Drop tr) (Def e _) = trim tr e
trim (Keep tr) (Def e v) = Def (trim tr e) v
trim _         _         = undefined

app :: Val -> Val -> Val
app t u = case t of
  VThunk t -> app t u
  VLam e t -> eval (Def e u) t
  t        -> VApp t u

eval :: Env -> Tm -> Val
eval e = \case
  Var x     -> lookupVar e x
  App t u   -> app (eval e t) (eval e u)
  Trim tr t -> eval (trim tr e) t
  Lam t     -> VLam e t
  Thunk t   -> VThunk (eval e t)