λ-Calculus + Types + Syntactic Sugar + Lazy Evaluation = Haskell

Meaning of One Simple Lambda Expression...

What does this mean?

    (λa.(λb.b))

Based on what we've learned so far, this can be

• False
• the constant identity function
• 0 (as a Church numeral)
• Nothing
• Nil
• Leaf

We don't know what it means without some extra information telling us what it is supposed to mean (i.e., what the type is).

Mistakes Happen...

What happens if you make a mistake writing in the lambda calculus...?

Reduction, without mistakes

lc> ((Plus 4) 4)
((Plus 4) 4)

After 0 β-reductions:

    ((Plus 4) 4)
  == (by definition)
    (((λn.(λm.(λf.(λb.((n f) ((m f) b)))))) 4) 4)


After 0 β-reductions:

    (((λn.(λm.(λf.(λb.((n f) ((m f) b)))))) 4) 4)
  →ᵦ
    ((λm.(λf.(λb.((4 f) ((m f) b))))) 4)


After 1 β-reductions:

    ((λm.(λf.(λb.((4 f) ((m f) b))))) 4)
  →ᵦ
    (λf.(λb.((4 f) ((4 f) b))))


After 2 β-reductions:

    (λf.(λb.((4 f) ((4 f) b))))
  == (by definition)
    (λf.(λb.(((λf.(λb.(f (f (f (f b)))))) f) ((4 f) b))))


After 2 β-reductions:

    (λf.(λb.(((λf.(λb.(f (f (f (f b)))))) f) ((4 f) b))))
  →ᵦ
    (λf.(λb.((λb'.(f (f (f (f b'))))) ((4 f) b))))


After 3 β-reductions:

    (λf.(λb.((λb'.(f (f (f (f b'))))) ((4 f) b))))
  →ᵦ
    (λf.(λb.(f (f (f (f ((4 f) b)))))))


After 4 β-reductions:

    (λf.(λb.(f (f (f (f ((4 f) b)))))))
  == (by definition)
    (λf.(λb.(f (f (f (f (((λf.(λb.(f (f (f (f b)))))) f) b)))))))


After 4 β-reductions:

    (λf.(λb.(f (f (f (f (((λf.(λb.(f (f (f (f b)))))) f) b)))))))
  →ᵦ
    (λf.(λb.(f (f (f (f ((λb'.(f (f (f (f b'))))) b)))))))


After 5 β-reductions:

    (λf.(λb.(f (f (f (f ((λb'.(f (f (f (f b'))))) b)))))))
  →ᵦ
    (λf.(λb.(f (f (f (f (f (f (f (f b))))))))))

(λf.(λb.(f (f (f (f (f (f (f (f b))))))))))

6 total steps

If we made a mistake...

lc> (Plus (4 4))
(Plus (4 4))

After 0 β-reductions:

    (Plus (4 4))
  == (by definition)
    ((λn.(λm.(λf.(λb.((n f) ((m f) b)))))) (4 4))


After 0 β-reductions:

    ((λn.(λm.(λf.(λb.((n f) ((m f) b)))))) (4 4))
  →ᵦ
    (λm.(λf.(λb.(((4 4) f) ((m f) b)))))


After 1 β-reductions:

    (λm.(λf.(λb.(((4 4) f) ((m f) b)))))
  == (by definition)
    (λm.(λf.(λb.((((λf.(λb.(f (f (f (f b)))))) 4) f) ((m f) b)))))


After 1 β-reductions:

    (λm.(λf.(λb.((((λf.(λb.(f (f (f (f b)))))) 4) f) ((m f) b)))))
  →ᵦ
    (λm.(λf.(λb.(((λb'.(4 (4 (4 (4 b'))))) f) ((m f) b)))))

[...]

After 172 β-reductions:

    (λm.(λf.(λb.(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 (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 (f (f (f (f (f (f (f (f (f (f (f (f ((λb'.(f (f (f (f b'))))) ((m f) b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  →ᵦ
    (λm.(λf.(λb.(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 (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 (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f ((m f) b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(λm.(λf.(λb.(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 (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 (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f ((m f) b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

173 total steps

If we had types!

The results of the correct code could look more like numbers or lists (i.e., we'd display results better).

lc> (Plus (1 1))
Error: Attempt to apply 1 (an Integer) to an argument!

Here it would realize that something will be applied to 1, and if we want 1 to only function as an integer, we can't allow that! Also, as cool as it is to be able to encode numbers as Church numerals in the lambda calculus (i.e., as functions), maybe it'd be more efficient just to have primitive types for numbers, because then arithmetic could be much more efficient. Types would make that possible. The system could know when it had numbers and when it had functions.

Syntactic Sugar

Syntactic sugar doesn't necessarily add any additional expressive power to a language (i.e., we can't compute things we couldn't compute before, we can code exactly the same algorithms using the same techniques), but it's something that we (as human beings) find much nicer and easier to understand. Examples of syntactic sugar we would like lambda calculus to have:

• Implicit parentheses
• Infix operators (e.g. + used between two operands)
• Better ways to handle cases (e.g. pattern matching, let expressions, etc)
• Conditional statements
• Better function declarations (e.g. using variables, using recursion, etc)

Infix operators

Do you like saying

    ((Plus ((Times 3) n)) 1)

What would you rather say?

    Plus (Times 3 n) 1

and have lc automatically put in the parenthesis to make the previous expression? (you can actually achieve this in lc with :set parens off)

Better yet, wouldn't you rather mean ((Plus ((Times 3) n)) 1) by just saying

  3 * n + 1

Let Expressions

Can you figure out how to turn

let x = Times 3 7
in  Plus x x 

Into the lambda calculus?

(λ x.Plus x x) (Times 3 7)

Generalizing, we see that for a let expression of the following form:

    let VAR = VALUE
    in BODY

The expression can be translated into lambda calculus as:

(λ VAR.BODY) VALUE

We can also express a destructuring let in this way.

Can you figure out how to turn

let (x, y) = NextStep p
in  Pair (Plus x 1) (Pred y)

Into the lambda calculus?

(NextStep p) (λx.λy.Pair (Plus x 1) (Pred y))

Generalizing, we see that for a destructuring let expression of the following form:

    let (VAR1, VAR2) = PAIR
    in BODY

The expression can be translated into lambda calculus as:

PAIR (λVAR1.λVAR2.BODY)

Wiki Extra: Conditional Syntax

It would be nicer to have the sugared syntax

if EXP1
then EXP2
else EXP3

We can easily transform this into basic lambda calculus by using the fact that booleans will operate as built-in if statements.

 ((EXP1 EXP2) EXP3) 

(Also, as cool is it is to be able to encode booleans in the lambda calculus as functions, maybe it'd be more efficient just to have primitive values for bools.)

Function Names with Arguments

Wouldn't it be nice to have

  And p q = p q False

Instead of

  And = (\p. (\q. ((p q) False)))

The ability to list the arguments next to the function name lets us clearly see the difference between the arguments and the results.

Recursion

Do you like saying

    Fact = (Y (\f.(\n.((((Equal n) 0) 1) ((Times n) (f ((Monus n) 1)))))))

Wouldn't it be nicer to say

    Fact = \n.((((Equal n) 0) 1) ((Times n) (Fact ((Monus n) 1)))))))

or better yet

    fact n = if n == 0 then 1 
                       else n * fact (n - 1)

Simple Patterns

In class, we turned the following

let s = ((Plus a) b)
  in ((Plus s) s)

into the lambda calculus below:

  ((\s. ((Plus s) s)) ((Plus a) b))

Here's another example. We turned the following

let (h,t) = (HeadAndTail l)
  in ((Cons (f h)) t)

into the lambda calculus below:

  ((HeadAndTail l) (\h. (\t. (Cons (f h) t))))

Can you figure out how to turn

let (x,y) = Pair 40 2
in  x+y

Into the lambda calculus? Remember that Pair 40 2 reduces to λb.b 40 20 .

Sure, we could write:

let x = (Fst ((Pair 40) 2))
in let y = (Snd ((Pair 40) 2))
in x+y

but that doesn't capitalize on the what we know about the structure of pairs as we chose to encode them. So what's a better way? Hint: remember that a pair of 40 and 2 is essentially just:

 (\b.((b 40) 2)) 

(Pair 40 2) Plus
  →ᵦ
Plus 40 2

More Efficient...?

Consider evaluating this expression.

    (\s.(Pair s s)) (Plus 1 1)

Let's look at the pieces...

lc> (\s.(Pair s s)) 2

After 0 β-reductions:

    (λs.Pair s s) 2
  →ᵦ
    Pair 2 2


After 1 β-reductions:

    Pair 2 2
  == (by definition)
    (λx.λy.λb.b x y) 2 2


After 1 β-reductions:

    (λx.λy.λb.b x y) 2 2
  →ᵦ
    (λy.λb.b 2 y) 2


After 2 β-reductions:

    (λy.λb.b 2 y) 2
  →ᵦ
    λb.b 2 2


3 total steps

and

lc> (Plus 1 1)

After 0 β-reductions:

    Plus 1 1
  == (by definition)
    (λn.λm.λf.λx.n f (m f x)) 1 1


After 0 β-reductions:

    (λn.λm.λf.λx.n f (m f x)) 1 1
  →ᵦ
    (λm.λf.λx.1 f (m f x)) 1


After 1 β-reductions:

    (λm.λf.λx.1 f (m f x)) 1
  →ᵦ
    λf.λx.1 f (1 f x)


After 2 β-reductions:

    λf.λx.1 f (1 f x)
  == (by definition)
    λf.λx.(λf.λb.f b) f (1 f x)


After 2 β-reductions:

    λf.λx.(λf.λb.f b) f (1 f x)
  →ᵦ
    λf.λx.(λb.f b) (1 f x)


After 3 β-reductions:

    λf.λx.(λb.f b) (1 f x)
  →ᵦ
    λf.λx.f (1 f x)


After 4 β-reductions:

    λf.λx.f (1 f x)
  == (by definition)
    λf.λx.f ((λf.λb.f b) f x)


After 4 β-reductions:

    λf.λx.f ((λf.λb.f b) f x)
  →ᵦ
    λf.λx.f ((λb.f b) x)


After 5 β-reductions:

    λf.λx.f ((λb.f b) x)
  →ᵦ
    λf.λx.f (f x)


6 total steps

You might thing it'll take only 6+3 = 9 steps, but actually it requires 3+6+6 = 15 steps.

lc> (\s.(Pair s s)) (Plus 1 1)

After 0 β-reductions:

    (λs.Pair s s) (Plus 1 1)
  →ᵦ
    Pair (Plus 1 1) (Plus 1 1)


After 1 β-reductions:

    Pair (Plus 1 1) (Plus 1 1)
  == (by definition)
    (λx.λy.λb.b x y) (Plus 1 1) (Plus 1 1)


After 1 β-reductions:

    (λx.λy.λb.b x y) (Plus 1 1) (Plus 1 1)
  →ᵦ
    (λy.λb.b (Plus 1 1) y) (Plus 1 1)


After 2 β-reductions:

    (λy.λb.b (Plus 1 1) y) (Plus 1 1)
  →ᵦ
    λb.b (Plus 1 1) (Plus 1 1)


After 3 β-reductions:

    λb.b (Plus 1 1) (b (Plus 1 1))
  == (by definition)
    λb.b ((λn.λm.λf.λx.n f (m f x)) 1 1) (b (Plus 1 1))


After 3 β-reductions:

    λb.b ((λn.λm.λf.λx.n f (m f x)) 1 1) (b (Plus 1 1))
  →ᵦ
    λb.b ((λm.λf.λx.1 f (m f x)) 1) (b (Plus 1 1))


After 4 β-reductions:

    λb.b ((λm.λf.λx.1 f (m f x)) 1) (b (Plus 1 1))
  →ᵦ
    λb.b (λf.λx.1 f (1 f x)) (b (Plus 1 1))


After 5 β-reductions:

    λb.b (λf.λx.1 f (1 f x)) (b (Plus 1 1))
  == (by definition)
    λb.b (λf.λx.(λf.λb.f b) f (1 f x)) (b (Plus 1 1))


After 5 β-reductions:

    λb.b (λf.λx.(λf.λb.f b) f (1 f x)) (b (Plus 1 1))
  →ᵦ
    λb.b (λf.λx.(λb'.f b') (1 f x)) (b (Plus 1 1))


After 6 β-reductions:

    λb.b (λf.λx.(λb'.f b') (1 f x)) (b (Plus 1 1))
  →ᵦ
    λb.b (λf.λx.f (1 f x)) (b (Plus 1 1))


After 7 β-reductions:

    λb.b (λf.λx.f (1 f x)) (b (Plus 1 1))
  == (by definition)
    λb.b (λf.λx.f ((λf.λb.f b) f x)) (b (Plus 1 1))


After 7 β-reductions:

    λb.b (λf.λx.f ((λf.λb.f b) f x)) (b (Plus 1 1))
  →ᵦ
    λb.b (λf.λx.f ((λb'.f b') x)) (b (Plus 1 1))


After 8 β-reductions:

    λb.b (λf.λx.f ((λb'.f b') x)) (b (Plus 1 1))
  →ᵦ
    λb.b (λf.λx.f (f x)) (b (Plus 1 1))


After 9 β-reductions:

    λb.b (λf.λx.f (f x)) (Plus 1 1)
  →ᵦ ... →ᵦ  (by 2 steps already seen above)
    λb.b (λf.λx.f (f x)) λf.λx.1 f (1 f x)


After 11 β-reductions:

    λb.b (λf.λx.f (f x)) λf.λx.1 f (1 f x)
  →ᵦ ... →ᵦ  (by 2 steps already seen above)
    λb.b (λf.λx.f (f x)) λf.λx.f (1 f x)


After 13 β-reductions:

    λb.b (λf.λx.f (f x)) λf.λx.f (1 f x)
  →ᵦ ... →ᵦ  (by 2 steps already seen above)
    λb.b (λf.λx.f (f x)) λf.λx.f (f x)


15 total steps

Ideally, we wouldn't have to evaluate the same thing twice. If we delayed evaluating something until we needed it, we won't have to do extra work.

What We Want...

We'd like

• Types
  • Catch more errors!
  • Allow multiple kinds of value (escape from “everything is always a function”)
  • Provide type inference where possible, so we don't say what the types are.
• Nice syntax (that reduces to our simple core) -- Syntactic sugar and pattern patching
• Efficiency
  • Outermost reduction with sharing (a.k.a. graph reduction), also known as lazy evaluation
  • Built-in types instead of encodings (actual numbers, booleans, efficient pairs, etc.)

That's Haskell!

Tour of Haskell

Much of this material echoes what students saw in the videos.

Laziness

Prelude> billions = [1..10000000000]
Prelude> take 10 billions
Prelude> forever = [1..]
Prelude> take 10 forever
[1,2,3,4,5,6,7,8,9,10]
Prelude> ones = [1,1..]
Prelude> odds = [1,3..]
Prelude> take 10 ones
[1,1,1,1,1,1,1,1,1,1]
Prelude> take 10 odds
[1,3,5,7,9,11,13,15,17,19]

Prelude> x = head []
Prelude> y = (x,x,x)
Prelude> z = [y,y,y,y,y]
Prelude> z
[(*** Exception: Prelude.head: empty list

Syntactic Sugar

Implicit parentheses

Prelude> take 10 odds
[1,3,5,7,9,11,13,15,17,19]
Prelude> (take 10) odds
[1,3,5,7,9,11,13,15,17,19]
Prelude> ((take 10) odds)

If we wanted, we could define all our recursive functions and infinite list with the Y combinator.

Prelude> ones = [1,1..]
Prelude> take 10 ones
[1,1,1,1,1,1,1,1,1,1]
Prelude> ones = 1 : ones
Prelude> take 10 ones
[1,1,1,1,1,1,1,1,1,1]
Prelude> ycomb f = f (ycomb f)
Prelude> ones = ycomb (\list -> 1 : list)
Prelude> take 10 ones
[1,1,1,1,1,1,1,1,1,1]

Examples of defining functions and using infix operators. Note that these definitions are equivalent functions.

Prelude> calc n m = 3 * n + m
Prelude> calc 4 1
13
Prelude> (calc 4) 1
13
Prelude> c4 = calc 4
Prelude> c4 1
13
Prelude> calc = \n -> \m -> 3 * n + 1
Prelude> calc 4 1
13
Prelude> calc = \n -> \m -> (((+) (((*) 3) n)) 1)
Prelude> calc 4 1
13
Prelude> calc n = \m -> 3 * n + 1
Prelude> calc 4 1

Rather than Cons and Nil, we have an infix operator : and [].

Prelude> []
[]
Prelude> 1 : (2 : (3 : (4 : [])))
[1,2,3,4]
Prelude> 1 : 2 : 3 : 4 : []
[1,2,3,4]
Prelude> 1 : [2,3,4]
[1,2,3,4]
Prelude> [1,2,3,4]
[1,2,3,4]
Prelude> 'a' : 'b' : 'c' : 'd' : []
"abcd"

Types

Every value has a type. By extension, all Haskell functions take in an input of a definite type and return an output of a definite type.

Prelude> :t "Hello"
"Hello" :: [Char]
Prelude> :t reverse
reverse :: [a] -> [a]
Prelude> reverse "Hello"
"olleH"
Prelude> :t reverse "Hello"
reverse "Hello" :: [Char]

Type errors can be helpful in catching mistakes.

Prelude> 'a' : 'b'

:18:7: error:
    • Couldn't match expected type ‘[Char]’ with actual type ‘Char’
    • In the second argument of ‘(:)’, namely ‘'b'’
      In the expression: 'a' : 'b'
      In an equation for ‘it’: it = 'a' : 'b'

Some types are built-in:

Prelude> 7==3
False
Prelude> :t 7==3
7==3 :: Bool

You can define your own types. Here, we define the Fuzzy type that has three possible values: Yes, Maybe, and No:

Prelude> data Fuzzy = Yes | Maybe | No
Prelude> x = Yes
Prelude> :{
Prelude| test Yes = 1.0
Prelude| test Maybe = 0.5
Prelude| test No = 0.0
Prelude| :}
Prelude> test Yes
1.0

Note: If we ask the interpreter what the type test is, we expect

test :: Fuzzy -> Double

but we actually get:

Prelude> :t test
test :: Fractional p => Fuzzy -> p

Pattern Matching

Prelude> mypair = (40,2)
Prelude> let (x,y) = mypair in x+y
42

Prelude> :{
Prelude| len [] = 0
Prelude| len (h : t) = 1 + (len t)
Prelude| :}
Prelude> len (1 : (2 : (3 : (4 : []))))
4
Prelude> len [1,2,3,4,5,6,7]
7
Prelude> len [2.3,3.1]
2
Prelude> len ["foo","bar"]
2
Prelude> len "Hello World"
11
Prelude> :t len
len :: [a] -> Integer

len works on any kind of list.

Actually, that type above is a lie, the type of len is (by default, without us providing a more restrictive type signature) is

• len :: Num n => [a] -> n

In English, we can read it as “for any numeric type, n, and any arbitrary type a, len will take a list of items of type a and return a number of type n.

What About Variable Modification?

This doesn't actually exist in Haskell. By default, variables are immutable, and an attempt to directly change a variable's originally declared value wouldn't compile, but if you were to enable multiple declarations of variables and write the following code:

n = 2
n = 40

The variable n would not actually change in memory. Instead, the second n is allocated somewhere else in memory and the first n is completely disregarded... unless the first n was used in a function definition:

n = 40
addSomething x = x + n
n = 2

Here, addSomething 2 would return 42, and not 4.

Useful Facilities

Prelude> :t map
map :: (a -> b) -> [a] -> [b]
Prelude> inc x = 1 + x
Prelude> inclist = map inc
Prelude> :t inc
inc :: Num a => a -> a
Prelude> :t inclist
inclist :: Num b => [b] -> [b]
Prelude> inclist [1,2,3,4]
[2,3,4,5]
Prelude> map inc [17,18]
[18,19]
Prelude> ((map inc) [17,18])
[18,19]
Prelude> ((map show) [17,18])
["17","18"]
Prelude> inc x = 1 + x
Prelude> inc x = (((+) 1) x)
Prelude> inc = ((+) 1)
Prelude> inc = (+) 1

-- MelissaONeill - 04 Feb 2020