r3 - 14 Feb 2020 - 14:10:19 - MelissaONeillYou are here: TWiki >

CS131Spring2020 Web > Week4Class2

Improving the Language We Built

Recap: Story So Far

The code we began in Week4Class1 and saw lab3a.hs in lab looks like this:

type VarName = String

data Expr = Var    VarName          -- variable
          | Lambda VarName Expr     -- anonymous function
          | Apply  Expr Expr        -- application
    deriving (Show, Eq, Ord)

-- Find the free variables in an expression

freeVars ::  Expr -> Set VarName
freeVars (Var v)       = Set.singleton v
freeVars (Lambda v e)  = freeVars e \ Set.singleton v
freeVars (Apply e1 e2) = freeVars e1 `union` freeVars e2

-- Code to replace free variables by *closed* expressions
--   substC e1 x e2   ==   e1 [x -> e2]

substC :: Expr -> VarName -> Expr -> Expr
substC e1 x e2 | Set.null (freeVars e2) = doSubst e1
               | otherwise              = error "Bad substitution"
  where
    doSubst (Var y)             | x == y    = e2
                                | otherwise = Var y
    doSubst (Lambda y eBody)    | x == y    = Lambda y eBody
                                | otherwise = Lambda y (doSubst eBody)
    doSubst (Apply eFn eArg)                = Apply (doSubst eFn) (doSubst eArg)


-- Reduction rules for call-by-name

cbn :: Expr -> Expr
cbn (Apply eFn eArg) = 
      case nFn of
         Lambda v eBody ->  cbn (substC eBody v eArg)
         _              ->  Apply nFn eArg
    where
        nFn = cbn eFn
cbn other = other

-- Reduction rules for call-by-value

cbv :: Expr -> Expr
cbv (Apply eFn eArg) = 
      case vFn of
         Lambda v eBody ->  cbv (substC eBody v vArg)
         _              ->  Apply vFn vArg
    where
        vFn  = cbv eFn
        vArg = cbv eArg
cbv other = other

As we've said before, the lambda calculus is “all functions, all the time”.

In the example below, we can see that if we give cbn or cbv a closed lambda expression (no free variables) to evaluate, we always get a lambda function (Lambda) as a result. (Thus, even though cbn and cbv are Expr -> Expr, only one kind of Expr is ever returned.)

cbn> λi.i
λi.i
cbn> λp.λq.λs.s p q
λp.λq.λs.s p q
cbn> (λp.λq.λs.s p q) (λa.λb.a) (λc.λd.d)
λs.s (λa.λb.a) (λc.λd.d)
cbn>

In substC, we insist that the code we try to substitute has no free variables. If we evaluate an expression that has free variables in it, sometimes things work, sometimes they don't (specifically, when there are free variables in an apply, if evaluation calls substC with free variables in the last argument)

cbn> f x
f x
cbn> (\y.\x.x y) x
!! caught exception: Bad substitution

Since we only really support closed expressions, it's better to change our code for cbn and cbv to give an error when we find a variable that's not been substituted out (which means it must be free because as we evaluate we substitute out the bound ones as they become bound).

In future code we'll write, the first case above will give an error too:

cbn> f x
!! caught exception: Unsubstituted variable: f

One thing to notice about our call-by-name reduction scheme is that it doesn't take things all the way to β-normal form—once it's reduced things down to a function value it stops, even if the body of the function could be further simplified. For example:

cbn> λx.(λi.i) x
λx.(λi.i) x
cbn>

If we had something that did full-blown normal-order reduction, we'd a different answer:

nml> λx.(λi.i) x
λx.x
nml>

But normal-order reduction has to handle more general substitution where there may be free variables and thus perform variable renaming. In the example below, the second lambda expression is α-equivalent to the first, but β-reducing the second one to normal form requires us to rename the inner x (to a in this case) to avoid changing the meaning of the code.

nml> λx.(λy.λz.y z) x
λx.λz.x z
nml> λx.(λy.λx.y x) x
λx.λa.x a
nml>

Nevertheless, we can still compute interesting things and compute any computable function. Below we have code to calculate factorials of the numbers 0…5 (based on code from the first homework). The Church numerals it produces aren't fully simplified, but you can still count the “f x”s to read out the answer.

cbn> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f x)
λf.λx.f ((λf.λx.x) f x)
cbn> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f (f x))
λf.λx.f ((λf.λx.f ((λf.λx.x) f x)) f x)
cbn> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f (f (f x)))
λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.x) f x)) f x)) f x)) f x)) f x)) f x)
cbn> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f (f (f (f x))))
λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.x) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)
cbn> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f (f (f (f (f x)))))
λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.f ((λf.λx.x) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)) f x)

So, yes, we can compute things, but it's not much fun to work with.

With normal-order reduction we'd get a nicer looking answer, for example, the final factorial above looks like this:

nml> (λk.k (λp.λb.b (λf.λx.p (λt.λf.t) f (f x)) (λf.p (λt.λf.t) (p (λt.λf.f) f))) (λb.b (λf.f) (λf.f)) (λt.λf.f) (λf.λn.f (λf.λx.f (n f x))) (λi.i) (λf.λx.x)) (\f.\x.f (f (f (f (f x)))))
λf.λx.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Making it better

data Expr = Var     VarName           -- variable
          | Apply   Expr Expr         -- application
          | BinOp   Expr Op Expr      -- built-in operator
          | If      Expr Expr Expr    -- if statement
          | Let     VarName Expr Expr -- let statement
          | Lambda  VarName Expr      -- function value
          | Number  Integer           -- integer value
          | Str     String            -- string value
          | Boolean Bool              -- boolean value
    deriving (Show, Eq, Ord)

data Op = Plus | Minus | Times | Divide 
        | Equals | NotEquals | LessThan | GreaterThan
        | Concat
    deriving (Show, Eq, Ord)

Some Improvements:

Before, only having vars, functions applications, and lambda functions made computing in λ-calculus difficult. Now, it's easier for us to do arithmetic or boolean logic.
Number, Str, and Boolean values improve readability in our execution of functions
We now have let expressions which let us clearly define substitutions let v = 6 in v → 6

Question from class? Why don't we add this superfluous functionality somewhere else? This implementation means that we lose out on the original abstraction of the original lambda calculus.

Issue with Let functionality when we are substituting a complicated expression such as 'Pig':
If we are using cbn rules, and the call let v = PIG in \v. blah v blah v blah v, then the entire PIG expression will be copied into each of the v values and we would eventually need to do the repetitive work of evaluating PIG 3 times.
If we are using cbv rules, and the call let v = PIG in \v. blah v blah v blah v, then (if PIG evaluated to 106) we would be passing 106 into each of the v values so we only need to evaluate PIG once in this case.

In our above Expr data type, String, Number, Boolean, and Lambda all can return as the result of a computation. There is nothing you can do to simplify them. We can use this to create a data type called Value to simplify Expr, which we have done below.

We've broken it into two parts Expr (for unevaluated expressions) and Value for results, and changed the type of cbn and cbv to Expr -> Value.

data Expr  = Var     VarName        -- variable
           | Apply   Expr Expr      -- application
           | BinOp   Expr Op Expr   -- built-in operator
           | Exactly Value          -- a value (doesn't need evaluation)
    deriving (Show, Eq, Ord)
    
data Value = Lambda VarName Expr    -- function value (closed function)
           | Number  Integer        -- numeric value
           | Str     String         -- string value
           | Boolean Bool           -- boolean value
    deriving (Show, Eq, Ord)

data Op = Plus | Minus | Times | Divide 
        | Equals | NotEquals | LessThan | GreaterThan
        | Concat
    deriving (Show, Eq, Ord)

Running the cbnInterpreter (or cbvInterpreter), we get:

cbnInterpreter 
cbn> λx.x
λx.x
cbn> (λx.x) (λy.y)
λy.y
cbn> 10
10
cbn> "Foo"
"Foo"
cbn> "Foo" == "Bar"
False
cbn> 1+1
2
cbn> 1+2
3
cbn> (λx.x) 1
1
cbn> (λx.x + 3) 1
4
cbn> (λy.λx.x + y) 7

Now we can write in our call-by-name interpreter

cbn> let y = λf.(λx.f (x x)) (λx.f (x x)) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact 6
720
cbn> (let y = λf.(λx.f (x x)) (λx.f (x x)) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact) 100
93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000
cbn> (let y = λf.(λx.f (x x)) (λx.f (x x)) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact)
λn.if n == 0 then 1 else n * (λx.(λfact.λn.if n == 0 then 1 else n * fact (n - 1)) (x x)) (λx.(λfact.λn.if n == 0 then 1 else n * fact (n - 1)) (x x)) (n - 1)

Note that (as we saw above) this Y combinator won't work with call-by-value:

cbv> let y = λf.(λx.f (x x)) (λx.f (x x)) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact 6
^C!! caught exception: user interrupt

But there is a Y combinator (known as Turing's Y Combinator that does work).

cbv> let y = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v))) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact 6
720
cbv> (let y = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v))) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact) 100
93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000
cbv> (let y = λf.(λx.f (λv.((x x) v))) (λx.f (λv.((x x) v))) in let fact = y (λfact.λn.if n == 0 then 1 else n * fact (n - 1)) in fact)
λn.if n == 0 then 1 else n * (λv.(λx.(λfact.λn.if n == 0 then 1 else n * fact (n - 1)) (λv.x x v)) (λx.(λfact.λn.if n == 0 then 1 else n * fact (n - 1)) (λv.x x v)) v) (n - 1)

Wiki Extra: Extending `substC`

Add to the cases of substC:

substC :: Expr -> VarName -> Expr -> Expr
substC e1 x e2 | Set.null (freeVars e2) = doSubst e1
               | otherwise              = error $ "Bad substitution: " ++ showExpr e2
  where
    doSubst var@(Var y)    | x == y    = e2
                           | otherwise = var
    doSubst fn@(Exactly (Lambda y eBody))
                           | x == y    = fn
                           | otherwise = Exactly (Lambda y (doSubst eBody))
    doSubst (Let y eDef eBody)
                           | x == y    = Let y eDef' eBody
                           | otherwise = Let y eDef' (doSubst eBody)
                where 
                    eDef' = doSubst eDef
    doSubst (Apply eFn eArg)           = Apply (doSubst eFn) (doSubst eArg)
    doSubst (BinOp eLHS op eRHS)       = BinOp (doSubst eLHS) op (doSubst eRHS)
    doSubst (If eCond eT eF)           = If (doSubst eCond) (doSubst eT)
                                                            (doSubst eF)
    doSubst other                      = other

Revised code for `cbv`

Our code for evaluation is now

cbv :: Expr -> Value
cbv (Var v)          = error ("Unsubstituted variable: " ++ v)
cbv (Exactly val)    = val
cbv (Apply eFn eArg) = 
      let vFn  = cbv eFn
          vArg = cbv eArg
      in case vFn of
             Lambda v eBody ->  cbv (substC eBody v vArg)
             _              ->  error "Can't apply a non-function"
cbv (BinOp eLHS op eRHS) = evalOp (cbv eLHS) op (cbv eRHS)
cbv (If eCond eT eF)     = if toBool (cbv eCond) then cbv eT else cbv eF
cbv (Let v eDef eBody)   = cbv (Apply (Exactly (Lambda v eBody)) eDef)

Recall that let v = DEF in LETBODY is just syntactic sugar for the lambda expression (λv.LETBODY) DEF, which is why we can simply use Lambda (etc.) in cbv for the Let case. The motivation for "de-sugaring" is twofold - (1), code reuse and (2) to avoid rewriting eval for all of the necessary cases.

All the code we saw running in when we were motiving extending the our interpreter now works.

The code above uses two helper functions

toBool :: Value -> Bool
evalOp :: Value -> Op -> Value -> Value

Wiki Extra: Helper functions

`toBool` convert a `Value` to a `Bool`

toBool (Boolean b)  = b
toBool (Number  n)  = n /= 0
toBool (Str     s)  = s /= ""
toBool (Lambda _ _) = error "Can't use a function as a Boolean"

evalOp evaluate a binary operator

{-- Evaluation for built-in operators --}

evalOp :: Value -> Op -> Value -> Value

-- error out for operands of different types (neat use of a complex guard!)

evalOp lhs op rhs | misMatchedTypes =
    error ("Mismatched types to " ++ show op ++ " operator")
  where misMatchedTypes = case (lhs, rhs) of
                              (Boolean _,  Boolean _)   -> False
                              (Number  _,  Number  _)   -> False
                              (Str     _,  Str     _)   -> False
                              (Lambda _ _, Lambda _ _)  -> False
                              _                         -> True

-- evaluation for function operations & operands (none)

evalOp (Lambda _ _) op (Lambda _ _) = 
    error ("No implementation of " ++ show op ++ " for functions")

-- evaluation of comparison operators for everything (except functions)

evalOp lhs Equals      rhs = Boolean (lhs == rhs)                -- a = b
evalOp lhs NotEquals   rhs = Boolean (lhs /= rhs)                -- a ≠ b
evalOp lhs LessThan    rhs = Boolean (lhs < rhs)                 -- a < b
evalOp lhs GreaterThan rhs = Boolean (lhs > rhs)                 -- a > b

-- evaluation for boolean operations & operands (nothing beyond comparison ops)

evalOp (Boolean _) op (Boolean _) = 
    error ("No implementation of " ++ show op ++ " for booleans")

-- evaluation for numeric operations & operands	(beyond comparison ops)

evalOp (Number lhs) Plus   (Number rhs) = Number (lhs + rhs)     -- a + b
evalOp (Number lhs) Minus  (Number rhs) = Number (lhs - rhs)     -- a - b
evalOp (Number lhs) Times  (Number rhs) = Number (lhs * rhs)     -- a * b
evalOp (Number lhs) Divide (Number rhs) = Number (lhs `div` rhs) -- a / b
evalOp (Number _)   op     (Number _) =
    error ("No implementation of " ++ show op ++ " for numbers")

-- evaluation for string operations & operands (beyond comparison ops)

evalOp (Str lhs) Concat (Str rhs) = Str (lhs ++ rhs)             -- a · b
evalOp (Str lhs) op     (Str rhs) =
    error ("No implementation of " ++ show op ++ " for strings")

Performance Issue (Trouble in Paradise part 1)

Consider this for next time...

let x1 = 1
in let x2 = 2
   in let x3 = 3 in
       ...
         in let xn = n
            in x1+x2+x3+ ... +xn

If you want to print this page, you can click to show all the answers.

-- MelissaONeill - 12 Feb 2020

CS131Spring2020

CS Webs
Main
QRefs
History

Current Courses

TWiki Webs
Sandbox
TWiki

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback