Lambda calculus description with beta reduction

Lambda.hs

{-#LANGUAGE StandaloneDeriving,MultiParamTypeClasses,GeneralizedNewtypeDeriving,ViewPatterns, DeriveFunctor #-}

import Data.List (nub)
import Control.Monad.Reader (runReader, local, asks, liftM2, Reader, MonadReader)


-- Lambda expressions 
data Expr a     = T a -- terminal name
                | a :-> Expr a -- lambda parameter abstraction
                | Expr a :$ Expr a -- expression composition
                deriving (Show, Functor, Eq)

-- replacing action parameters
data Replace a = Replace {
    target :: a, -- name target to replace
    expr :: Expr a, -- expression replacing the target
    freevarset :: [a] -- shared free variables of the expr
    } deriving (Show)

-- make a replace from a target and a replacing expression
replace :: Eq a =>  a -> Expr a -> Replace a
replace x = Replace x <*> nub . freevars 

-- free variables of an expression , with duplicates 
freevars :: Eq a => Expr a -> [a]
freevars (T x) = [x]
freevars (x :-> t) = filter (/= x) $ freevars t
freevars (e :$ e') = freevars e ++ freevars e'

-- computational environment, serving fresh renaming via Reader interface
newtype Freshes a b = Freshes (Reader [a] b) deriving (Functor, Applicative, Monad, MonadReader [a])

-- run, given a list of fresh names
withFreshes :: [a] -> Freshes a b -> b
withFreshes xs (Freshes r) = runReader r xs

-- (==) is noisy
eq :: Eq a => a -> a -> Bool
eq = (==)

-- change occurrences of x in p in expr, using Functor.
-- should be correct to use Functor Expr as even lambda introduction of the target will be substituted, 
-- overhead for not ignoring shadowing

substitute :: Eq a => a -> a -> Expr a -> Expr a
substitute p y  = fmap s where
    s (eq y -> True) = p
    s z = z

-- main logic for beta-reduction. this solution unshadows all, changing all abstraction names
captures :: Eq a =>  Expr a -> Replace a -> Freshes a (Expr a)
captures (T x) (Replace (eq x -> True) r _)  = return r -- replace
captures v@(T _) _ = return v -- keep old
captures (t :$ s) r = liftM2 (:$) (captures t r) (captures s r) -- let captures through both
captures l@(x :-> _) (Replace (eq x -> True) _ _)  = return l -- the introduction cancels the replacement
captures (x :-> t) r = do
        p:ps <- asks $ dropWhile (`elem` freevarset r)  -- throw away free variables in t, hostinate alpha 
        local (const $ filter (/= p) ps) $ -- what ever is taken as new name, never reuse it down this path
            (:->) p <$> captures (substitute p x t) r -- actual alpha transform


-- single reduction step, hunting and collapsing  x :-> y :$ z pattern (lambda application)
reduction :: Eq a => Expr a -> Freshes a (Expr a)
reduction v@(T x) = return v -- reduction branch over
reduction (x :-> t) = (:->) x <$> reduction t -- lambda through
reduction (x :-> t :$ y) = reduction y >>= local (filter $ (/=) x) . captures t . replace x -- here we go
reduction (e :$ e') = liftM2 (:$) (reduction e) (reduction e') -- application through

--  beta-reduction steps
betas :: Eq a => Expr a -> Freshes a [Expr a]
betas e = (e :) <$> do 
    e' <- reduction e
    if e == e' then return []
    else betas e'

beta :: Eq a => Expr a -> Freshes a (Expr a) 
beta e = last <$> betas e

-- alpha equality check
alpha :: Eq a => Expr a -> Expr a -> Bool
alpha = alpha' [] where
    alpha' as (T x) (T y) = case lookup x as of
        Nothing -> x == y -- free vars matching
        Just y' -> y == y' -- bound vars matching
    alpha' as (x :-> tx) (y :-> ty) = alpha' ((x,y):as) tx ty
    alpha' as (x1 :$ x2) (y1 :$ y2) = alpha' as x1 y1 && alpha' as x2 y2
    alpha' _ _ _ = False

------------ running ----------------------------------------------------

run :: Enum a => a -> Freshes a b -> b
run x = withFreshes (enumFrom x)

runBeta :: (Enum a, Eq a) => a -> Expr a -> Expr a
runBeta x = run x . beta

--------- famous -----------------------------------------------------

self x = x :-> (T x :$ T x)
omega x = self x :$ self x
id_ x = x :-> T x

zero x y = x :-> (y :-> T y)
suc w y x = w :-> (y :-> (x  :-> (T y :$ (T w :$ T y :$ T x))))
  
----- appealing fresh names set ----------------------------------------------
data V = X | Y | Z | W | J | U | L | H | R | G | S | N | M | K | Q | F | D | O | B | C deriving (Show,Enum,Eq,Bounded)
 
z = zero X Y 
s = (suc X Y Z :$) 
one = s z
two = s one
three = s two
--------------------------------------------

main = mapM_ print $ run X . betas $ three