Is it possible to showcase the different strategies of evaluation by modifying this simple reducer?

Question

I am the kind that prefers learning by looking at code instead of reading long explanations. This might be one of the reasons I dislike long academic papers. Code is unambiguous, compact, noise-free and if you don't get something you can just play with it - no need to ask the author.

This is a complete definition of the Lambda Calculus:

-- A Lambda Calculus term is a function, an application or a variable.
data Term = Lam Term | App Term Term | Var Int deriving (Show,Eq,Ord)

-- Reduces lambda term to its normal form.
reduce :: Term -> Term
reduce (Var index)      = Var index
reduce (Lam body)       = Lam (reduce body)
reduce (App left right) = case reduce left of
    Lam body  -> reduce (substitute (reduce right) body)
    otherwise -> App (reduce left) (reduce right)

-- Replaces bound variables of `target` by `term` and adjusts bruijn indices.
-- Don't mind those variables, they just keep track of the bruijn indices.
substitute :: Term -> Term -> Term
substitute term target = go term True 0 (-1) target where
    go t s d w (App a b)             = App (go t s d w a) (go t s d w b)
    go t s d w (Lam a)               = Lam (go t s (d+1) w a) 
    go t s d w (Var a) | s && a == d = go (Var 0) False (-1) d t 
    go t s d w (Var a) | otherwise   = Var (a + (if a > d then w else 0))

-- If the evaluator is correct, this test should print the church number #4.
main = do
    let two = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0)))))
    print $ reduce (App two two)

In my opinion, the "reduce" function above says much more about the Lambda Calculus than pages of explanations and I wish I could just look at it when I started learning. You can also see it implements a very strict evaluation strategy that goes even inside abstractions. On that spirit, how could that code be modified in order to illustrate the many different evaluation strategies that the LC can have (call-by-name, lazy evaluation, call-by-value, call-by-sharing, partial evaluation and so on)?

Answer 1

Call-by-name requires only a few changes:

1. Not evaluating the body of a lambda abstraction: reduce (Lam body) = (Lam body).

2. Not evaluating the argument of the application. Instead, we should substitute it as is:

   reduce (App left right) = case reduce left of
       Lam body -> reduce (substitute right body)
   

Call-by-need(aka lazy evaluation) seems harder(or maybe impossible) to implement in a fully declarative manner because we need to memoize values of expressions. I do not see a way to achieve it with minor changes.

Call by-sharing is not applicable to simple lambda calculus because we do not have objects and assignments here.

We could also use full beta reduction, but we need to chose some deterministic order of evaluation(we cannot pick an "arbitrary" redex and reduce it using the code we have now). This choice will yield some evaluation strategy(possible one of the described above).

Answer 2

The topic is quite broad. I'll just write about a few ideas.

The proposed reduce performs parallel rewriting. That is, it maps App t1 t2 to App t1' t2' (provided t1' is not an abstraction). Some strategies such as CBV and CBN are more sequential, in that they only have a single redex.

To describe them, I would modify reduce so that it returns whether a reduction was actually done, or if instead the term was a normal form. This can be done by returning a Maybe Term, where Nothing means normal form.

In that way, CBN would be

reduce :: Term -> Maybe Term
reduce (Var index)            = Nothing   -- Vars are NF
reduce (Lam body)             = Nothing   -- no reduction under Lam
reduce (App (Lam body) right) = Just $ substitute right body
reduce (App left right) = 
      (flip App right <$> reduce left) <|>  -- try reducing left
      (App left       <$> reduce right)     -- o.w., try reducing right

while CBV would be

reduce :: Term -> Maybe Term
reduce (Var index)            = Nothing
reduce (Lam body)             = Nothing   -- no reduction under Lam
reduce (App (Lam body) right) 
     | reduce right == Nothing            -- right must be a NF
     = Just $ substitute right body
reduce (App left right) = 
      (flip App right <$> reduce left) <|>
      (App left       <$> reduce right)

Lazy evaluation (with sharing) can not be expressed using terms, if I remember correctly. It requires graphs to denote that a subterm is being shared.