Haskell Lambda Alpha Equivalence

Question

I am trying to write down an alpha equivalence function in Haskell for lambda.

data Expr = App Expr Expr | Lam Int Expr | Var Int deriving (Show,Eq)

I've read some online resources but I can't transform them into code. Thank you

Answer 1

So two expressions are alpha equivalent if you can turn one into the other by renaming variables. So how could we capture this? There are two main ways:

1. Keep track of which variable names must correspond to one another in the two expressions.
2. (Explicitly or implicitly) convert into a form where instead of variable names, the number of the enclosing scope is used.

Let’s go for the first one

-- helper functions for association lists
type Alist a = [(a,a)]
assoc, rassoc :: Eq a => a -> Alist a -> a
assoc x ((a,b):ps) = if x == a then b else assoc x ps
rassoc x = assoc x . map (\(a,b) -> (b,a))
acons a b l = (a,b):l

(=*=) :: Expr -> Expr -> Bool
a =*= b = eq [] a b where
  eq l (Lam n x) (Lam m y) = eq (acons n m l) x y
  eq l (Var n) (Var m) = assoc n l == m && n == rassoc m l
  eq l (App f u) (App g v) = eq l f g && eq l u v
  eq l _ _ = False

The only real subtlety here is the case of comparing variables. To check that x and y are alpha equivalent we need to check that the binding for x corresponds to a binding of y AND the binding for y corresponds to a binding for x. Otherwise we might say that \x.\y.x is alpha equivalent to \y.\y.y.

It’s also worth noting that malformed expressions will result in match failures.

Here’s how to implicitly do the second option:

varN :: Eq a => a -> [a] -> Int
varN a xs = v 0 xs where
  v n (x:xs) = if a == x then n else v (n+1) xs

a =*= b = eq [] [] a b in where
  eq k l (Lam n x) (Lam m y) = eq (n:k) (m:l) x y
  eq k l (Var n) (Var m) = varN n k == varN m l
  eq k l (App f u) (App g v) = eq k l f g && eq k l u v
  eq k l _ _ = False

Hopefully you can see that these are equivalent