Programming a language

Nicolas Rinaudo • @NicolasRinaudo@functional.cafe

1 / 703

Representing code2 / 703

3 / 703

1 + 2

4 / 703

enum Expr:

1 + 2

5 / 703

enum Expr:
  case Num()

1 + 2

6 / 703

enum Expr:
  case Num(value: Int)

1 + 2

7 / 703

enum Expr:
  case Num(value: Int)
  case Add()

1 + 2

8 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Num)

1 + 2

9 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Num, rhs: Num)

1 + 2

10 / 703

Num value ⇓ ???

1 + 2

11 / 703

Num value ⇓ ???

1 + 2

12 / 703

Num value ⇓ ???

1 + 2

13 / 703

Num value ⇓ value

1 + 2

14 / 703

Add lhs rhs ⇓ ???

1 + 2

15 / 703

Add lhs rhs ⇓ ???

1 + 2

16 / 703

Add lhs rhs ⇓ lhs + rhs

1 + 2

17 / 703

Add lhs rhs ⇓ lhs + rhs

1 + 2

18 / 703

lhs ⇓ v₁
Add lhs rhs ⇓ lhs + rhs

1 + 2

19 / 703

lhs ⇓ v₁      rhs ⇓ v₂
Add lhs rhs ⇓ lhs + rhs

1 + 2

20 / 703

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ lhs + rhs

1 + 2

21 / 703

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ lhs + rhs

1 + 2

22 / 703

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

1 + 2

23 / 703

def interpret(expr: Expr): ??? =

24 / 703

def interpret(expr: Expr): ??? =

25 / 703

def interpret(expr: Expr): ??? =
​
​
​
​

26 / 703

def interpret(expr: Expr): Int =
​
​
​
​

27 / 703

def interpret(expr: Expr): Int = expr match
​
​
​
​

28 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)    =>


Num value ⇓ value

29 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)    => value


Num value ⇓ value

30 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)    => value
  case Add(lhs, rhs) =>

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

31 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)    => value
  case Add(lhs, rhs) => add(lhs, rhs)

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

32 / 703

def add(lhs: Num, rhs: Num) =

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

33 / 703

def add(lhs: Num, rhs: Num) =
  val v1 = interpret(lhs)

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

34 / 703

def add(lhs: Num, rhs: Num) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

35 / 703

def add(lhs: Num, rhs: Num) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

36 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

37 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

38 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

39 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

40 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)
// val res0: Int = 3

41 / 703

(1 + 2)

val expr = Add(Num(1), Num(2))

interpret(expr)
// val res0: Int = 3

42 / 703

((1)     +       ((2)))

val expr = Add(Num(1), Num(2))

interpret(expr)
// val res0: Int = 3

43 / 703

1 + 2

44 / 703

1 + 2

45 / 703

1 + 2

46 / 703

1 + 2

47 / 703

1 + (2 + 3)

48 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Num, rhs: Num)

49 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)

50 / 703

def add(lhs: Num, rhs: Num) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

51 / 703

def add(lhs: Num, rhs: Num) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

52 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

53 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

54 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

55 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

56 / 703

1 + 2

val expr = Add(Num(1), Num(2))

interpret(expr)

57 / 703

1 + (2 + 3)

val expr = Add(Num(1), Add(Num(2), Num(3)))

interpret(expr)

58 / 703

1 + (2 + 3)

val expr = Add(Num(1), Add(Num(2), Num(3)))

interpret(expr)
// val res1: Int = 6

59 / 703

Key takeaways

60 / 703

Key takeaways

Source code is represented as a recursive sum type

61 / 703

Key takeaways

Source code is represented as a recursive sum type
This is called an AST

62 / 703

Key takeaways

Source code is represented as a recursive sum type
This is called an AST
Interpretation is done through pattern matching

63 / 703

Taking decisions64 / 703

if true then 1 + 2
        else 3 + 4

65 / 703

if true then 1 + 2
        else 3 + 4

66 / 703

if true then 1 + 2
        else 3 + 4

67 / 703

if true then 1 + 2
        else 3 + 4

68 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond ⇓ ???

if true then 1 + 2
        else 3 + 4

69 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred ⇓ ???

if true then 1 + 2
        else 3 + 4

70 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT ⇓ ???

if true then 1 + 2
        else 3 + 4

71 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

72 / 703

pred ⇓ ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

73 / 703

pred ⇓ ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

74 / 703

pred ⇓ true
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

75 / 703

pred ⇓ true
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

76 / 703

pred ⇓ true
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

77 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

78 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

79 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

80 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

81 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

82 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ ???

if true then 1 + 2
        else 3 + 4

83 / 703

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

if true then 1 + 2
        else 3 + 4

84 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

85 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)
  case Cond()

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

86 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

87 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

88 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

89 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

90 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

91 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

92 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

93 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

94 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

95 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

96 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) != 0 then interpret(onT)
  else                         interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

97 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) != 0 then interpret(onT)
  else                         interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

98 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

99 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

100 / 703

enum Value:

101 / 703

enum Value:
  case Num(value: Int)
​
​
​
​

102 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
​
​
​

103 / 703

def interpret(expr: Expr): Int = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)
​
​

104 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)
​
​

105 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)


Num value ⇓ value

106 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => value
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)
​
​

​
​
Num value ⇓ value
​
​
​
​

107 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => Value.Num(value)
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)
​
​

​
​
Num value ⇓ Value.Num value
​
​
​
​

108 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

109 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ v₁      rhs ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Add lhs rhs ⇓ v₁ + v₂

110 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        Add lhs rhs ⇓ v₁ + v₂

111 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        Add lhs rhs ⇓ v₁ + v₂

112 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

113 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

114 / 703

def add(lhs: Expr, rhs: Expr) =
  val v1 = interpret(lhs)
  val v2 = interpret(rhs)
  v1 + v2

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

115 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) =>

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

116 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) =>

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

117 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) =>

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

118 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Num(v1 + v2)

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

119 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Num(v1 + v2)
    case _                              =>

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

120 / 703

def add(lhs: Expr, rhs: Expr) =
  (interpret(lhs), interpret(rhs)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Num(v1 + v2)
    case _                              => typeError("add")

lhs ⇓ Value.Num v₁      rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Add lhs rhs ⇓ Value.Num (v₁ + v₂)

121 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v
pred ⇓ false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
  Cond pred onT onF ⇓ v

122 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

123 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

124 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

125 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  if interpret(pred) then interpret(onT)
  else                    interpret(onF)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

126 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

127 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  =>

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

128 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  => interpret(onT)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

129 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  => interpret(onT)
    case Value.Bool(false) =>

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

130 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  => interpret(onT)
    case Value.Bool(false) => interpret(onF)

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

131 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  => interpret(onT)
    case Value.Bool(false) => interpret(onF)
    case _                 =>

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

132 / 703

def cond(pred: Expr, onT: Expr, onF: Expr) =
  interpret(pred) match
    case Value.Bool(true)  => interpret(onT)
    case Value.Bool(false) => interpret(onF)
    case _                 => typeError("cond")

pred ⇓ Value.Bool true        onT ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v
pred ⇓ Value.Bool false       onF ⇓ v
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
       Cond pred onT onF ⇓ v

133 / 703

if true then 1
        else 2

134 / 703

if true then 1
        else 2

135 / 703

if true then 1
        else 2


Bool ⇓ ???

136 / 703

if true then 1
        else 2


Bool value ⇓ ???

137 / 703

if true then 1
        else 2


Bool value ⇓ ???

138 / 703

if true then 1
        else 2


Bool value ⇓ Value.Bool value

139 / 703

enum Expr:
  case Num(value: Int)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)


Bool value ⇓ Value.Bool value

140 / 703

enum Expr:
  case Num(value: Int)
  case Bool()
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)


Bool value ⇓ Value.Bool value

141 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)


Bool value ⇓ Value.Bool value

142 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => Value.Num(value)
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)


Bool value ⇓ Value.Bool value

143 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => Value.Num(value)
  case Bool(value)          =>
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)


Bool value ⇓ Value.Bool value

144 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)           => Value.Num(value)
  case Bool(value)          => Value.Bool(value)
  case Add(lhs, rhs)        => add(lhs, rhs)
  case Cond(pred, onT, onF) => cond(pred, onT, onF)


Bool value ⇓ Value.Bool value

145 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)

146 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)

147 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)

148 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)

149 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)

150 / 703

if true then 1
        else 2

val expr = Cond(
  pred = Bool(true),
  onT  = Num(1),
  onF  = Num(2)
)

interpret(expr)
// val res2: Value = Num(1)

151 / 703

Key takeaways

152 / 703

Key takeaways

Conditionals are straightforward to support

153 / 703

Key takeaways

Conditionals are straightforward to support
They forced us to support multiple types of values

154 / 703

Key takeaways

Conditionals are straightforward to support
They forced us to support multiple types of values
Friends don't let friends implement truthiness

155 / 703

Naming things156 / 703

let x = 1
x

157 / 703

let x = 1
x

158 / 703

x
let x = 1

159 / 703

let x = 1 in
  x + 2

160 / 703

let x = 1 in
  x + 2

161 / 703

x = 1

let x = 1 in
  x + 2

162 / 703

x = 1

let x = 1 in
  x + 2

163 / 703

x = 1

let x = 1 in
  x + 2

164 / 703

x = 1

let x = 1 in
  1 + 2

165 / 703

x = 1

let x = 1 in
  1 + 2

166 / 703

x = 1

let x = 1 in
  3

167 / 703

x = 1

let x = 1 in
  3

168 / 703

x = 1

169 / 703

let x = 1 + 2 in
  if true then 1
  else         x

170 / 703

let x = 1 + 2 in
  if true then 1
  else         x

171 / 703

let x = 1 + 2 in
  if true then 1
  else         x

172 / 703

let x = 1 + 2 in
  if true then 1
  else         x

173 / 703

let x = 1 + 2 in
  if true then 1
  else         x

174 / 703

let x = 1 + 2 in
  if true then 1
  else         x

175 / 703

let x = 3 in
  if true then 1
  else         x

176 / 703

let x = 3 in
  if true then 1
  else         x

177 / 703

x = 3

let x = 3 in
  if true then 1
  else         x

178 / 703

let x = 1 in
  x + (let x = 2 in x)

179 / 703

let x = 1 in
  x + (let x = 2 in x)

180 / 703

let x = 1 in
  x + (let x = 2 in x)

181 / 703

let x = 1 in
  x + (let x = 2 in x)

182 / 703

let x = 1 in
  x + (let x = 2 in x)

183 / 703

let x = 1 in
  x + (let x = 2 in x)

184 / 703

let x = 1 in
  (let x = 2 in x) + x

185 / 703

let x = 1 in
  (let x = 2 in x) + x

186 / 703

x = 1

let x = 1 in
  (let x = 2 in x) + x

187 / 703

x = 1

let x = 1 in
  (let x = 2 in x) + x

188 / 703

x = 1

let x = 1 in
  (let x = 2 in x) + x

189 / 703

x = 2

let x = 1 in
  (let x = 2 in x) + x

190 / 703

x = 2

let x = 1 in
  (let x = 2 in x) + x

191 / 703

x = 2

let x = 1 in
  (let x = 2 in 2) + x

192 / 703

x = 2

let x = 1 in
  (let x = 2 in 2) + x

193 / 703

x = 2

let x = 1 in
  2 + x

194 / 703

x = 2

let x = 1 in
  2 + x

195 / 703

x = 2

let x = 1 in
  2 + 2

196 / 703

x = 2

let x = 1 in
  2 + 2

197 / 703

x = 2

let x = 1 in
  4

198 / 703

x = 1

let x = 1 in
  (let x = 2 in x) + x

199 / 703

x = 1
x = 2

let x = 1 in
  (let x = 2 in x) + x

200 / 703

x = 1
x = 2

let x = 1 in
  (let x = 2 in x) + x

201 / 703

x = 1
x = 2

let x = 1 in
  (let x = 2 in 2) + x

202 / 703

x = 1
​x = 2

let x = 1 in
  (let x = 2 in 2) + x
​

203 / 703

x = 1

let x = 1 in
  2 + x

204 / 703

x = 1

let x = 1 in
  2 + x

205 / 703

x = 1

let x = 1 in
  2 + 1

206 / 703

x = 1

let x = 1 in
  2 + 1

207 / 703

x = 1

let x = 1 in
  3

208 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let ⇓ ???

let x = 1 in
  x + 2

209 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name ⇓ ???

let x = 1 in
  x + 2

210 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name value ⇓ ???

let x = 1 in
  x + 2

211 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name value body ⇓ ???

let x = 1 in
  x + 2

212 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name value body ⇓ ???

let x = 1 in
  x + 2

213 / 703

value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name value body ⇓ ???

let x = 1 in
  x + 2

214 / 703

value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
            Let name value body ⇓ ???

let x = 1 in
  x + 2

215 / 703

e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

216 / 703

e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

217 / 703

e |- value ⇓ v₁                    ??? |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

218 / 703

e |- value ⇓ v₁                    ??? |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

219 / 703

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

220 / 703

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ ???

let x = 1 in
  x + 2

221 / 703

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ v₂

let x = 1 in
  x + 2

222 / 703

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ v₂

let x = 1 in
  x + 2

223 / 703

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
          e |- Let name value body ⇓ v₂

let x = 1 in
  x + 2

224 / 703


e |- Ref ⇓ ???

let x = 1 in
  x + 2

225 / 703


e |- Ref name ⇓ ???

let x = 1 in
  x + 2

226 / 703


e |- Ref name ⇓ ???

let x = 1 in
  x + 2

227 / 703


e |- Ref name ⇓ e(name)

let x = 1 in
  x + 2

228 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

229 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let()

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

230 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

231 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

232 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

233 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)


e |- Ref name ⇓ e(name)

234 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref()


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
e |- Ref name ⇓ e(name)

235 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)


e |- Ref name ⇓ e(name)

236 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)


e |- Ref name ⇓ e(name)

237 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)


e |- Ref name ⇓ e(name)

238 / 703

case class Env():

239 / 703

case class Env(env: List[Env.Binding]):

240 / 703

case class Env(env: List[Env.Binding]):
object Env:
  case class Binding()

241 / 703

case class Env(env: List[Env.Binding]):
object Env:
  case class Binding(name: String)

242 / 703

case class Env(env: List[Env.Binding]):
object Env:
  case class Binding(name: String, value: Value)

243 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
object Env:
  case class Binding(name: String, value: Value)


e |- Ref name ⇓ e(name)

244 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
object Env:
  case class Binding(name: String, value: Value)


e |- Ref name ⇓ e(name)

245 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
object Env:
  case class Binding(name: String, value: Value)


e |- Ref name ⇓ e(name)

246 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
object Env:
  case class Binding(name: String, value: Value)


e |- Ref name ⇓ e(name)

247 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
object Env:
  case class Binding(name: String, value: Value)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

248 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
    Env.Binding(name, value)
object Env:
  case class Binding(name: String, value: Value)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

249 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
    Env.Binding(name, value) :: env
object Env:
  case class Binding(name: String, value: Value)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

250 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
object Env:
  case class Binding(name: String, value: Value)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

251 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
object Env:
  case class Binding(name: String, value: Value)
  val empty = Env(List.empty)

252 / 703

def interpret(expr: Expr): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF)

253 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)

254 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

255 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

256 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =
  val v1 = interpret(value, e)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

257 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =
  val v1 = interpret(value, e)
  val v2 = interpret(body, ???)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

258 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =
  val v1 = interpret(value, e)
  val v2 = interpret(body, ???)

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

259 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =
  val v1 = interpret(value, e)
  val v2 = interpret(body, e.bind(name, v1))

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

260 / 703

def let(name: String, value: Expr, body: Expr, e: Env) =
  val v1 = interpret(value, e)
  val v2 = interpret(body, e.bind(name, v1))
  v2

e |- value ⇓ v₁          e[name <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         e |- Let name value body ⇓ v₂

261 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)


e |- Ref name ⇓ e(name)

262 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              =>


e |- Ref name ⇓ e(name)

263 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)


e |- Ref name ⇓ e(name)

264 / 703

let x = 1 in
  (let x = 2 in x) + x

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

265 / 703

let x = 1 in
  (let x = 2 in x) + x

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// val res3: Value = Num(3)

266 / 703

Key takeaways

267 / 703

Key takeaways

Local bindings have a scope that can be analyzed statically

268 / 703

Key takeaways

Local bindings have a scope that can be analyzed statically
They can shadowed, but not overwritten

269 / 703

Key takeaways

Local bindings have a scope that can be analyzed statically
They can shadowed, but not overwritten
Their interpretation requires an environment

270 / 703

Reusing Code271 / 703

let x = 1 in
  x + 2

272 / 703

let x = 1 in
  x + 2

273 / 703

let x = 1 in
  x + 2

274 / 703

let x = 1 in
  x + 2

275 / 703

(x -> x + 2) 1

276 / 703

(x -> x + 2) 1

277 / 703

(x -> x + 2) 1

278 / 703

(x -> x + 2) 1

279 / 703

​x = 1
​
​

​x + 2
​
​
​

280 / 703

x = 1

x + 2

281 / 703

x = 1

1 + 2

282 / 703

x = 1

1 + 2

283 / 703

x = 1

284 / 703

let f = x -> x + 2 in
  f 1

285 / 703

let f = x -> x + 2 in
  f 1

286 / 703

let f = x -> x + 2 in
  f 1

287 / 703

let f = x -> x + 2 in
  f 1

288 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)

let f = x -> x + 2 in
  f 1

289 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun()

let f = x -> x + 2 in
  f 1

290 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun(param: String)

let f = x -> x + 2 in
  f 1

291 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun(param: String, body: Expr)

let f = x -> x + 2 in
  f 1

292 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

293 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

294 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

295 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

296 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

297 / 703

y = 1

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

298 / 703

y = 1

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

299 / 703

y = 1
f = x -> x + y

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

300 / 703

y = 1
f = x -> x + y

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

301 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

302 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

303 / 703

y = 1
f = x -> x + y
y = 2
​x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      x + y

304 / 703

y = 1
f = x -> x + y
y = 2
​x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      x + y

305 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      3 + y

306 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      3 + y

307 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      3 + 2

308 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      3 + 2

309 / 703

y = 1
f = x -> x + y
y = 2

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      5

310 / 703

y = 1
f = x -> x + y
y = 2
x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

311 / 703

y = 1
f = x -> x + y
y = 2
x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

312 / 703

y = 1
f = x -> x + y
y = 2
x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

313 / 703

y = 1
f = x -> x + y
y = 2
x = 3

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

314 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun(param: String, body: Expr)

315 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun(param: String, body: Expr, env: Env)

316 / 703


e |- Fun ⇓ ???

let f = x -> x + 2 in
  f 1

317 / 703


e |- Fun param ⇓ ???

let f = x -> x + 2 in
  f 1

318 / 703


e |- Fun param body ⇓ ???

let f = x -> x + 2 in
  f 1

319 / 703


e |- Fun param body ⇓ ???

let f = x -> x + 2 in
  f 1

320 / 703


e |- Fun param body ⇓ Value.Fun

let f = x -> x + 2 in
  f 1

321 / 703


e |- Fun param body ⇓ Value.Fun param

let f = x -> x + 2 in
  f 1

322 / 703


e |- Fun param body ⇓ Value.Fun param body

let f = x -> x + 2 in
  f 1

323 / 703


e |- Fun param body ⇓ Value.Fun param body e

let f = x -> x + 2 in
  f 1

324 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply ⇓ ???

let f = x -> x + 2 in
  f 1

325 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun ⇓ ???

let f = x -> x + 2 in
  f 1

326 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

327 / 703

e |- fun ⇓ ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

328 / 703

e |- fun ⇓ ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

329 / 703

e |- fun ⇓ Value.Fun param body eʹ
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

330 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

331 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
??? |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

332 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
??? |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

333 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

334 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

335 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

336 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

337 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

338 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ ???

let f = x -> x + 2 in
  f 1

339 / 703

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

let f = x -> x + 2 in
  f 1

340 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)


e |- Fun param body ⇓ Value.Fun param body e

341 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun()


e |- Fun param body ⇓ Value.Fun param body e

342 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String)


e |- Fun param body ⇓ Value.Fun param body e

343 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)


e |- Fun param body ⇓ Value.Fun param body e

344 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

345 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply()

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

346 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

347 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

348 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)


e |- Fun param body ⇓ Value.Fun param body e

349 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)


e |- Fun param body ⇓ Value.Fun param body e

350 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)


e |- Fun param body ⇓ Value.Fun param body e

351 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

352 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)
  case Apply(fun, arg)        => apply(fun, arg, e)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

353 / 703

def apply(fun: Expr, arg: Expr, e: Env) =

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

354 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

355 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

356 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)
      val v2 = interpret(body, ???)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

357 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)
      val v2 = interpret(body, ???)

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

358 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)
      val v2 = interpret(body, eʹ.bind(param, v1))

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

359 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)
      val v2 = interpret(body, eʹ.bind(param, v1))
      v2

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

360 / 703

def apply(fun: Expr, arg: Expr, e: Env) =
  interpret(fun, e) match
    case Value.Fun(param, body, eʹ) =>
      val v1 = interpret(arg, e)
      val v2 = interpret(body, eʹ.bind(param, v1))
      v2
    case _ => typeError("apply")

e |- fun ⇓ Value.Fun param body eʹ      e |- arg ⇓ v₁
eʹ[param <- v₁] |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
             e |- Apply fun arg ⇓ v₂

361 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

362 / 703

let y = 1 in
  let f = x -> x + y in
    let y = 2 in
      f 3

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// val res4: Value = Num(4)

363 / 703

let add = ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

364 / 703

let add = ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

365 / 703

let add = lhs -> ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

366 / 703

let add = lhs -> ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

367 / 703

let add = lhs -> rhs -> ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

368 / 703

let add = lhs -> rhs -> ??? in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

369 / 703

let add = lhs -> rhs -> lhs + rhs in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

370 / 703

let add = lhs -> rhs -> lhs + rhs in
  add 1 2

val expr = ???

interpret(expr, Env.empty)

371 / 703

let add = lhs -> rhs -> lhs + rhs in
  add 1 2

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

372 / 703

let add = lhs -> rhs -> lhs + rhs in
  add 1 2

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// val res5: Value = Num(3)

373 / 703

Key takeaways

374 / 703

Key takeaways

Functions are values

375 / 703

Key takeaways

Functions are values
They close over their environment

376 / 703

Key takeaways

Functions are values
They close over their environment
Yes, unary functions are sufficient

377 / 703

Repeating actions378 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

379 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

380 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

381 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

382 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

383 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10

384 / 703

let sumFor = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumFor 1 10
​
​

385 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumWhile 1 10
​
​

386 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    for i = lower to upper do
      acc = acc + i
    acc
  in sumWhile 1 10

387 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    var i   = lower
    for i = lower to upper do
      acc = acc + i
    acc
  in sumWhile 1 10
​

388 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    var i   = lower
    for i = lower to upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumWhile 1 10

389 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    var i   = lower
    for i = lower to upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumWhile 1 10

390 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    var i   = lower
    while i < upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumWhile 1 10

391 / 703

let sumWhile = lower -> upper ->
    var acc = 0
    var i   = lower
    while i < upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumWhile 1 10

392 / 703

let sumRec = lower -> upper ->
    var acc = 0
    var i   = lower
    while i < upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumRec 1 10

393 / 703

let sumRec = lower -> upper ->
    var acc = 0
    var i   = lower
    while i < upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumRec 1 10

394 / 703

let sumRec = lower -> upper ->
    var acc = 0
    var i   = lower
    while i < upper do
      acc = acc + i
      i   = i + 1
    acc
  in sumRec 1 10

395 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      while i < upper do
        acc = acc + i
        i   = i + 1
      acc
    in go 0 lower
  in sumRec 1 10

396 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      while i < upper do
        acc = acc + i
        i   = i + 1
      acc
    in go 0 lower
  in sumRec 1 10

397 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      acc
    in go 0 lower
  in sumRec 1 10
​
​

398 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      acc
    in go 0 lower
  in sumRec 1 10
​
​

399 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      else acc
    in go 0 lower
  in sumRec 1 10
​
​

400 / 703

let sumRec = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      else acc
    in go 0 lower
  in sumRec 1 10
​
​

401 / 703

let sum = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      else acc
    in go 0 lower
  in sum 1 10
​
​

402 / 703

let sum = lower -> upper ->
    let go = acc -> i ->
      if i < upper then go (acc + i) (i + 1)
      else acc
    in go 0 lower
  in sum 1 10
​
​

403 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10
​
​
​
​

404 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

405 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

406 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

407 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

408 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt ⇓ ???

if 1 > 2 then false
         else true

409 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs ⇓ ???

if 1 > 2 then false
         else true

410 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ ???

if 1 > 2 then false
         else true

411 / 703

e |- lhs ⇓ Value.Num v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ ???

if 1 > 2 then false
         else true

412 / 703

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ ???

if 1 > 2 then false
         else true

413 / 703

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ ???

if 1 > 2 then false
         else true

414 / 703

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

if 1 > 2 then false
         else true

415 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

416 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt()
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

417 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

418 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

419 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)
  case Apply(fun, arg)        => apply(fun, arg, e)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

420 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)             => Value.Num(value)
  case Bool(value)            => Value.Bool(value)
  case Add(lhs, rhs)          => add(lhs, rhs, e)
  case Gt(lhs, rhs)           => gt(lhs, rhs, e)
  case Cond(pred, onT, onF)   => cond(pred, onT, onF, e)
  case Let(name, value, body) => let(name, value, body, e)
  case Ref(name)              => e.lookup(name)
  case Fun(param, body)       => Value.Fun(param, body, e)
  case Apply(fun, arg)        => apply(fun, arg, e)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

421 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

422 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) =>

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

423 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) =>

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

424 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) =>

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

425 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Bool(v1 > v2)

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

426 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Bool(v1 > v2)
    case _                              =>

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

427 / 703

def gt(lhs: Expr, rhs: Expr, e: Env) =
  (interpret(lhs, e), interpret(rhs, e)) match
    case (Value.Num(v1), Value.Num(v2)) => Value.Bool(v1 > v2)
    case _                              => typeError("gt")

e |- lhs ⇓ Value.Num v₁      e |- rhs ⇓ Value.Num v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
        e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂)

428 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

429 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// ⛔ Unbound variable: sum

430 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// ⛔ Unbound variable: sum

431 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// ⛔ Unbound variable: sum

432 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)
// ⛔ Unbound variable: sum

433 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

434 / 703

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

435 / 703

enum Value:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Fun(param: String, body: Expr, env: Env)

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

436 / 703

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

437 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

438 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

439 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

440 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

441 / 703

e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

442 / 703

e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

443 / 703

eʹ = e[name <- ???]; e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

444 / 703

eʹ = e[name <- ???]; e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

445 / 703

eʹ = e[name <- ∅]; e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

446 / 703

eʹ = e[name <- ∅]; e |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

447 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

448 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

449 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

450 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

451 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ ???

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

452 / 703

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

453 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

454 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec()
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

455 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

456 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

457 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

458 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

459 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
object Env:
  case class Binding(name: String, value: Value)
  val empty = Env(List.empty)

460 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
​
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
​
  def update(name: String, value: Value) =
​
object Env:
  case class Binding(name: String, value: Value)
​
  val empty = Env(List.empty)
​
​

461 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
​
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
​
  def update(name: String, value: Value) =
    env.find(_.name == name)
​
object Env:
  case class Binding(name: String, value: Value)
​
  val empty = Env(List.empty)
​

462 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
​
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
​
  def update(name: String, value: Value) =
    env.find(_.name == name)
       .foreach(_.value = value)
​
object Env:
  case class Binding(name: String, value: Value)
​
  val empty = Env(List.empty)

463 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
​
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
​
  def update(name: String, value: Value) =
    env.find(_.name == name)
       .foreach(_.value = value)
​
object Env:
  case class Binding(name: String, value: Value)
​
  val empty = Env(List.empty)

464 / 703

case class Env(env: List[Env.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.value)
       .getOrElse(sys.error(s"Unbound variable: $name"))
​
  def bind(name: String, value: Value) =
    Env(Env.Binding(name, value) :: env)
​
  def update(name: String, value: Value) =
    env.find(_.name == name)
       .foreach(_.value = value)
​
object Env:
  case class Binding(name: String, var value: Value)
​
  val empty = Env(List.empty)

465 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)                => Value.Num(value)
  case Bool(value)               => Value.Bool(value)
  case Add(lhs, rhs)             => add(lhs, rhs, e)
  case Gt(lhs, rhs)              => gt(lhs, rhs, e)
  case Cond(pred, onT, onF)      => cond(pred, onT, onF, e)
  case Let(name, value, body)    => let(name, value, body, e)
  case Ref(name)                 => e.lookup(name)
  case Fun(param, body)          => Value.Fun(param, body, e)
  case Apply(fun, arg)           => apply(fun, arg, e)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

466 / 703

def interpret(expr: Expr, e: Env): Value = expr match
  case Num(value)                => Value.Num(value)
  case Bool(value)               => Value.Bool(value)
  case Add(lhs, rhs)             => add(lhs, rhs, e)
  case Gt(lhs, rhs)              => gt(lhs, rhs, e)
  case Cond(pred, onT, onF)      => cond(pred, onT, onF, e)
  case Let(name, value, body)    => let(name, value, body, e)
  case LetRec(name, value, body) => letRec(name, value, body, e)
  case Ref(name)                 => e.lookup(name)
  case Fun(param, body)          => Value.Fun(param, body, e)
  case Apply(fun, arg)           => apply(fun, arg, e)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

467 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

468 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =
  val eʹ = e.bind(name, null)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

469 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =
  val eʹ = e.bind(name, null)
  val v1 = interpret(value, eʹ)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

470 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =
  val eʹ = e.bind(name, null)
  val v1 = interpret(value, eʹ)
  eʹ.update(name, v1)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

471 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =
  val eʹ = e.bind(name, null)
  val v1 = interpret(value, eʹ)
  eʹ.update(name, v1)
  val v2 = interpret(body, eʹ)

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

472 / 703

def letRec(name: String, value: Expr, body: Expr, e: Env) =
  val eʹ = e.bind(name, null)
  val v1 = interpret(value, eʹ)
  eʹ.update(name, v1)
  val v2 = interpret(body, eʹ)
  v2

eʹ = e[name <- ∅]; eʹ |- value ⇓ v₁
  eʹ[name := v₁]; eʹ |- body ⇓ v₂
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
 e |- LetRec name value body ⇓ v₂

473 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

474 / 703

let sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = Let(
  // ...
)

interpret(expr, Env.empty)

475 / 703

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = LetRec(
  // ...
)

interpret(expr, Env.empty)

476 / 703

let rec sum = lower -> upper ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = LetRec(
  // ...
)

interpret(expr, Env.empty)
// val res6: Value = Num(55)

477 / 703

Key takeaways

478 / 703

Key takeaways

Loops are implemented as recursive functions

479 / 703

Key takeaways

Loops are implemented as recursive functions
Recursive functions need special syntax...

480 / 703

Key takeaways

Loops are implemented as recursive functions
Recursive functions need special syntax...
... and a mutable environment

481 / 703

Identifying invalid programs482 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

483 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

484 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

485 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

486 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)
// ⛔ Type error in add

487 / 703

def typeCheck(expr: Expr): ??? =

488 / 703

def typeCheck(expr: Expr): ??? =

489 / 703

def typeCheck(expr: Expr): ??? =

490 / 703

def typeCheck(expr: Expr): Boolean =

491 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => ???

492 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => ???

493 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true

494 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => ???

495 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => ???

496 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true

497 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => ???

498 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => ???

499 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

500 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

501 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

interpret(expr, Env.empty)

502 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

typeCheck(expr)

503 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

typeCheck(expr)
// val res7: Boolean = true

504 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

505 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

506 / 703

enum Type:

507 / 703

enum Type:
  case Num
​
​
​

508 / 703

enum Type:
  case Num
  case Bool
​
​

509 / 703

def typeCheck(expr: Expr): Boolean =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

510 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

511 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

512 / 703

Num value : ???

513 / 703

Num value : ???

514 / 703

Num value : ???

515 / 703

Num value : ???

516 / 703

Num value : Type.Num

517 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => true
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

Num value : Type.Num

518 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

Num value : Type.Num

519 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

520 / 703

Bool value : ???

true

521 / 703

Bool value : ???

true

522 / 703

Bool value : Type.Bool

true

523 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => true
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

Bool value : Type.Bool

524 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

Bool value : Type.Bool

525 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

526 / 703

      Add lhs rhs : ???

1 + 2

527 / 703

lhs : Type.Num
      Add lhs rhs : ???

1 + 2

528 / 703

lhs : Type.Num       rhs : Type.Num
      Add lhs rhs : ???

1 + 2

529 / 703

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : ???

1 + 2

530 / 703

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : ???

1 + 2

531 / 703

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

1 + 2

532 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs)

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

533 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => checkAdd(lhs, rhs)

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

534 / 703

def checkAdd(lhs: Expr, rhs: Expr) =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

535 / 703

def checkAdd(lhs: Expr, rhs: Expr) =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

536 / 703

def expect() =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

537 / 703

def expect(expr: Expr) =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

538 / 703

def expect(expr: Expr, expected: Type) =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

539 / 703

def expect(expr: Expr, expected: Type) =
  typeCheck(expr).flatMap =>

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

540 / 703

def expect(expr: Expr, expected: Type) =
  typeCheck(expr).flatMap: observed =>

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

541 / 703

def expect(expr: Expr, expected: Type) =
  typeCheck(expr).flatMap: observed =>
    if observed == expected then

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

542 / 703

def expect(expr: Expr, expected: Type) =
  typeCheck(expr).flatMap: observed =>
    if observed == expected then Right(())

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

543 / 703

def expect(expr: Expr, expected: Type) =
  typeCheck(expr).flatMap: observed =>
    if observed == expected then Right(())
    else Left(s"Expected $expected, found $observed")

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

544 / 703

def checkAdd(lhs: Expr, rhs: Expr) =

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

545 / 703

def checkAdd(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

546 / 703

def checkAdd(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)
      _ <- expect(rhs, Type.Num)

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

547 / 703

def checkAdd(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)
      _ <- expect(rhs, Type.Num)
  yield Type.Num

lhs : Type.Num       rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Add lhs rhs : Type.Num

548 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : ???

1 > 2

549 / 703

lhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : ???

1 > 2

550 / 703

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : ???

1 > 2

551 / 703

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : ???

1 > 2

552 / 703

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

1 > 2

553 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => checkAdd(lhs, rhs)

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

554 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)  =>

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

555 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)    => Right(Type.Num)
    case Bool(value)   => Right(Type.Bool)
    case Add(lhs, rhs) => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)  => checkGt(lhs, rhs)

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

556 / 703

def checkGt(lhs: Expr, rhs: Expr) =

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

557 / 703

def checkGt(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

558 / 703

def checkGt(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)
      _ <- expect(rhs, Type.Num)

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

559 / 703

def checkGt(lhs: Expr, rhs: Expr) =
  for _ <- expect(lhs, Type.Num)
      _ <- expect(rhs, Type.Num)
  yield Type.Bool

lhs : Type.Num      rhs : Type.Num
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Gt lhs rhs : Type.Bool

560 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

561 / 703

pred : Type.Bool
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

562 / 703

pred : Type.Bool      onT : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

563 / 703

pred : Type.Bool      onT : X      onF : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

564 / 703

pred : Type.Bool      onT : X      onF : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

565 / 703

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

566 / 703

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : ???

if true then 1
        else 2

567 / 703

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

if true then 1
        else 2

568 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)           => Right(Type.Num)
    case Bool(value)          => Right(Type.Bool)
    case Add(lhs, rhs)        => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)         => checkGt(lhs, rhs)

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

569 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)           => Right(Type.Num)
    case Bool(value)          => Right(Type.Bool)
    case Add(lhs, rhs)        => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)         => checkGt(lhs, rhs)
    case Cond(pred, onT, onF) =>

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

570 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)           => Right(Type.Num)
    case Bool(value)          => Right(Type.Bool)
    case Add(lhs, rhs)        => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)         => checkGt(lhs, rhs)
    case Cond(pred, onT, onF) => checkCond(pred, onT, onF)

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

571 / 703

def checkCond(pred: Expr, onT: Expr, onF: Expr) =

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

572 / 703

def checkCond(pred: Expr, onT: Expr, onF: Expr) =
  for _ <- expect(pred, Type.Bool)

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

573 / 703

def checkCond(pred: Expr, onT: Expr, onF: Expr) =
  for _ <- expect(pred, Type.Bool)
      x <- typeCheck(onT)

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

574 / 703

def checkCond(pred: Expr, onT: Expr, onF: Expr) =
  for _ <- expect(pred, Type.Bool)
      x <- typeCheck(onT)
      _ <- expect(onF, x)

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

575 / 703

def checkCond(pred: Expr, onT: Expr, onF: Expr) =
  for _ <- expect(pred, Type.Bool)
      x <- typeCheck(onT)
      _ <- expect(onF, x)
  yield x

pred : Type.Bool      onT : X       onF : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
         Cond pred onT onF : X

576 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
           Let name value body : ???

let x = 1 in
  x + 2

577 / 703

value : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
           Let name value body : ???

let x = 1 in
  x + 2

578 / 703

value : X                            body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
           Let name value body : ???

let x = 1 in
  x + 2

579 / 703

Γ |- value : X                  Γ |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : ???

let x = 1 in
  x + 2

580 / 703

Γ |- value : X                  Γ |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : ???

let x = 1 in
  x + 2

581 / 703

Γ |- value : X                  Γ |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : ???

let x = 1 in
  x + 2

582 / 703

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : ???

let x = 1 in
  x + 2

583 / 703

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : ???

let x = 1 in
  x + 2

584 / 703

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

let x = 1 in
  x + 2

585 / 703


Γ |- Ref name : ???

let x = 1 in
  x + 2

586 / 703


Γ |- Ref name : ???

let x = 1 in
  x + 2

587 / 703


Γ |- Ref name : Γ(name)

let x = 1 in
  x + 2

588 / 703


Γ |- Ref name : Γ(name)

let x = 1 in
  x + 2

589 / 703

case class TypeEnv():

590 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
​
​
​
​
​
​
​
​
​
​
​
​

591 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
​
​object TypeEnv:
  case class Binding()
​
​
​
​
​
​
​
​
​

592 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
​
object TypeEnv:
  case class Binding(name: String)
​
​
​
​
​
​
​
​
​

593 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​
​
​
​
​
​
​

594 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​
​
​
​
​
​

595 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​
​
​
​
​

596 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​
​
​
​

597 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​
​
​

598 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
  def bind(name: String, tpe: Type) =
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​
​

599 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
  def bind(name: String, tpe: Type) =
    TypeEnv.Binding(name, tpe)
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​

600 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
  def bind(name: String, tpe: Type) =
    TypeEnv.Binding(name, tpe) :: env
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​

601 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
  def bind(name: String, tpe: Type) =
    TypeEnv(TypeEnv.Binding(name, tpe) :: env)
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
​

602 / 703

case class TypeEnv(env: List[TypeEnv.Binding]):
  def lookup(name: String) =
    env.find(_.name == name)
       .map(_.tpe)
       .toRight(s"Type binding $name not found")
​
  def bind(name: String, tpe: Type) =
    TypeEnv(TypeEnv.Binding(name, tpe) :: env)
​
object TypeEnv:
  case class Binding(name: String, tpe: Type)
​
  val empty = TypeEnv(List.empty)

603 / 703

def typeCheck(expr: Expr): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF)

604 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)

605 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) =>

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

606 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

607 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

608 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =
  for x <- typeCheck(value, Γ)

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

609 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =
  for x <- typeCheck(value, Γ)
      y <- typeCheck(body, ???)

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

610 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =
  for x <- typeCheck(value, Γ)
      y <- typeCheck(body, ???)

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

611 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =
  for x <- typeCheck(value, Γ)
      y <- typeCheck(body, Γ.bind(name, x))

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

612 / 703

def checkLet(name: String, value: Expr, body: Expr, Γ: TypeEnv) =
  for x <- typeCheck(value, Γ)
      y <- typeCheck(body, Γ.bind(name, x))
  yield y

Γ |- value : X       Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- Let name value body : Y

613 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)


Γ |- Ref name : Γ(name)

614 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)
    case Ref(name)              =>


Γ |- Ref name : Γ(name)

615 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)
    case Ref(name)              => Γ.lookup(name)


Γ |- Ref name : Γ(name)

616 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

617 / 703

     Γ |- body : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

618 / 703

     Γ |- body : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

619 / 703

    Γ[param <- X] |- body : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

620 / 703

    Γ[param <- X] |- body : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

621 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

622 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : ???

let f = x -> x + 1 in
  f 2

623 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : X -> Y

let f = x -> x + 1 in
  f 2

624 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : X -> Y

let f = x -> x + 1 in
  f 2

625 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun param body : X -> Y

let f = x -> x + 1 in
  f 2

626 / 703

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

let f = (x: Num) -> x + 1 in
  f 2

627 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

628 / 703

Γ |- fun : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

629 / 703

Γ |- fun : ???
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

630 / 703

Γ |- fun : X -> Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

631 / 703

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

632 / 703

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : ???

let f = (x: Num) -> x + 1 in
  f 2

633 / 703

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
     Γ |- Apply fun arg : Y

let f = (x: Num) -> x + 1 in
  f 2

634 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Ref(name: String )
  case Fun(param: String, body: Expr)
  case Apply(fun: Expr, arg: Expr)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

635 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Ref(name: String )
  case Fun(param: String, pType: Type, body: Expr)
  case Apply(fun: Expr, arg: Expr)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

636 / 703

enum Type:
  case Num
  case Bool

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

637 / 703

enum Type:
  case Num
  case Bool
  case Fun()

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

638 / 703

enum Type:
  case Num
  case Bool
  case Fun(from: Type)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

639 / 703

enum Type:
  case Num
  case Bool
  case Fun(from: Type, to: Type)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

640 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)
    case Ref(name)              => Γ.lookup(name)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

641 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)
    case Ref(name)              => Γ.lookup(name)
    case Fun(param, x, body)    =>

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

642 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)             => Right(Type.Num)
    case Bool(value)            => Right(Type.Bool)
    case Add(lhs, rhs)          => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)           => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)   => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body) => checkLet(name, value, body, Γ)
    case Ref(name)              => Γ.lookup(name)
    case Fun(param, x, body)    => checkFun(param, x, body Γ)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

643 / 703

def checkFun(param: String, x: Type, body: Expr, Γ: TypeEnv) =

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

644 / 703

def checkFun(param: String, x: Type, body: Expr, Γ: TypeEnv) =
  for y <- typeCheck(body, ???)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

645 / 703

def checkFun(param: String, x: Type, body: Expr, Γ: TypeEnv) =
  for y <- typeCheck(body, ???)

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

646 / 703

def checkFun(param: String, x: Type, body: Expr, Γ: TypeEnv) =
  for y <- typeCheck(body, Γ.bind(param, x))

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

647 / 703

def checkFun(param: String, x: Type, body: Expr, Γ: TypeEnv) =
  for y <- typeCheck(body, Γ.bind(param, x))
  yield x -> y

    Γ[param <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
Γ |- Fun (param : X) body : X -> Y

648 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

649 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)
    case Apply(fun, arg)         =>

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

650 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)
    case Apply(fun, arg)         => checkApply(fun, arg, Γ)

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

651 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

652 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

653 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:
    case x -> y =>

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

654 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:
    case x -> y => expect(arg, x, Γ)

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

655 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:
    case x -> y => expect(arg, x, Γ)
                     .map(_ => y)

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

656 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:
    case x -> y => expect(arg, x, Γ)
                     .map(_ => y)
    case other  =>

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

657 / 703

def checkApply(fun: Expr, arg: Expr, Γ: TypeEnv) =
  typeCheck(fun, Γ).flatMap:
    case x -> y => expect(arg, x, Γ)
                     .map(_ => y)
    case other  => Left(s"Expected function, found $other")

Γ |- fun : X -> Y     Γ |- arg : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
    Γ |- Apply fun arg : Y

658 / 703


⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

659 / 703

??? |- value : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

660 / 703

??? |- value : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

661 / 703

Γ[name <- X] |- value : X
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

662 / 703

Γ[name <- X] |- value : X               ??? |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

663 / 703

Γ[name <- X] |- value : X               ??? |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

664 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

665 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : ???

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

666 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : Y

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

667 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : Y

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

668 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name value body : Y

let rec sum = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

669 / 703

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

let rec (sum: Num -> Num -> Num) = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

670 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, body: Expr)
  case Ref(name: String)
  case Fun(param: String, paramType: Type, body: Expr)
  case Apply(fun: Expr, arg: Expr)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

671 / 703

enum Expr:
  case Num(value: Int)
  case Bool(value: Boolean)
  case Add(lhs: Expr, rhs: Expr)
  case Gt(lhs: Expr, rhs: Expr)
  case Cond(pred: Expr, onT: Expr, onF: Expr)
  case Let(name: String, value: Expr, body: Expr)
  case LetRec(name: String, value: Expr, vType: Type, body: Expr)
  case Ref(name: String)
  case Fun(param: String, paramType: Type, body: Expr)
  case Apply(fun: Expr, arg: Expr)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

672 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Apply(fun, arg)         => checkApply(fun, arg, Γ)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

673 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Apply(fun, arg)         => checkApply(fun, arg, Γ)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)
    case LetRec(name, value, x, body) =>

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

674 / 703

def typeCheck(expr: Expr, Γ: TypeEnv): Either[String, Type] =
  expr match
    case Num(value)              => Right(Type.Num)
    case Bool(value)             => Right(Type.Bool)
    case Add(lhs, rhs)           => checkAdd(lhs, rhs, Γ)
    case Gt(lhs, rhs)            => checkGt(lhs, rhs, Γ)
    case Cond(pred, onT, onF)    => checkCond(pred, onT, onF, Γ)
    case Let(name, value, body)  => checkLet(name, value, body, Γ)
    case Ref(name)               => Γ.lookup(name)
    case Apply(fun, arg)         => checkApply(fun, arg, Γ)
    case Fun(param, pType, body) => checkFun(param, pType, body, Γ)
    case LetRec(name, value, x, body) =>
      checkLetRec(name, value, x, body, Γ)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

675 / 703

def checkLetRec(name: String, value: Expr, x: Type,
                body: Expr, Γ: TypeEnv) =

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

676 / 703

def checkLetRec(name: String, value: Expr, x: Type,
                body: Expr, Γ: TypeEnv) =
  val eʹ = Γ.bind(name, x)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

677 / 703

def checkLetRec(name: String, value: Expr, x: Type,
                body: Expr, Γ: TypeEnv) =
  val eʹ = Γ.bind(name, x)
  for _ <- expect(value, x, eʹ)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

678 / 703

def checkLetRec(name: String, value: Expr, x: Type,
                body: Expr, Γ: TypeEnv) =
  val eʹ = Γ.bind(name, x)
  for _ <- expect(value, x, eʹ)
      y <- typeCheck(body, eʹ)

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

679 / 703

def checkLetRec(name: String, value: Expr, x: Type,
                body: Expr, Γ: TypeEnv) =
  val eʹ = Γ.bind(name, x)
  for _ <- expect(value, x, eʹ)
      y <- typeCheck(body, eʹ)
  yield y

Γ[name <- X] |- value : X      Γ[name <- X] |- body : Y
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯
      Γ |- LetRec name (value : X) body : Y

680 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

typeCheck(expr, TypeEnv.empty)

681 / 703

1 + true

val expr = Add(
  Num(1),
  Bool(true)
)

typeCheck(expr, TypeEnv.empty)
// val res9: Either[String, Type] = Left(Expected Num, found Bool)

682 / 703

let rec (sum: Num -> Num -> Num) = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = LetRec(
  // ...
)

typeCheck(expr, TypeEnv.empty)

683 / 703

let rec (sum: Num -> Num -> Num) = (lower: Num) -> (upper: Num) ->
    if lower > upper then 0
    else lower + (sum (lower + 1) upper)
  in sum 1 10

val expr = LetRec(
  // ...
)

typeCheck(expr, TypeEnv.empty)
// val res10: Either[String, Type] = Right(Num)

684 / 703

Key takeaways

685 / 703

Key takeaways

Type checking is very similar to interpretation

686 / 703

Key takeaways

Type checking is very similar to interpretation
It follows the same "formalise / implement" logic

687 / 703

Key takeaways

Type checking is very similar to interpretation
It follows the same "formalise / implement" logic
We're still allowing illegal programs though...

688 / 703

In closing689 / 703

If you only remember 1 slide...690 / 703

If you only remember 1 slide...Programs are represented as ASTs
691 / 703

If you only remember 1 slide...

Programs are represented as ASTs
We use formal semantics to reason about them

692 / 703

If you only remember 1 slide...

Programs are represented as ASTs
We use formal semantics to reason about them
Implementation is then relatively straightforward

693 / 703

Nicolas Rinaudo • @NicolasRinaudo@functional.cafe

694 / 703

Typed Expression695 / 703

enum TypedExpr[A]:
  case Num(value: Int) extends TypedExpr[Type.Num.type]
  case Bool(value: Boolean) extends TypedExpr[Type.Bool.type]
  case Add(lhs: TypedExpr[Type.Num.type], rhs: TypedExpr[Type.Num.type]) extends TypedExpr[Type.Num.type]
  case Gt(lhs: TypedExpr[Type.Num.type], rhs: TypedExpr[Type.Num.type]) extends TypedExpr[Type.Bool.type]
  case Cond[A](pred: TypedExpr[Type.Bool.type], onT: TypedExpr[A], onF: TypedExpr[A]) extends TypedExpr[A]
  case Let[A, B](name: String, value: TypedExpr[A], body: TypedExpr[B]) extends TypedExpr[B]
  case LetRec[A](name: String, value: TypedExpr[Type.Fun], body: TypedExpr[A]) extends TypedExpr[A]
  case Ref[A](name: String) extends TypedExpr[A]
  case Fun[A](param: String, body: TypedExpr[A]) extends TypedExpr[Type.Fun]
  case Apply[A, B](fun: TypedExpr[Type.Fun], arg: TypedExpr[A]) extends TypedExpr[B]

696 / 703

enum Type:
  case Num
  case Bool
  case Fun(from: Type, to: Type)
object Type:
  type Num = Type.Num.type
  type Bool = Type.Bool.type

697 / 703

enum TypedExpr[A]:
  case Num(value: Int) extends TypedExpr[Type.Num]
  case Bool(value: Boolean) extends TypedExpr[Type.Bool]
  case Add(lhs: TypedExpr[Type.Num], rhs: TypedExpr[Type.Num]) extends TypedExpr[Type.Num]
  case Gt(lhs: TypedExpr[Type.Num], rhs: TypedExpr[Type.Num]) extends TypedExpr[Type.Bool]
  case Cond[A](pred: TypedExpr[Type.Bool], onT: TypedExpr[A], onF: TypedExpr[A]) extends TypedExpr[A]
  case Let[A, B](name: String, value: TypedExpr[A], body: TypedExpr[B]) extends TypedExpr[B]
  case LetRec[A](name: String, value: TypedExpr[Type.Fun], body: TypedExpr[A]) extends TypedExpr[A]
  case Fun[A](param: String, body: TypedExpr[A]) extends TypedExpr[Type.Fun]
  case Ref[A](name: String) extends TypedExpr[A]
  case Apply[A, B](fun: TypedExpr[Type.Fun], arg: TypedExpr[A]) extends TypedExpr[B]

698 / 703

enum Type:
  case Num
  case Bool
  case Fun[From <: Type, To <: Type](from: From, to: To)
object Type:
  type Num = Type.Num.type
  type Bool = Type.Bool.type
type ->[A <: Type, B <: Type] = Type.Fun[A, B]

699 / 703

enum TypedExpr[A <: Type]:
  case Num(value: Int) extends TypedExpr[Type.Num]
  case Bool(value: Boolean) extends TypedExpr[Type.Bool]
  case Add(lhs: TypedExpr[Type.Num], rhs: TypedExpr[Type.Num]) extends TypedExpr[Type.Num]
  case Gt(lhs: TypedExpr[Type.Num], rhs: TypedExpr[Type.Num]) extends TypedExpr[Type.Bool]
  case Cond[A <: Type](pred: TypedExpr[Type.Bool], onT: TypedExpr[A], onF: TypedExpr[A]) extends TypedExpr[A]
  case Let[A <: Type, B <: Type](name: String, value: TypedExpr[A], body: TypedExpr[B]) extends TypedExpr[B]
  case LetRec[A <: Type, B <: Type, C <: Type](name: String, value: TypedExpr[A -> B], body: TypedExpr[C]) extends TypedExpr[C]
  case Ref[A <: Type](name: String) extends TypedExpr[A]
  case Fun[A <: Type, B <: Type](param: String, body: TypedExpr[B]) extends TypedExpr[A -> B]
  case Apply[A <: Type, B <: Type](fun: TypedExpr[A -> B], arg: TypedExpr[A]) extends TypedExpr[B]

700 / 703

import TypedExpr.*
Let(
  name  = "x",
  value = Bool(true),
  body  = Add(Ref("x"), Num(1))
)
// val res11: TypedExpr[Type.Num.type] = Let(x,Bool(true),Add(Ref(x),Num(1)))

701 / 703

val expr: TypedExpr[Type.Bool -> Type.Num] = Fun(
  param = "x",
  body  = Add(Ref("x"), Num(1))
)

702 / 703

↑, ←, Pg Up, k	Go to previous slide
↓, →, Pg Dn, Space, j	Go to next slide
Home	Go to first slide
End	Go to last slide
Number + Return	Go to specific slide
b / m / f	Toggle blackout / mirrored / fullscreen mode
c	Clone slideshow
p	Toggle presenter mode
t	Restart the presentation timer
?, h	Toggle this help

Programming a language

Representing code

Key takeaways

Key takeaways

Key takeaways

Key takeaways

Taking decisions

Key takeaways

Key takeaways

Key takeaways

Key takeaways

Naming things

Key takeaways

Key takeaways

Key takeaways

Key takeaways

Reusing Code

Key takeaways

Key takeaways

Key takeaways

Key takeaways

Repeating actions

Key takeaways

Key takeaways

Key takeaways

Key takeaways

Identifying invalid programs

Key takeaways

Key takeaways

Key takeaways

Key takeaways

In closing

If you only remember 1 slide...

If you only remember 1 slide...

If you only remember 1 slide...

If you only remember 1 slide...

Typed Expression

TOC

Representing code

Help