Homework/HW6.hs

module HW6 where

import Prelude hiding (print,and,or,not,pred,succ,fst,snd,either,length,sum,product)

import DeBruijn


--
-- * Part 1: Nameless lambda calculus
--

-- | λx. (λx.x) x
--
--   >>> eval ex1
--   Abs (Ref 0)
--
ex1 :: Exp
ex1 = Abs (App (Abs (Ref 0)) (Ref 0))

-- | (λxy.xz) z z
--
--   >>> eval ex2
--   App (Ref 0) (Ref 0)
--
ex2 :: Exp
ex2 = App (App (Abs (Abs (App (Ref 1) (Ref 2)))) (Ref 0)) (Ref 0)

-- | λy. (λxy.yx) y z
--
--   >>> eval ex3
--   Abs (App (Ref 1) (Ref 0))
--   
ex3 :: Exp
ex3 = Abs (App (App (Abs (Abs (App (Ref 0) (Ref 1)))) (Ref 0)) (Ref 1))


-- | Is the given nameless lambda calculus term a closed expression? That is,
--   does it contain no free variables?
--
--   >>> closed (Ref 0)
--   False
--
--   >>> closed (Abs (Ref 0))
--   True
--
--   >>> closed (Abs (App (Ref 0) (Ref 1)))
--   False
--
--   >>> closed (Abs (App (Abs (App (Ref 0) (Ref 1))) (Ref 0)))
--   True
--
closed :: Exp -> Bool
closed = cl 0
    where
        cl n (Ref i) = i < n
        cl n (App l r) = cl n l && cl n r
        cl n (Abs e) = cl (n+1) e


--
-- * Part 2: Church pair update functions
--

-- | Write a lambda calculus function that replaces the first element in a
--   Church-encoded pair. The first argument to the function is the new
--   first element, the second argument is the original pair.
--
--   >>> :{
--     eval (app2 pair true (num 3)) ==
--     eval (app2 setFst true (app2 pair (num 2) (num 3)))
--   :}
--   True
--
setFst :: Exp
setFst = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 4)) (Ref 0))
    -- \x -> \p -> \f -> p (\a -> \b -> f x b)

-- | Write a lambda calculus function that replaces the second element in a
--   Church-encoded pair. The first argument to the function is the new
--   second element, the second argument is the original pair.
--
--   >>> :{
--     eval (app2 pair (num 2) true) ==
--     eval (app2 setSnd true (app2 pair (num 2) (num 3)))
--   :}
--   True
--
setSnd :: Exp
setSnd = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 1)) (Ref 4))
    -- \x -> \p -> \f -> p (\a -> \b -> f a x)

--
-- * Part 3: Church encoding a Haskell program
--

-- | Pretend Haskell's Int is restricted to Nats.
type Nat = Int

-- | A simple data for representing shapes.
data Shape
   = Circle    Nat
   | Rectangle Nat Nat
  deriving (Eq,Show)

-- | A smart constructor for building squares.
square :: Nat -> Shape
square l = Rectangle l l

-- | Compute the area of a shape using a rough approximation of pi.
area :: Shape -> Nat
area (Circle r)      = 3 * r * r
area (Rectangle l w) = l * w

-- | Compute the perimeter of a shape using a rough approximation of pi.
perimeter :: Shape -> Nat
perimeter (Circle r)      = 2 * 3 * r
perimeter (Rectangle l w) = 2 * l + 2 * w

-- | Encode the circle constructor as a lambda calculus term. The term
--   should be a function that takes a Church-encoded natural number as input
--   and produces a Church-encoded shape as output.
circleExp :: Exp
circleExp = inL

-- | Encode the rectangle constructor as a lambda calculus term. The term
--   should be a function that takes two Church-encoded natural numbers as
--   input and produces a Church-encoded shape as output.
rectangleExp :: Exp
rectangleExp = Abs $ Abs $ App inR $ app2 pair (Ref 1) (Ref 0)

-- | Convert a shape into a lambda calculus term. This function helps to
--   illustrate how your encodings of the constructors should work.
encodeShape :: Shape -> Exp
encodeShape (Circle r)      = App circleExp (num r)
encodeShape (Rectangle l w) = app2 rectangleExp (num l) (num w)

-- | Encode the square function as a lambda calculus term.
squareExp :: Exp
squareExp = Abs $ app2 rectangleExp (Ref 0) (Ref 0)

-- | Encode the area function as a lambda calculus term.
areaExp :: Exp
areaExp = Abs $ app2 (Ref 0)
    (Abs $ app2 mult (num 3) (app2 mult (Ref 0) (Ref 0)))
    (Abs $ App (Ref 0) mult)

-- | Encode the perimeter function as a lambda calculus term.
perimeterExp :: Exp
perimeterExp = Abs $ app2 (Ref 0)
    (Abs $ app2 mult (num 6) (Ref 0))
    (Abs $ App (Ref 0) $ Abs $ Abs $ app2 mult (num 2) (app2 add (Ref 0) (Ref 1)))

-- | Some tests of your lambda calculus encodings.
--
--   >>> :{
--     checkEval (area (Circle 3))
--       (App areaExp (App circleExp (num 3)))
--   :}
--   True
--
--   >>> :{
--     checkEval (area (Rectangle 3 5))
--       (App areaExp (app2 rectangleExp (num 3) (num 5)))
--   :}
--   True
--
--   >>> :{
--     checkEval (area (square 4))
--       (App areaExp (App squareExp (num 4)))
--   :}
--   True
--
--   >>> :{
--     checkEval (perimeter (Circle 3))
--       (App perimeterExp (App circleExp (num 3)))
--   :}
--   True
--
--   >>> :{
--     checkEval (perimeter (Rectangle 3 5))
--       (App perimeterExp (app2 rectangleExp (num 3) (num 5)))
--   :}
--   True
--
--   >>> :{
--     checkEval (perimeter (square 4))
--       (App perimeterExp (App squareExp (num 4)))
--   :}
--   True
-- 
checkEval :: Nat -> Exp -> Bool
checkEval n e = num n == eval e

-- Alright, extra practice, let's go.
-- Part 1: 4-tuples (Bonus: n-tuples)
absN :: Int -> Exp -> Exp
absN n = flip (foldr $ const Abs) $ replicate n ()

apps :: Exp -> [Exp] -> Exp
apps e = foldl App e

tupleN :: Int -> Exp
tupleN n = absN (n+1) $ apps (Ref 0) $ map Ref $ [n, (n-1) .. 1]

selN :: Int -> Int -> Exp
selN n m = Abs $ App (Ref 0) $ absN m $ Ref $ m - n

tuple4 :: Exp
tuple4 = tupleN 4

sel14 :: Exp
sel14 = selN 1 4

sel24 :: Exp
sel24 = selN 2 4

sel34 :: Exp
sel34 = selN 3 4

sel44 :: Exp
sel44 = selN 4 4

-- Wait, the extra credit practice is mostly mechanical?
-- Boo!