-- | Notes taken by Jonas Grybė
--
-- VARIABLE BINDING PROBLEM:
-- When substituting in lambda calculus, we must change only FREE variables, not BOUND ones.
-- Example: (λx.λy.x(xy)) - x and y are bound, we can't just replace them.
--
-- TWO SOLUTIONS:
-- 1. Barendregt Convention: All variables must be unique (eliminates name conflicts).
-- 2. De Bruijn Indices: Don't use names - use numbers indicating distance to binding lambda.
--    Examples: λx.x → λ.0  |  λx.λy.x(xy) → λ.λ.1(10)  |  λx.λy.b(yx) → λ.λ.2(01)
--
-- EVALUATION STRATEGIES:
-- - Full Beta Reduction: Reduce anywhere (messy, can use function or argument first)
-- - Call by Value: Evaluate arguments before passing (Java, C#, C)
-- - Call by Name: No reduction inside abstractions (Haskell)

{-# LANGUAGE InstanceSigs #-}
module Lessons.Lesson14 where
import qualified Data.List as L


-- | Named lambda calculus representation. Grammar: term = x | λx.t | tt
data Term = Var String | Abs String Term | App Term Term

instance Show Term where
  show :: Term -> String
  show :: Term -> String
show (Var String
n) = String
n
  show (Abs String
n Term
t) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(/|", String
n, String
".", Term -> String
forall a. Show a => a -> String
show Term
t, String
")"]
  show (App Term
t1 Term
t2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(", Term -> String
forall a. Show a => a -> String
show Term
t1, String
" ", Term -> String
forall a. Show a => a -> String
show Term
t2, String
")"]

-- | Church boolean TRUE: λt.λf.t (returns first argument)
-- >>> show tru
-- "(/|t.(/|f.t))"
tru :: Term
tru :: Term
tru = String -> Term -> Term
Abs String
"t" (String -> Term -> Term
Abs String
"f" (String -> Term
Var String
"t"))

-- | Church boolean FALSE: λt.λf.f (returns second argument)
-- >>> show fls
-- "(/|t.(/|f.f))"
fls :: Term
fls :: Term
fls = String -> Term -> Term
Abs String
"t" (String -> Term -> Term
Abs String
"f" (String -> Term
Var String
"f"))

-- | Church numeral ZERO: λs.λz.z (successor applied 0 times)
-- Based on Peano numbers: z=zero, s=successor function.
-- >>> show c0
-- "(/|s.(/|z.z))"
c0 :: Term
c0 :: Term
c0 = String -> Term -> Term
Abs String
"s" (String -> Term -> Term
Abs String
"z" (String -> Term
Var String
"z"))

-- | Church numeral TWO: λs.λz.s(s z) (successor applied 2 times)
-- >>> show c2
-- "(/|s.(/|z.(s (s z))))"
c2 :: Term
c2 :: Term
c2 = String -> Term -> Term
Abs String
"s" (String -> Term -> Term
Abs String
"z" (Term -> Term -> Term
App (String -> Term
Var String
"s") (Term -> Term -> Term
App (String -> Term
Var String
"s") (String -> Term
Var String
"z"))))

-- | Builds left-associative applications from a list of terms.
-- Allows us to write expression over expression, building complex applications.
-- Takes multiple terms and combines them: apps [t1, t2, t3] = ((t1 t2) t3)
apps :: [Term] -> Term
apps :: [Term] -> Term
apps [] = String -> Term
forall a. HasCallStack => String -> a
error String
"Empty application"
apps [Term
_] = String -> Term
forall a. HasCallStack => String -> a
error String
"Two terms needed for application"
apps (Term
t1 : Term
t2 : [Term]
ts) = Term -> [Term] -> Term
apps' (Term -> Term -> Term
App Term
t1 Term
t2) [Term]
ts
  where
    apps' :: Term -> [Term] -> Term
apps' Term
t [] = Term
t
    apps' Term
t (Term
x : [Term]
xs) = Term -> [Term] -> Term
apps' (Term -> Term -> Term
App Term
t Term
x) [Term]
xs

-- | Logical AND for Church booleans: λb.λc.b c false
-- >>> show land
-- "(/|b.(/|c.((b c) (/|t.(/|f.f)))))"
land :: Term
land :: Term
land = String -> Term -> Term
Abs String
"b" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term
Abs String
"c" (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
apps [String -> Term
Var String
"b", String -> Term
Var String
"c", Term
fls]

-- | Example expression: (land true true)
-- >>> show expr
-- "(((/|b.(/|c.((b c) (/|t.(/|f.f))))) (/|t.(/|f.t))) (/|t.(/|f.t)))"
expr :: Term
expr :: Term
expr = [Term] -> Term
apps [Term
land, Term
tru, Term
tru]

-- plus :: Term
-- plus = Abs "m" $ Abs "n" $ Abs "s" $ Abs "z" $ apps [Var "m", Var "s", apps [Var "n", Var "s", Var "z"]]

-- | Nameless lambda terms using De Bruijn indices (no variable names, just numbers).
data ITerm
  = IVar Int
  | IAbs ITerm
  | IApp ITerm ITerm
  deriving (ITerm -> ITerm -> Bool
(ITerm -> ITerm -> Bool) -> (ITerm -> ITerm -> Bool) -> Eq ITerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ITerm -> ITerm -> Bool
== :: ITerm -> ITerm -> Bool
$c/= :: ITerm -> ITerm -> Bool
/= :: ITerm -> ITerm -> Bool
Eq)

instance Show ITerm where
  show :: ITerm -> String
  show :: ITerm -> String
show (IVar Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i
  show (IAbs ITerm
t) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(/|.", ITerm -> String
forall a. Show a => a -> String
show ITerm
t, String
")"]
  show (IApp ITerm
t1 ITerm
t2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(", ITerm -> String
forall a. Show a => a -> String
show ITerm
t1, String
" ", ITerm -> String
forall a. Show a => a -> String
show ITerm
t2, String
")"]

-- | Converts named terms to De Bruijn indices.
-- ctx: free variable names (context) - not bound within the term.
-- Walk the term with empty stack initially. When numbering, we go from inside to inside,
-- stacking variable names as we enter abstractions (n : stack).
-- findInd checks stack first (bound vars), then context (free vars).
-- For context variables: take context position + length of stack to renumber properly.

-- @
-- >>> deBruijnIndices [] tru
-- (/|.(/|.1))
-- >>> deBruijnIndices [] fls
-- (/|.(/|.0))
-- >>> deBruijnIndices ["a", "b", "c", "d"] $ Abs "s" (Abs "z" (Var "d"))
-- (/|.(/|.5))
-- @

deBruijnIndices :: [String] -> Term -> ITerm
deBruijnIndices :: [String] -> Term -> ITerm
deBruijnIndices [String]
ctx Term
t = [String] -> Term -> ITerm
walk [] Term
t
  where
    walk :: [String] -> Term -> ITerm
walk [String]
stack (Var String
n) = Int -> ITerm
IVar ([String] -> String -> Int
findInd [String]
stack String
n)
    walk [String]
stack (Abs String
n Term
t) = ITerm -> ITerm
IAbs ([String] -> Term -> ITerm
walk (String
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
stack) Term
t)
    walk [String]
stack (App Term
t1 Term
t2) = ITerm -> ITerm -> ITerm
IApp ([String] -> Term -> ITerm
walk [String]
stack Term
t1) ([String] -> Term -> ITerm
walk [String]
stack Term
t2)
    findInd :: [String] -> String -> Int
findInd [String]
stack String
n =
      case (String
n String -> [String] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`L.elemIndex` [String]
stack, String
n String -> [String] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`L.elemIndex` [String]
ctx) of
        (Just Int
i, Maybe Int
_) -> Int
i
        (Maybe Int
Nothing, Just Int
i) -> [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
L.length [String]
stack Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
        (Maybe Int, Maybe Int)
_ -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"No index for free variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n

-- | Shifts free variables by d. Cutoff c tracks binding depth.
-- Variables with index >= c are free and get shifted.
termShift :: Int -> ITerm -> ITerm
termShift :: Int -> ITerm -> ITerm
termShift Int
d = Int -> ITerm -> ITerm
walk Int
0
  where
    walk :: Int -> ITerm -> ITerm
walk Int
c (IVar Int
x)
      | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
c = Int -> ITerm
IVar (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d)
      | Bool
otherwise = Int -> ITerm
IVar Int
x
    walk Int
c (IAbs ITerm
t') = ITerm -> ITerm
IAbs (Int -> ITerm -> ITerm
walk (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ITerm
t')
    walk Int
c (IApp ITerm
t1 ITerm
t2) = ITerm -> ITerm -> ITerm
IApp (Int -> ITerm -> ITerm
walk Int
c ITerm
t1) (Int -> ITerm -> ITerm
walk Int
c ITerm
t2)

-- | Substitutes term s for variable j. Core operation for beta reduction.
-- When x == j+c, replace with s (shifted by c for binders).
termSubst :: Int -> ITerm -> ITerm -> ITerm
termSubst :: Int -> ITerm -> ITerm -> ITerm
termSubst Int
j ITerm
s = Int -> ITerm -> ITerm
walk Int
0
  where
    walk :: Int -> ITerm -> ITerm
walk Int
c (IVar Int
x)
      | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
c = Int -> ITerm -> ITerm
termShift Int
c ITerm
s
      | Bool
otherwise = Int -> ITerm
IVar Int
x
    walk Int
c (IAbs ITerm
t') = ITerm -> ITerm
IAbs (Int -> ITerm -> ITerm
walk (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ITerm
t')
    walk Int
c (IApp ITerm
t1 ITerm
t2) = ITerm -> ITerm -> ITerm
IApp (Int -> ITerm -> ITerm
walk Int
c ITerm
t1) (Int -> ITerm -> ITerm
walk Int
c ITerm
t2)

-- | Top-level substitution for beta reduction: (λ.t) s → [s/0]t
-- Shift s up, substitute, shift result down.
termSubstTop :: ITerm -> ITerm -> ITerm
termSubstTop :: ITerm -> ITerm -> ITerm
termSubstTop ITerm
s ITerm
t = Int -> ITerm -> ITerm
termShift (-Int
1) (Int -> ITerm -> ITerm -> ITerm
termSubst Int
0 (Int -> ITerm -> ITerm
termShift Int
1 ITerm
s) ITerm
t)

-- | Only abstractions are values in call-by-name.
isVal :: ITerm -> Bool
isVal :: ITerm -> Bool
isVal (IAbs ITerm
_) = Bool
True
isVal ITerm
_ = Bool
False

-- | Single-step evaluator (call-by-name, like Haskell).
-- From Pierce's "Types and Programming Languages".
-- Each eval call returns a shorter expression.

-- @
-- >>> eval $ deBruijnIndices [] expr
-- ((/|.(((/|.(/|.1)) 0) (/|.(/|.0)))) (/|.(/|.1)))
-- >>> eval $ eval $ deBruijnIndices [] expr
-- (((/|.(/|.1)) (/|.(/|.1))) (/|.(/|.0)))
-- >>> eval $ eval $ eval $ deBruijnIndices [] expr
-- ((/|.(/|.(/|.1))) (/|.(/|.0)))
-- >>> eval $ eval $ eval $ eval $ deBruijnIndices [] expr
-- (/|.(/|.1))
-- @

eval :: ITerm -> ITerm
eval :: ITerm -> ITerm
eval (IApp (IAbs ITerm
t') ITerm
v2) | ITerm -> Bool
isVal ITerm
v2 = ITerm -> ITerm -> ITerm
termSubstTop ITerm
v2 ITerm
t'
eval (IApp ITerm
v1 ITerm
t2) | ITerm -> Bool
isVal ITerm
v1 = ITerm -> ITerm -> ITerm
IApp ITerm
v1 (ITerm -> ITerm
eval ITerm
t2)
eval (IApp ITerm
t1 ITerm
t2) = ITerm -> ITerm -> ITerm
IApp (ITerm -> ITerm
eval ITerm
t1) ITerm
t2
eval ITerm
t = String -> ITerm
forall a. HasCallStack => String -> a
error (String -> ITerm) -> String -> ITerm
forall a b. (a -> b) -> a -> b
$ String
"No rule to apply for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ITerm -> String
forall a. Show a => a -> String
show ITerm
t