Lambda.hs

module Lambda where

-----------------------------------------------------------
----------------------- API -------------------------------
-----------------------------------------------------------

num2fun :: Int -> Fun
num2fun n = Fun (show n) [] $ go n
  where
    go n | n < 0  = E[F neg, go (-n)]
         | n == 0 = E[F zero]
         | n > 0  = E[F inc, go (n-1)]

desugar :: Fun -> Lam
desugar = f2lam

enlist :: [Fun] -> Fun
enlist = foldr (\f a -> apply [cons, f, a]) empty

apply :: [Fun] -> Fun
apply funs = Fn [] $ E $ map F funs

reduce :: Fun -> Lam
reduce = eval . f2lam

pretty :: Lam -> IO ()
pretty e = putStrLn $ go e
  where
    go   (Var c)   = [c]
    go   (App x y) = brace $ go x ++   " "    ++ go y
    go f@(Abs c e)
        | f === reduce true  = "true"
        | f === reduce false = "false"
        | f === reduce empty = "[]"
        | f === reduce (num2fun 5) = "5"
        | f === reduce (num2fun 4) = "4"
        | f === reduce (num2fun 3) = "3"
        | f === reduce (num2fun 2) = "2"
        | f === reduce (num2fun 1) = "1"
        | f === reduce (num2fun 0) = "0"
        | otherwise = brace $ "λ" ++ c : " ⇒ " ++ go e

-----------------------------------------------------------
--------------- lambda terms & beta reduction -------------
-----------------------------------------------------------

-- λ-terms
data Lam = Var Char      -- variable        e.g. x
         | App Lam  Lam  -- application     e.g. f x
         | Abs Char Lam  -- abstraction     e.g. \x -> exp

instance Show Lam where
    show (Var c)   = [c]
    show (App x y) = brace $ show x ++   " "    ++ show y
    show (Abs c e) = brace $ "λ" ++ c : " ⇒ " ++ show e

-- find the free variables in a λ-term
fv :: Lam -> [Char]
fv = distinct . fv' where
    fv' (Var c) = [c]
    fv' (App m n) = fv' m ++ fv' n
    fv' (Abs c e) = filter (/=c) $ fv' e

-- find the bound variables in a λ-term
bv :: Lam -> [Char]
bv = distinct . bv' where
    bv' (Var c) = []
    bv' (App m n) = bv' m ++ bv' n
    bv' (Abs c e) = c : bv' e

-- substitute a λ-term for every free occurrence
-- of a variable in another λ-term changing bound
-- variables to avoid clashes if needed.
sub :: Lam -> Char -> Lam -> Lam
sub n x (Var v)
    | x == v    = n
    | otherwise = Var v
sub n x (App p q) = App (sub n x p) (sub n x q)
sub n x (Abs y p)
    | x == y           = Abs y p
    | x `notElem` fv p = Abs y p
    | y `notElem` fv n = Abs y $ sub n x p
    | otherwise        = Abs z $ sub n x $ sub (Var z) y p
  where
    z = pickNewVar n p

-- check if 2 λ-terms are α-convertible
(===) :: Lam -> Lam -> Bool
(===) (Var x)   (Var y)   = x == y
(===) (App p q) (App r s) = (p === r) && (q === s)
(===) (Abs x p) (Abs y q)
    | x == y    = p  ===  q
    | otherwise = p' ===  q'
  where
    z  = pickNewVar  p q
    p' = sub (Var z) x p
    q' = sub (Var z) y q
(===) _ _ = False

-- β-reduction
beta :: Lam -> Maybe Lam
beta (App (Abs x m) n) = Just $ sub n x m
beta _                 = Nothing

-- do *all* reductions starting from the left
-- warning: won't terminate for recursive functions!
eval :: Lam -> Lam
eval ex = case go ex of
    Just ex' -> eval ex'
    Nothing  -> ex
  where
    go (Var c)   = Nothing
    go (Abs c m) = fmap (Abs c) (go m)
    go (App m n) = case beta (App m n) of
        Just p  -> Just p
        Nothing -> case go m of
            Just p  -> Just $ App p n
            Nothing -> case go n of
                Just p  -> Just $ App m p
                Nothing -> Nothing

-- Y combinator: λf.(λx.f(x x)) (λx.f(x x))
yComb :: Lam
yComb = Abs 'f' $ App fxx fxx
  where
    xx  = App (Var 'x') (Var 'x')
    fxx = Abs 'x' $ App (Var 'f') xx

fix :: Lam -> Lam
fix = App yComb

-- picks a new non-clashing variable
pickNewVar :: Lam -> Lam -> Char
pickNewVar p q = head $ filter notFree ['a'..'z']
  where notFree = (`notElem` fv (App p q))

-----------------------------------------------------------
------------------ syntacic sugar -------------------------
-----------------------------------------------------------

data Fun = Fun String [Char] Exp     -- named functions
         | Fn         [Char] Exp     -- lambda expressions

data Exp = E [Exp]                   -- expression sequence
         | L  Char [Char] Exp Exp    -- let binding
         | R  Char [Char] Exp Exp    -- recursive let binding
         | F  Fun                    -- singleton function
         | V  Char                   -- a variable

instance Show Fun where
    show (Fn       []   ex) = show ex
    show (Fn       args ex) = 'λ' : unwords [
        args2Str args, "⇒", show ex]
    show (Fun name args ex) = unwords [name,
        args2Str args,  "=", show ex]

instance Show Exp where
    show (E exps) = brace $ unwords $ map show exps
    show (F  (Fun s _ _)) = s
    show (F  fn)  = brace $ show fn
    show (V  var) = [var]
    show (L  v args body ex) = unwords ["let",    [v],
        args2Str args, "=", show body, "in ", show ex]
    show (R  v args body ex) = unwords ["letrec", [v],
        args2Str args, "=", show body, "in ", show ex]

-- convert a function to a λ-term
f2lam :: Fun -> Lam
f2lam = go where
    go (Fn    args ex) = go' args ex
    go (Fun _ args ex) = go' args ex
    go' args ex = foldr Abs (e2lam ex) args

-- convert an expression to a λ-term
e2lam :: Exp -> Lam
e2lam (E exps) = foldl1 App $ map e2lam exps
e2lam (F  fun) = f2lam fun
e2lam (V  var) = Var var
e2lam (L  v args body ex) = e2lam let2ex where
    let2ex = E[F(Fn [v] ex), F(Fn args body)]
e2lam (R  f args body ex) = App let2ex (fix recExp) where
    recExp = e2lam $ F(Fn (f:args) body)
    let2ex = e2lam $ F(Fn [f] ex)

a = V 'a'
b = V 'b'
c = V 'c'
d = V 'd'
e = V 'e'
f = V 'f'
g = V 'g'
h = V 'h'
l = V 'l'
m = V 'm'
n = V 'n'
p = V 'p'
s = V 's'
t = V 't'
x = V 'x'
y = V 'y'
z = V 'z'

-- id x = x
identity :: Fun
identity = Fun "id" "x" x

-----------------------------------------------------------
------------------------- tuples --------------------------
-----------------------------------------------------------

-- tuple x y z = \t -> t x y z
tuple :: Fun
tuple  = Fun "tuple" "xyz" $ F $ Fn "t" $ E[t,x,y,z]

-- first  t = t (\x y z -> x)
first :: Fun
first  = Fun "fst" "t" $ E[t, F(Fn "xyz" x)]

-- second t = t (\x y z -> y)
second :: Fun
second = Fun "snd" "t" $ E[t, F(Fn "xyz" y)]

-- third t = t (\x y z -> z)
third :: Fun
third  = Fun "thd" "t" $ E[t, F(Fn "xyz" z)]

-----------------------------------------------------------
-------------------------- booleans -----------------------
-----------------------------------------------------------

-- true  = \x y -> x
-- false = \x y -> y
true :: Fun
true  = Fun "True"  "xy" x
false :: Fun
false = Fun "False" "xy" y

-- ifThenElse c x y = c x y
ite :: Fun
ite = Fun "ifThenElse" "cxy" $ E[c,x,y]

-- and x y = ifthenelse x (ifthenelse y true) false
and' :: Fun
and' = Fun "and" "xy" $
    E[F ite, x, E[F ite, y, F true], F false]

-- or  x y = ifthenelse x true (ifthenelse y true false)
or' :: Fun
or'  = Fun "or"  "xy" $
    E[F ite, x, F true, E[F ite, y, F true, F false]]

-- not x = ifthenelse x false true
not' :: Fun
not' = Fun "not" "x" $ E[F ite, x, F false, F true]

-- xor x y = (x or y) and (not x or not y)
xor :: Fun
xor = Fun "xor" "xy" $ E[F and', E[F or', x, y],
    E[F or', E[F not', x], E[F not', x]]]

-- xnor x y = not (xor x y)
xnor :: Fun
xnor = Fun "xnor" "xy" $ E[F not', E[F xor, x, y]]

-----------------------------------------------------------
-------------------------- lists --------------------------
-----------------------------------------------------------

-- cons = \h t -> \c -> c h t
cons :: Fun
cons = Fun "cons" "ht" $ F $ Fn "c" $ E[c,h,t]

-- head  l = l (\x y -> x)
head' :: Fun
head' = Fun "fst" "l" $ E[l, F(Fn "xy" x)]

-- tail l = l (\x y -> y)
tail' :: Fun
tail' = Fun "snd" "l" $ E[l, F(Fn "xy" y)]

-- [] = \f -> true
empty :: Fun
empty = Fun "empty" "f" $ F true

-- isEmpty l = l (\h t -> false)
isEmpty :: Fun
isEmpty = Fun "isEmpty" "l" $ E[l, F(Fn "ht" $ F false)]

-- foldl f acc lst =
--       if isEmpty lst
--         then acc
--         else foldl f (f acc (head lst)) (tail lst)
--
-- Amended to use recursive let!!!
--  fold = letrec g f a l = ... g ... in g
fold :: Fun
fold = Fun "fold" [] $ R 'g' "fal" (
    E[F ite, E[F isEmpty, l],     -- if isEmpty lst
    a, E[g, f,                    -- then acc else foldl f
    E[f, a, E[F head', l]],       -- (f (head lst) acc)
    E[F tail', l]]])              -- (tail lst)
    g

-- reverse lst = foldl (\acc elt -> (elt:acc)) [] lst
reverse' :: Fun
reverse' = Fun "reverse" "l" $
    E[F fold, F(Fn "ae" $ E[F cons, e, a]), F empty, l]

-- map f lst  =
--      let
--        map' f lst lst' =
--          if isEmpty lst
--            then (reverse lst') else
--            map' f (tail lst) (head lst: lst')
--      in
--        map' f lst []
map' :: Fun
map' = Fun "map" "fl" $
    R 'm' "la" (E[F ite, E[F isEmpty, l],
    E[F reverse', a],
    E[m, E[F tail', l], E[F cons, E[f, E[F head', l]], a]]]) $
    E[m, l, F empty]

-- list concatenation
-- (+++) l1 l2 = foldl (\acc elt -> (elt:acc)) l2 (reverse l1)
(+++) :: Fun
(+++) = Fun "++" "xy" $ E[F fold, F f, y, E[F reverse', x]]
  where
    f = Fn "ae" $ E[F cons, e, a]

-- length lst = foldl calc_length 0 lst
--   where
--     calc_length _ len = inc len
length' :: Fun
length' = Fun "length" "x" $ E[F fold, F f, F zero, x]
  where
    f = Fn "l_" $ E[F inc, l]

-----------------------------------------------------------
------------------------- integers ------------------------
-----------------------------------------------------------

-- u0 = false:[]
u0 :: Exp
u0 = E[F cons, F false, F empty]

-- +0 = true:u0
zero :: Fun
zero = Fun "zero" [] $ E[F cons, F true, u0]

-- isPos n = head n
isPos :: Fun
isPos = Fun "isPos" "n" $ E[F head', n]

-- isNeg n = not (head n)
isNeg :: Fun
isNeg = Fun "isNeg" "n" $ E[F not', E[F head', n]]

-- isZero n = not (head (tail n))
isZero :: Fun
isZero = Fun "isZero" "n" $
    E[F not', E[F head', E[F tail', n]]]

-- sign n = head n
sign :: Fun
sign = Fun "sign" "n" $ E[F head', n]

-- (==) m n = let
--     s = head m
--     t = head n
--     a = head (tail m)
--     b = head (tail n)
--     if (xnor s t) then
--       if (and (not a) (not b))
--         then true
--         else
--           if (and a b)
--             then  (==) (s:(tail m)) (t:(tail n))
--             else false
--       else false
eq :: Fun
eq = Fun "==" [] $ R 'f' "mn" (
    L 's' [] (E[F head', m]) (
    L 't' [] (E[F head', n]) (
    L 'a' [] (E[F head', E[F tail', m]]) (
    L 'b' [] (E[F head', E[F tail', n]]) (
    E[F ite, E[F xnor, s, t],
        E[F ite, E[F and', E[F not', a], E[F not', b]],
            F true,
            E[F ite, E[F and', a, b],
                E[f, E[F cons, s, E[F tail', m],
                     E[F cons, t, E[F tail', n]]]],
                F false],
    F false]])))))
    f

-- neg n = (not (head n)):(tail n)
neg :: Fun
neg = Fun "neg" "n" $
    E[F cons, E[F not', E[F head', n]], E[F tail', n]]

-- inc n = if isPos n
--          then true:true:(tail n)
--          else if isZero n
--            then 1
--            else false:(tail (tail n))
inc :: Fun
inc = Fun "inc" "n" $
    E[F ite, E[F isPos, n],
      E[F cons, F true, E[F cons, F true, E[F tail', n]]],
      E[F ite, E[F isZero, n],
        E[F cons, F true, E[F cons, F true, u0]],
        E[F cons, F false, E[F tail', E[F tail', n]]]]]

-- dec n = if isZero n
--            then -1
--            else if isNeg n
--              then false:true:(tail n) n
--              else true:(tail (tail n))
dec :: Fun
dec = Fun "dec" "n" $
  E[F ite, E[F isZero, n],
    E[F cons, F false, E[F cons, F true, u0]],
    E[F ite, E[F isNeg, n],
      E[F cons, F false, E[F cons, F true, E[F tail', n]]],
      E[F cons, F true, E[F tail', E[F tail', n]]]]]

-- add m n = f (if isNeg m then neg m else m) n
--           where
--             f m n = if isZero m
--               then n
--               else f (dec m) (inc n)
add :: Fun
add = Fun "add" "mn" $
    R 'f' "ab" (
    E[F ite, E[F isZero, a],
        b,
        E[f, E[F dec, a], E[F inc, b]]])(
    E[f, E[F ite, E[F isNeg, m], E[F neg, m], m], n])

-- mult m n = if or (isZero m) (isZero n)
--              then zero
--              else f (if isNeg m then neg m else m) zero
--   where
--     f m a = if isZero m
--       then a
--       else f (dec m) (add a n)
mult :: Fun
mult = Fun "mult" "mn" $
  R 'f' "ma" (
  E[F ite, E[F isZero, m],
    a,
    E[f, E[F dec, m], E[F add, a, n]]]) (
  E[F ite, E[F or', E[F isZero, m], E[F isZero, n]],
    F zero,
    E[f, E[F ite, E[F isNeg, m], E[F neg, m], m], F zero]])

-----------------------------------------------------------
------------------------- utils ---------------------------
-----------------------------------------------------------

-- remove duplicates from list
distinct :: Eq a => [a] -> [a]
distinct [] = []
distinct (x:xs) | x `elem` xs = distinct xs
                | otherwise = x:distinct xs

-- enclose string in braces
brace :: String -> String
brace s = "(" ++ s ++ ")"

-- format args with spaces
args2Str :: [Char] -> String
args2Str args = unwords (map (:[]) args)

-----------------------------------------------------------

> pretty $ desugar $ apply [inc, zero]
((λn ⇒ ((((λc ⇒ (λx ⇒ (λy ⇒ ((c x) y)))) ((λn ⇒ ((λl ⇒ (l true)) n)) n)) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) true) (((λh ⇒ (λ
t ⇒ (λc ⇒ ((c h) t)))) true) ((λl ⇒ (l false)) n)))) ((((λc ⇒ (λx ⇒ (λy ⇒ ((c x) y)))) ((λn ⇒ ((λx ⇒ ((((λc ⇒ (λx ⇒ (λy ⇒
((c x) y)))) x) false) true)) ((λl ⇒ (l true)) ((λl ⇒ (l false)) n)))) n)) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) true) (((λh ⇒
(λt ⇒ (λc ⇒ ((c h) t)))) true) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) false) [])))) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) false) ((λl
 ⇒ (l false)) ((λl ⇒ (l false)) n)))))) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) true) (((λh ⇒ (λt ⇒ (λc ⇒ ((c h) t)))) false) [])
))