GenericEvaluators.hs

import Control.Monad.State



-- Introduction forms, including variables. We parameterize by the type of a
-- scope argument `s` and scope body `b`, as well as the type of auxiliary
-- terms `a`

data Intro s b a
  = Var String
  | Pair a a
  | Lam (s -> b)

-- Intro can map over its auxiliary term position

mapAuxIntro :: (a -> a') -> Intro s b a -> Intro s b a'
mapAuxIntro _ (Var x) = Var x
mapAuxIntro f (Pair x y) = Pair (f x) (f y)
mapAuxIntro _ (Lam g) = Lam g

-- Elim forms. We parameterize by the type of a scope argument `s`, auxiliary
-- terms `a`, and main terms / redex-position terms `b`.

data Elim s m a
  = Fst m | Snd m
  | App m a

-- Elim can also map over its aux position, as well as its main term position

mapAuxElim :: (a -> a') -> Elim s m a -> Elim s m a'
mapAuxElim _ (Fst p) = Fst p
mapAuxElim _ (Snd p) = Snd p
mapAuxElim f (App g x) = App g (f x)

mapMainElim :: (m -> m') -> Elim s m a -> Elim s m' a
mapMainElim f (Fst p) = Fst (f p)
mapMainElim f (Snd p) = Snd (f p)
mapMainElim f (App g x) = App (f g) x

-- The core concept of evaluation is a local reduction, turning a redux,
-- which consits of an Elim after an Intro, into a simpler term, ie, beta.

reduce :: Elim a (Intro a a a) a -> a
reduce (Fst (Pair x y)) = x
reduce (Snd (Pair x y)) = y
reduce (App (Lam f) x)  = f x

-- A term is just either an Intro or an Elim, with the various positions
-- able to be filled recursively by terms.

data Term = I (Intro Term Term Term) | E (Elim Term Term Term)

instance Show Term where
  show t = fst (runState (go t) 0)
    where
      go :: Term -> State Int String
      go (I (Var x)) = return x
      go (I (Pair x y)) = do x' <- go x
                             y' <- go y
                             return $ "<" ++ x' ++ "," ++ y' ++ ">"
      go (I (Lam f)) = do i <- get
                          put (i+1)
                          let v = "x" ++ show i
                          b <- go (f (I (Var v)))
                          return $ "\\" ++ v ++ " -> " ++ b
      go (E (Fst p)) = do p' <- go p
                          return $ "fst(" ++ p' ++ ")"
      go (E (Snd p)) = do p' <- go p
                          return $ "snd(" ++ p' ++ ")"
      go (E (App f x)) = do f' <- go f
                            x' <- go x
                            return $ "(" ++ f' ++ " " ++ x' ++ ")"



-- Evaluating into WHNF in the usual way. When we evaluate an Intro, we're
-- done, but when we evaluate an Elim, we recursively evaluate its main
-- term to produce a redex, then reduce it, then evaluate the result.

evalWHNF :: Term -> Intro Term Term Term
evalWHNF (I i) = i
evalWHNF (E e) = evalWHNF (reduce (mapMainElim evalWHNF e))

-- Evaluating to HNF in the usual way. Same as WHNF, except when we evaluate
-- an Intro, we also recursively evaluate its aux terms rather than leaving
-- them un-evaluated.

evalHNF :: Term -> Intro Term Term Term
evalHNF (I i) = mapAuxIntro (I . evalHNF) i
evalHNF (E e) = evalHNF (reduce (mapMainElim evalHNF e))

-- A stack-based WHNF evaluator. These normally have stack frames that consist
-- of the local shape of an Elim, eg InFst, InSnd, InAppFun x, which, when
-- put in a list constitutes a Zipper (or in McBride's variant, a Tube) into
-- a position for recursive computation. When we return to one with an Intro,
-- with have an Elim meeting an Intro, i.e. a redex, and computation occurs.
-- Because we have distinct Intro and Elim types, a stack frame can instead
-- be a function that turns an Intro into an Elim-after-an-Intro, i.e. exactly
-- the sort of thing that the `reduce` function needs.

data StackFrame
  = StackFrame (Intro Term Term Term -> Elim Term (Intro Term Term Term) Term)

-- Stacks are either computing (:>:) or returning (:<:)

data Stack = [StackFrame] :>: Term
           | [StackFrame] :<: Term

-- To evaluate with a stack evaluator, we just step the stack repeatedly.
-- When we ask to compute on an Intro, we're done, since we're computing WHNF,
-- and when we're asked to compute on an Elim, we make a new frame and
-- step on its main term. When we return an Intro, we form the redex and
-- reduce, and compute on the result.

stackWHNF :: Term -> Intro Term Term Term
stackWHNF tm = let [] :<: I i = go ([] :>: tm)
               in i
  where
    go :: Stack -> Stack
    go (fms :>: I i) = go (fms :<: I i)
    go (fms :>: E (Fst p)) = go ((StackFrame Fst:fms) :>: p)
    go (fms :>: E (Snd p)) = go ((StackFrame Snd:fms) :>: p)
    go (fms :>: E (App f x)) = go ((StackFrame (\g -> App g x):fms) :>: f)
    go ((StackFrame f:fms) :<: I i) = go (fms :>: reduce (f i))
    go s = s
    
-- Just to prove it works:

main :: IO ()
main = do print t
          print (I (evalWHNF t))
          print (I (evalHNF t))
          print (I (stackWHNF t))
          
          putStrLn ""
          
          print t'
          print (I (evalWHNF t'))
          print (I (evalHNF t'))
          print (I (stackWHNF t'))
          
          putStrLn ""
          
          print t''
          print (I (evalWHNF t''))
          print (I (evalHNF t''))
          print (I (stackWHNF t''))
  where
    t = E (Fst (E (Fst (I (Pair (I (Pair (I (Var "A")) (I (Var "B")))) (I (Var "C")))))))
    t' = E (Fst (I (Pair (E (Fst (I (Pair (I (Var "A")) (I (Var "B")))))) (I (Var "C")))))
    t'' = I (Pair (E (Fst (I (Pair (I (Var "A")) (I (Var "B")))))) (I (Var "C")))