content: module LambdaChurch where
  
  import Data.Char (isLetter)
  import Data.List ( nub )
  
  class ShowNice a where
      showNice :: a -> String
  
  class ReadNice a where
      readNice :: String -> (a, String)
  
  data Variable
    = Variable
    { name :: String
    , count :: Int
    }
    deriving (Show, Eq, Ord)
  
  var :: String -> Variable
  var x = Variable x 0
  
  instance ShowNice Variable where
      showNice (Variable x 0) = x
      showNice (Variable x cnt) = x <> "_" <> show cnt
  
  instance ReadNice Variable where
      readNice s
        | null x = error $ "expected variable but found " <> s
        | otherwise = (var x, s')
        where
          (x, s') = span isLetter s
  
  freshVariable :: Variable -> [Variable] -> Variable
  freshVariable var vars = Variable x (cnt + 1)
    where
      x = name var
      varsWithName = filter ((== x) . name) vars
      Variable _ cnt = maximum (var : varsWithName)
  
  
  data Term
    = V Variable
    | App Term Term
    | Lam Variable Term
    deriving (Show)
  
  -- alpha-equivalence
  aEq :: Term -> Term -> Bool
  aEq (V x) (V x') = x == x'
  aEq (App t1 t2) (App t1' t2') = aEq t1 t1' && aEq t2 t2'
  aEq (Lam x t) (Lam x' t')
    | x == x'   = aEq t t'
    | otherwise = aEq (subst (V y) x t) (subst (V y) x' t')
    where
      fvT = freeVars t
      fvT' = freeVars t'
      allFV = nub ([x, x'] ++ fvT ++ fvT')
      y = freshVariable x allFV
  aEq _ _ = False
  
  v :: String -> Term
  v x = V (var x)
  
  lam :: String -> Term -> Term
  lam x = Lam (var x)
  
  lams :: [String] -> Term -> Term
  lams xs t = foldr lam t xs
  
  ($$) :: Term -> Term -> Term
  ($$) = App
  infixl 9 $$
  
  instance ShowNice Term where
      showNice (V var) = showNice var
      showNice (App t1 t2) = "(" <> showNice t1 <> " " <> showNice t2 <> ")"
      showNice (Lam var t) = "(" <> "\\" <> showNice var <> "." <> showNice t <> ")"
  
  instance ReadNice Term where
      readNice [] = error "Nothing to read"
      readNice ('(' : '\\' : s) = (Lam var t, s'')
        where
          (var, '.' : s') = readNice s
          (t, ')' : s'') = readNice s'
      readNice ('(' : s) = (App t1 t2, s'')
        where
          (t1, ' ' : s') = readNice s
          (t2, ')' : s'') = readNice s'
      readNice s = (V var, s')
        where
          (var, s') = readNice s
  
  freeVars :: Term -> [Variable]
  freeVars (V var) = [var]
  freeVars (App t1 t2) = nub $ freeVars t1 ++ freeVars t2
  freeVars (Lam var t) = filter (/= var) (freeVars t)
  
  
  -- subst u x t defines [u/x]t, i.e.,  substituting u for x in t
  -- for example [3/x](x + x) == 3 + 3
  -- This substitution avoids variable captures so it is safe to be used when 
  -- reducing terms with free variables (e.g., if evaluating inside lambda abstractions)
  subst
      :: Term     -- ^ substitution term
      -> Variable -- ^ variable to be substitutes
      -> Term     -- ^ term in which the substitution occurs
      -> Term
  subst u x (V y)
    | x == y    = u
    | otherwise = V y
  subst u x (App t1 t2) = App (subst u x t1) (subst u x t2)
  subst u x (Lam y t)
    | x == y          = Lam y t
    | y `notElem` fvU = Lam y (subst u x t)
    | x `notElem` fvT = Lam y t
    | otherwise       = Lam y' (subst u x (subst (V y') y t))
    where
      fvT = freeVars t
      fvU = freeVars u
      allFV = nub ([x] ++ fvU ++ fvT)
      y' = freshVariable y allFV
  
  -- Normal order reduction
  -- - like call by name
  -- - but also reduce under lambda abstractions if no application is possible
  -- - guarantees reaching a normal form if it exists
  normalReduceStep :: Term -> Maybe Term
  normalReduceStep (App (Lam v t) t2) = Just $ subst t2 v t
  normalReduceStep (App t1 t2)
    | Just t1' <- normalReduceStep t1 = Just $ App t1' t2
    | Just t2' <- normalReduceStep t2 = Just $ App t1 t2'
  normalReduceStep (Lam x t)
    | Just t' <- normalReduceStep t = Just $ Lam x t'
  normalReduceStep _ = Nothing
  
  normalReduce :: Term -> Term
  normalReduce t
    | Just t' <- normalReduceStep t = normalReduce t'
    | otherwise = t
  
  reduce :: Term -> Term
  reduce = normalReduce
  
  -- alpha-beta equivalence (for strongly normalizing terms) is obtained by
  -- fully evaluating the terms using beta-reduction, then checking their
  -- alpha-equivalence.
  abEq :: Term -> Term -> Bool
  abEq t1 t2 = aEq (reduce t1) (reduce t2)
  
  evaluate :: String -> String
  evaluate s = showNice (reduce t)
    where
      (t, "") = readNice s
  
  
  -- Church Encodings in Lambda
  