# Beta Reducer in Haskell

This is my first Haskell application, so any non-name-calling tips will be taken extremely well! It is just a beta reducer:

data Term = Var Int | Lam Term | App Term Term | Num Int | Add Term Term
deriving (Show)

subs :: Int -> Term -> Term -> Term
subs depth value (Lam body) = Lam (subs (depth + 1) value body)
subs depth value (App abstraction body) = App (subs depth value abstraction) (subs depth value body)
subs depth value (Var bind)
| bind == depth = inc depth value
| otherwise     = Var (bind + depth)

inc :: Int -> Term -> Term
inc depth (Var a) = Var (a + depth)
inc depth (App a b) = App (inc depth a) (inc depth b)
inc depth (Lam a) = Lam (inc depth a)

red :: Term -> Term
red (Var a) = Var a
red (Lam a) = Lam (red a)
red (App (Lam body) value) = red (subs 0 value body)
red (App a b) = (App (red a) (red b))

val = red (App (Lam (Lam (Lam (App (Var 2) (Var 1))))) (Lam (Var 77)))

main = print val


I want to know what I could improve on the style or how I could make the code cleaner. I have mostly problems with indentation, I never know where I can (and should) make a newline without confusing the parser.

Comment: making this was ridiculously easier than I thought. The type system actually helped me a lot.

## 2 Answers

This looks reasonable and idiomatic to me.

I don't recognise the reduction strategy, though. Specifically, the line

red (App a b) = App (red a) (red b)


looks like you're not reducing to a normal form, and you might be reducing, say, one redex in the function and one in the argument. This may be intentional on your part, but if it isn't, maybe take a look here for a brief overview of reduction strategies, or here for more detail.

I haven't looked at de Bruijn indices in a while, so I wouldn't be able to promise that your implementation is correct. Nothing untoward comes to mind, though.

About the style–and this is really nitpicking–in the subs definition you might use simply a instead of the cumbersome abstraction. And I'd have indented the | one more space. (See? Nitpicking.)

• Oh, of course. It does reach normal form if I apply red to App (red a) (red b) and to (subs 0 val body), right? Great advices, though, thanks. Replaced the names. Why the extra space there? – MaiaVictor Mar 15 '14 at 22:59
• Well, what about App (Var 0) (Var 0)? This is a normal form, but I don't think your program terminates on it. Try take a look at p. 425 in the second link. (It's an excerpt, it's not actually 425 pages.) – Søren Debois Mar 15 '14 at 23:05
• I guess I got it now... is it correct? I'm still reducing the body inside a lambda abstraction, though, the author doesn't. – MaiaVictor Mar 15 '14 at 23:27
• I can't find the difference between this and the original? – Søren Debois Mar 16 '14 at 7:47

There is a problem with your inc function: it should only modify the variables which are free in the term you are traversing. Here you are going to have a bad time if you are pushing a closed term under a lambda. Let's see an example of such a situation. We start by introducing normalization as the reflexive, transitive closure of red:

closure :: Eq a => (a -> a) -> a -> a
closure f a =
let fa = f a
in if fa == a then fa
else closure f fa

norm :: Term -> Term
norm = closure red


Now, let's call tid the identity in your language (i.e. Lam (Var 0)). The term App (Lam tid) tid should reduce to tid but when running

main = print . norm \$ App (Lam tid) tid


we get: Lam (Var 1)

The traditional solution to checking whether a variable is bound or free in this kind of context is to introduce an extra parameter protected which counts the number of Lam abstraction we go under.

inc :: Int -> Term -> Term
inc depth term = go 0 depth term
where
go :: Int -> Int -> Term -> Term
go protected depth (Var a)
| a < protected = Var a
| otherwise     = Var (a + depth)
go protected depth (App a b) = App (go protected depth a) (go protected depth b)
go protected depth (Lam a)   = Lam (go (protected + 1) depth a)


Now, we are one step closer to a correct solution. There is still a bit of weakening in the Var case of the subs function. Once this is fixed too (same pattern: add an extra parameter to remember which variables are protected), you'll get a correct implementation of the normalizer.