Beta Reducer in Haskell

Question

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.

Answer 1

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

Answer 2

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.