Haskell save recursive steps into a list

Question

I'm working on Haskell lambda calculus interpreter. I have a method which reduces expression to it's normal form.

type Var = String

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
  deriving Show

normal :: Term -> Term
normal (Variable index)      = Variable index
normal (Lambda var body)       = Lambda var (normal body)
normal (Apply left right) = case normal left of
    Lambda var body  -> normal (substitute var (normal right) body)
    otherwise -> Apply (normal left) (normal right)

How can I save the steps taken into a collection?

My normal function outputs this: \a. \b. a (a (a (a b))) and my goal would be to get all the steps as:

(\f. \x. f (f x)) (\f. \x. f (f x)),
\a. (\f. \x. f (f x)) ((\f. \x. f (f x)) a),
\a. \b. (\f. \x. f (f x)) a ((\f. \x. f (f x)) a b),
\a. \b. (\b. a (a b)) ((\f. \x. f (f x)) a b),
\a. \b. a (a ((\f. \x. f (f x)) a b)),
\a. \b. a (a ((\b. a (a b)) b)),
\a. \b. a (a (a (a b)))]

I've tried encapsulating the normal method into lists as follows:

normal :: Term -> [Term]
normal (Variable index)      = Variable index
normal (Lambda var body)       = term: [Lambda var (normal body)]
normal (Apply left right) = case normal left of
    Lambda var body  -> normal (substitute var (normal right) body)
    otherwise -> Apply (normal left) (normal right)

But that doesn't seem to be the right approach.

Answer 1

I think you're putting the cart before the horse. normal repeatedly reduces a term until it cannot be reduced any more. Where, then, is the function that actually reduces a term once?

reduce :: Term -> Maybe Term -- returns Nothing if no reduction
reduce (Variable _) = Nothing -- variables don't reduce
reduce (Lambda v b) = Lambda v <$> reduce b -- an abstraction reduces as its body does
reduce (Apply (Lambda v b) x) = Just $ substitute v x b -- actual meaning of reduction
reduce (Apply f x) = flip Apply x <$> reduce f <|> Apply f <$> reduce x -- try to reduce f, else try x

Then

normal :: Term -> [Term]
normal x = x : maybe [] normal (reduce x)

Or, to be slightly more accurate

import Data.List.NonEmpty as NE
normal :: Term -> NonEmpty Term
normal = NE.unfoldr $ (,) <*> reduce

---

Note that this definition of reduce also corrects a bug in your original normal. There are terms which have normal forms that your normal fails to evaluate. Consider the term

(\x y. y) ((\x. x x) (\x. x x)) -- (const id) omega

This normalizes to \y. y. Depending on how substitute is implemented, your normal might succeed or fail to normalize this term. If it succeeds, it will have been saved by laziness. A hypothetical "stepping" version of your normal, which normalizes arguments before substitution, would definitely fail to normalize this.

Refraining from reducing the argument before substitution guarantees you will find the normal form of any term, if a normal form exists. You can restore the eager behavior with

eagerReduce t@(Apply f@(Lambda v b) x) = Apply f <$> eagerReduce x <|> Just (substitute v x b)
-- other equations...
eagerNormal = NE.unfoldr $ (,) <*> eagerReduce

As promised, eagerNormal produces an infinite list on my example term and never finds the normal form.

Answer 2

You're on the right track, but there's just a lot more you need to do. Remember, if you change the type of your function from Term -> Term to Term -> [Term], then you need to make sure that for any input Term, the function produces an output [Term]. However, in your new implementation of normal, you only made the change for one case (and in doing so, you made up some new value called term — not sure why you did that).

So, let's think through the whole problem. What is the list of Term that should be produced by normal when the input is Variable index? Well, there's no work to do, so it should probably be a singleton list:

normal' (Variable index) = [Variable index]

How about for Lambda var body? You wrote term: [Lambda var (normal' body)], but this doesn't make any sense. Remember that normal' body is now producing a list, but Lambda can't take a list of terms as its body argument. And what is this term value you're trying to cons onto your singleton list?

Calling normal' body is a great idea. This produces a list of Terms, which represent partial normalizations of the body. But, we want to produce partial normalizations of the lambda, not just the body. So, we need to modify each element in the list, converting it from a body to a lamdba:

normal' (Lambda var body) = Lambda var <$> normal' body

Hooray! (Note that since we're not doing any actual normalization in this step, we don't need to increase the length of the list.)

(For the sake of coding convenience, for the final case, we will construct the list of partial terms in reverse order. We can always reverse it later.)

The last case is the hardest, but it follows the same principles. We begin by recognizing that the recursive calls normal' left and normal' right will return lists of results rather than simply the final term:

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right

One question this raises is: Which evaluation steps do we take first? Let's choose to evaluate left first. This means that all of the evaluation steps for left must be paired with the original right, and all of the evaluation steps for right must be paired with the most evaluated left.

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right
      lefts'  = flip Apply right <$> lefts
      rights' = Apply (head lefts) <$> init rights
      evalSoFar = rights' + lefts'

Note the use of init rights at the end — since the last element of rights should be equal to right and we already have a value with the head of lefts and the last element of rights in lefts', we omit the last element of of rights when building rights'.

From here, all we need to do is actually perform our substitution (assuming that head lefts is indeed a Lambda expression) and concatenate our evalSoFar list to what it produces:

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right
      lefts'  = flip Apply right <$> lefts
      rights' = Apply (head lefts) <$> init rights
      evalSoFar = rights' ++ lefts'
  in case (lefts, rights) of
    (Lambda var body : _, right' : _) -> normal' (substitute var right' body) ++ evalSoFar
    _ -> evalSoFar

Remember that this produces the list backwards, so we can define normal as follows:

normal :: Term -> [Term]
normal = reverse . normal'

---

It's hard for me to test this exactly considering you didn't provide a definition of substitute, but I'm pretty sure it should do what you want.

That said, I will note that the resulting evaluation steps I get from evaluating your sample term are not the same as those given in the question. Specifically, your second evaluation step, going from

\a. (\f. \x. f (f x)) ((\f. \x. f (f x)) a),
\a. \b. (\f. \x. f (f x)) a ((\f. \x. f (f x)) a b),

seems wrong based on your implementation. Note that here you're performing a substitution before fully evaluating the argument. If you run the code in this answer, you'll see that the result you get does not perform this step but rather fully evaluates the function argument (that is, ((\f. \x. f (f x)) a)) before substituting.