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.
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.