class: center, middle # Programming a language [Nicolas Rinaudo] • [@NicolasRinaudo@functional.cafe] --- class: center, middle name: ast # Representing code --- ```scala ​ ​ ​ ``` ```scala 1 ``` --- ```scala ​ ​ ​ ``` .diff-add[ ```scala *1 `+ 2` ``` ] --- .diff-add[ ```scala *​`enum Expr:` ​ ​ ``` ] ```scala 1 + 2 ``` --- .diff-add[ ```scala enum Expr: * `case Num()` ​ ``` ] ```scala 1 + `2` ``` --- .diff-add[ ```scala enum Expr: * case Num(`value: Int`) ​ ``` ] ```scala 1 + `2` ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) * `case Add()` ``` ] ```scala 1 `+` 2 ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) * case Add(`lhs: Num`) ``` ] ```scala ​`1` + 2 ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) * case Add(lhs: Num`, rhs: Num`) ``` ] ```scala 1 + `2` ``` --- ```scala ​`Num value` ⇓ ??? ​ ​ ``` ```scala 1 + `2` ``` --- ```scala Num value `⇓` ??? ​ ​ ``` ```scala 1 + `2` ``` --- .diff-rm[ ```scala *Num value ⇓ `???` ​ ​ ``` ] ```scala 1 + `2` ``` --- .diff-add[ ```scala *Num value ⇓ `value` ​ ​ ``` ] ```scala 1 + `2` ``` --- ```scala ​`Add lhs rhs` ⇓ ??? ​ ​ ``` ```scala 1 + 2 ``` --- .diff-rm[ ```scala *Add lhs rhs ⇓ `???` ​ ​ ``` ] ```scala 1 + 2 ``` --- .diff-add[ ```scala *Add lhs rhs ⇓ `lhs + rhs` ​ ​ ``` ] ```scala 1 + 2 ``` --- ```scala Add `lhs` `rhs` ⇓ lhs + rhs ​ ​ ``` ```scala 1 + 2 ``` --- .diff-add[ ```scala *​`lhs ⇓ v₁` Add lhs rhs ⇓ lhs + rhs ​ ``` ] ```scala ​`1` + 2 ``` --- .diff-add[ ```scala *lhs ⇓ v₁ `rhs ⇓ v₂` Add lhs rhs ⇓ lhs + rhs ​ ``` ] ```scala 1 + `2` ``` --- .diff-add[ ```scala lhs ⇓ v₁ rhs ⇓ v₂ *​`⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯` Add lhs rhs ⇓ lhs + rhs ``` ] ```scala 1 + 2 ``` --- .diff-rm[ ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Add lhs rhs ⇓ `lhs + rhs` ``` ] ```scala ​`1 + 2` ``` --- .diff-add[ ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Add lhs rhs ⇓ `v₁ + v₂` ``` ] ```scala ​`1 + 2` ``` --- ```scala def interpret(expr: Expr): Int = ??? ​ ​ ​ ​ ``` --- .diff-rm[ ```scala *def interpret(expr: Expr): Int = `???` ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala *def interpret(expr: Expr): Int = `expr match` ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala def interpret(expr: Expr): Int = expr match * `case Num(value) => ???` ​ ​ ​ ``` ] ```scala ​ ​ ​`Num value` ⇓ value ``` --- .diff-rm[ ```scala def interpret(expr: Expr): Int = expr match * case Num(value) => `???` ​ ​ ​ ``` ] ```scala ​ ​ Num value ⇓ `value` ``` --- .diff-add[ ```scala def interpret(expr: Expr): Int = expr match * case Num(value) => `value` ​ ​ ​ ``` ] ```scala ​ ​ Num value ⇓ `value` ``` --- .diff-add[ ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value * `case Add(lhs, rhs) => ???` ​ ​ ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ ​`Add lhs rhs` ⇓ v₁ + v₂ ``` --- .diff-rm[ ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value * case Add(lhs, rhs) => `???` ​ ​ ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-add[ ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value * case Add(lhs, rhs) => `add(lhs, rhs)` ​ ​ ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- ```scala def add(lhs: Num, rhs: Num) = ??? ​ ​ ​ ​ ``` ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-rm[ ```scala *def add(lhs: Num, rhs: Num) = `???` ​ ​ ​ ​ ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-add[ ```scala def add(lhs: Num, rhs: Num) = * `val v1 = interpret(lhs)` ​ ​ ​ ``` ] ```scala ​`lhs ⇓ v₁` rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-add[ ```scala def add(lhs: Num, rhs: Num) = val v1 = interpret(lhs) * `val v2 = interpret(rhs)` ​ ​ ``` ] ```scala lhs ⇓ v₁ `rhs ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-add[ ```scala def add(lhs: Num, rhs: Num) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ * `v1 + v2` ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ `v₁ + v₂` ``` --- ```ocaml 1 + 2 ``` ```scala val expr = ??? ``` ```scala interpret(expr) ``` --- ```ocaml 1 `+` 2 ``` .diff-rm[ ```scala *val expr = `???` ``` ] ```scala interpret(expr) ``` --- ```ocaml 1 `+` 2 ``` .diff-add[ ```scala *val expr = `Add(???, ???)` ``` ] ```scala interpret(expr) ``` --- ```ocaml ​`1` + 2 ``` .diff-rm[ ```scala *val expr = Add(`???`, ???) ``` ] ```scala interpret(expr) ``` --- ```ocaml ​`1` + 2 ``` .diff-add[ ```scala *val expr = Add(`Num(1)`, ???) ``` ] ```scala interpret(expr) ``` --- ```ocaml 1 + `2` ``` .diff-rm[ ```scala *val expr = Add(Num(1), `???`) ``` ] ```scala interpret(expr) ``` --- ```ocaml 1 + `2` ``` .diff-add[ ```scala *val expr = Add(Num(1), `Num(2)`) ``` ] ```scala interpret(expr) ``` --- ```ocaml 1 + 2 ``` ```scala val expr = Add(Num(1), Num(2)) ``` ```scala interpret(expr) // val res0: Int = 3 ``` --- .diff-add[ ```ocaml *​`(`1 + 2`)` ``` ] ```scala val expr = Add(Num(1), Num(2)) ``` ```scala interpret(expr) // val res0: Int = 3 ``` --- .diff-add[ ```ocaml *​(`(`1`)` + `((`2`))`) ``` ] ```scala val expr = Add(Num(1), Num(2)) ``` ```scala interpret(expr) // val res0: Int = 3 ``` --- .center[] ```ocaml 1 `+` 2 ``` --- .center[] ```ocaml ​`1` + `2` ``` --- .center[] ```ocaml 1 + 2 ``` --- .center[] .diff-rm[ ```ocaml *1 + `2` ``` ] --- .center[] .diff-add[ ```ocaml *1 + `(2 + 3)` ``` ] --- .center[] .diff-rm[ ```scala enum Expr: case Num(value: Int) * case Add(lhs: `Num`, rhs: `Num`) ``` ] --- .center[] .diff-add[ ```scala enum Expr: case Num(value: Int) * case Add(lhs: `Expr`, rhs: `Expr`) ``` ] --- ```scala def add(lhs: Num, rhs: Num) = val v1 = interpret(lhs) val v2 = interpret(rhs) v1 + v2 ``` ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-rm[ ```scala *def add(lhs: `Num`, rhs: `Num`) = val v1 = interpret(lhs) val v2 = interpret(rhs) v1 + v2 ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- .diff-add[ ```scala *def add(lhs: `Expr`, rhs: `Expr`) = val v1 = interpret(lhs) val v2 = interpret(rhs) v1 + v2 ``` ] ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- ```scala def add(lhs: Expr, rhs: Expr) = `val v1 = interpret(lhs)` val v2 = interpret(rhs) v1 + v2 ``` ```scala ​`lhs ⇓ v₁` rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) `val v2 = interpret(rhs)` v1 + v2 ``` ```scala lhs ⇓ v₁ `rhs ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ``` --- ```ocaml 1 + 2 ``` ```scala val expr = Add(Num(1), Num(2)) ``` ```scala interpret(expr) ``` --- .diff-rm[ ```ocaml *1 + `2` ``` ] .diff-rm[ ```scala *val expr = Add(Num(1), `Num(2)`) ``` ] ```scala interpret(expr) ``` --- .diff-add[ ```ocaml *1 + `(2 + 3)` ``` ] .diff-add[ ```scala *val expr = Add(Num(1), `Add(Num(2), Num(3))`) ``` ] ```scala interpret(expr) ``` --- ```ocaml 1 + (2 + 3) ``` ```scala val expr = Add(Num(1), Add(Num(2), Num(3))) ``` ```scala interpret(expr) // val res1: Int = 6 ``` --- ## [Key takeaways](#conclusion) -- * Source code is represented as a recursive sum type -- * This is called an AST -- * Interpretation is done through pattern matching --- class: center, middle name: conditionals # Taking decisions --- ```ocaml if true then 1 + 2 else 3 + 4 ``` --- ```ocaml if `true` then 1 + 2 else 3 + 4 ``` --- ```ocaml if true then `1 + 2` else 3 + 4 ``` --- ```ocaml if true then 1 + 2 else `3 + 4` ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond` ⇓ ??? ​ ​ ​ ​ ``` ```ocaml ​`if` true then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond `pred` ⇓ ??? ​ ​ ​ ​ ``` ] ```ocaml if `true` then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred `onT` ⇓ ??? ​ ​ ​ ​ ``` ] ```ocaml if true then `1 + 2` else 3 + 4 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT `onF` ⇓ ??? ​ ​ ​ ​ ``` ] ```ocaml if true then 1 + 2 else `3 + 4` ``` --- .diff-add[ ```scala *​`pred ⇓ ???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ ​ ​ ​ ``` ] ```ocaml if `true` then 1 + 2 else 3 + 4 ``` --- .diff-rm[ ```scala *pred ⇓ `???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ ​ ​ ​ ``` ] ```ocaml if `true` then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala *pred ⇓ `true` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ *​`pred ⇓ false` *​`⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯` * `Cond pred onT onF ⇓ ???` ``` ] ```ocaml if true then 1 + 2 else 3 + 4 ``` --- ```scala pred ⇓ `true` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ pred ⇓ `false` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ```ocaml if true then 1 + 2 else 3 + 4 ``` --- ```scala pred ⇓ `true` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ pred ⇓ false ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ```ocaml if true then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala *pred ⇓ true `onT ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ​ pred ⇓ false ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ] ```ocaml if true then `1 + 2` else 3 + 4 ``` --- .diff-rm[ ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF ⇓ `???` ​ pred ⇓ false ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ] ```ocaml if true then `1 + 2` else 3 + 4 ``` --- .diff-add[ ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF ⇓ `v` ​ pred ⇓ false ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ] ```ocaml if true then `1 + 2` else 3 + 4 ``` --- ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ `false` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ```ocaml if true then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ *pred ⇓ false `onF ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ ??? ``` ] ```ocaml if true then 1 + 2 else `3 + 4` ``` --- .diff-rm[ ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF ⇓ `???` ``` ] ```ocaml if true then 1 + 2 else 3 + 4 ``` --- .diff-add[ ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF ⇓ `v` ``` ] ```ocaml if true then 1 + 2 else 3 + 4 ``` --- ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) * `case Cond()` ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond` pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond` pred onT onF ⇓ v ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) * case Cond(`pred: Expr`) ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond `pred` onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond `pred` onT onF ⇓ v ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) * case Cond(pred: Expr`, onT: Expr`) ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred `onT` onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred `onT` onF ⇓ v ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) * case Cond(pred: Expr, onT: Expr`, onF: Expr`) ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT `onF` ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT `onF` ⇓ v ``` --- ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value case Add(lhs, rhs) => add(lhs, rhs) ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value case Add(lhs, rhs) => add(lhs, rhs) * `case Cond(pred, onT, onF) => ???` ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond pred onT onF` ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond pred onT onF` ⇓ v ``` --- .diff-rm[ ```scala def interpret(expr: Expr): Int = expr match case Num(value) => value case Add(lhs, rhs) => add(lhs, rhs) * case Cond(pred, onT, onF) => `???` ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala 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)` ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = ??? ​ ​ ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-rm[ ```scala *def cond(pred: Expr, onT: Expr, onF: Expr) = `???` ​ ​ ​ ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * `if interpret(pred) then` ​ ​ ​ ​ ``` ] ```scala ​`pred ⇓ true` onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * if interpret(pred) then` interpret(onT)` ​ ​ ​ ​ ``` ] ```scala pred ⇓ true `onT ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) * `else interpret(onF)` ​ ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false `onF ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if `interpret(pred)` then interpret(onT) else interpret(onF) ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * if interpret(pred) `!= 0` then interpret(onT) * else ` ` interpret(onF) ​ ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-rm[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * if interpret(pred) `!= 0` then interpret(onT) * else ` ` interpret(onF) ​ ​ ​ ``` ] ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) else interpret(onF) ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```scala 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) ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```scala enum Value: ​ ​ ​ ​ ​ ``` --- .diff-add[ ```scala enum Value: * `case Num(value: Int)` ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala enum Value: case Num(value: Int) * `case Bool(value: Boolean)` ​ ​ ​ ``` ] --- .diff-rm[ ```scala *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) ​ ​ ``` ] --- .diff-add[ ```scala *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) ​ ​ ``` ] --- ```scala 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) ​ ​ ``` ```scala ​ ​ ​`Num value` ⇓ value ​ ​ ​ ​ ``` --- .diff-rm[ ```scala 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) ​ ​ ``` ] .diff-rm[ ```scala ​ ​ *Num value ⇓ `value` ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ``` ] .diff-add[ ```scala ​ ​ *Num value ⇓ `Value.Num value` ​ ​ ​ ​ ``` ] --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` ```scala lhs ⇓ v₁ rhs ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ ​`Add lhs rhs` ⇓ v₁ + v₂ ​ ​ ​ ​ ``` --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` .diff-rm[ ```scala *lhs ⇓ `v₁` rhs ⇓ `v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ​ ​ ​ ​ ``` ] --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` .diff-add[ ```scala *lhs ⇓ `Value.Num v₁` rhs ⇓ `Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ v₁ + v₂ ​ ​ ​ ​ ``` ] --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` .diff-rm[ ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Add lhs rhs ⇓ `v₁ + v₂` ​ ​ ​ ​ ``` ] --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` .diff-add[ ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Add lhs rhs ⇓ `Value.Num (v₁ + v₂)` ​ ​ ​ ​ ``` ] --- ```scala def add(lhs: Expr, rhs: Expr) = val v1 = interpret(lhs) val v2 = interpret(rhs) ​ v1 + v2 ​ ``` ```scala lhs ⇓ `Value.Num v₁` rhs ⇓ `Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- .diff-rm[ ```scala def add(lhs: Expr, rhs: Expr) = * `val v1 = interpret(lhs)` * `val v2 = interpret(rhs)` *​ * `v1 + v2` ​ ``` ] ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- .diff-add[ ```scala def add(lhs: Expr, rhs: Expr) = * `(interpret(lhs), interpret(rhs)) match` * `case (Value.Num(v1), Value.Num(v2)) => ???` ​ ​ ​ ``` ] ```scala ​`lhs ⇓ Value.Num v₁` `rhs ⇓ Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- ```scala def add(lhs: Expr, rhs: Expr) = (`interpret(lhs)`, interpret(rhs)) match case (`Value.Num(v1)`, Value.Num(v2)) => ??? ​ ​ ​ ``` ```scala ​`lhs ⇓ Value.Num v₁` rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- ```scala def add(lhs: Expr, rhs: Expr) = (interpret(lhs), `interpret(rhs)`) match case (Value.Num(v1), `Value.Num(v2)`) => ??? ​ ​ ​ ``` ```scala lhs ⇓ Value.Num v₁ `rhs ⇓ Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- .diff-rm[ ```scala def add(lhs: Expr, rhs: Expr) = (interpret(lhs), interpret(rhs)) match * case (Value.Num(v1), Value.Num(v2)) => `???` ​ ​ ​ ``` ] ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ `Value.Num (v₁ + v₂)` ​ ​ ​ ​ ``` --- .diff-add[ ```scala def add(lhs: Expr, rhs: Expr) = (interpret(lhs), interpret(rhs)) match * case (Value.Num(v1), Value.Num(v2)) => `Value.Num(v1 + v2)` ​ ​ ​ ``` ] ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ `Value.Num (v₁ + v₂)` ​ ​ ​ ​ ``` --- .diff-add[ ```scala 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")` ​ ​ ``` ] ```scala lhs ⇓ Value.Num v₁ rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs ⇓ Value.Num (v₁ + v₂) ​ ​ ​ ​ ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) else interpret(onF) ​ ​ ​ ``` ```scala pred ⇓ true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond pred onT onF` ⇓ v ​ pred ⇓ false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond pred onT onF` ⇓ v ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) else interpret(onF) ​ ​ ​ ``` .diff-add[ ```scala *pred ⇓ `Value.Bool` true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ *pred ⇓ `Value.Bool` false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` ] --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) else interpret(onF) ​ ​ ​ ``` ```scala pred ⇓ Value.Bool true onT ⇓ `v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false onF ⇓ `v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = if interpret(pred) then interpret(onT) else interpret(onF) ​ ​ ​ ``` ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ``` --- .diff-rm[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * `if interpret(pred) then interpret(onT)` * `else interpret(onF)` ​ ​ ​ ``` ] ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = * `interpret(pred) match` ​ ​ ​ ​ ``` ] ```scala ​`pred` ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ ​`pred` ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match * `case Value.Bool(true) => ???` ​ ​ ​ ``` ] ```scala pred ⇓ `Value.Bool true` onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-rm[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match * case Value.Bool(true) => `???` ​ ​ ​ ``` ] ```scala pred ⇓ Value.Bool true `onT ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match * case Value.Bool(true) => `interpret(onT)` ​ ​ ​ ``` ] ```scala pred ⇓ Value.Bool true `onT ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match case Value.Bool(true) => interpret(onT) * `case Value.Bool(false) => ???` ​ ​ ``` ] ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ `Value.Bool false` onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- .diff-rm[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match case Value.Bool(true) => interpret(onT) * case Value.Bool(false) => `???` ​ ​ ``` ] ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false `onF ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ``` --- .diff-add[ ```scala def cond(pred: Expr, onT: Expr, onF: Expr) = interpret(pred) match case Value.Bool(true) => interpret(onT) * case Value.Bool(false) => `interpret(onF)` ​ ​ ``` ] ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false `onF ⇓ v` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ `v` ``` --- .diff-add[ ```scala 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")` ​ ``` ] ```scala pred ⇓ Value.Bool true onT ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ​ pred ⇓ Value.Bool false onF ⇓ v ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF ⇓ v ``` --- ```ocaml if true then 1 else 2 ​ ​ ​ ​ ``` ```scala ​ ​ ​ ``` --- ```ocaml if `true` then 1 else 2 ​ ​ ​ ​ ``` ```scala ​ ​ ​ ``` --- ```ocaml if `true` then 1 else 2 ​ ​ ​ ​ ``` ```scala ​ ​ ​`Bool` ⇓ ??? ``` --- ```ocaml if `true` then 1 else 2 ​ ​ ​ ​ ``` .diff-add[ ```scala ​ ​ *Bool `value` ⇓ ??? ``` ] --- ```ocaml if true then 1 else 2 ​ ​ ​ ​ ``` .diff-rm[ ```scala ​ ​ *Bool value ⇓ `???` ``` ] --- ```ocaml if true then 1 else 2 ​ ​ ​ ​ ``` .diff-add[ ```scala ​ ​ *Bool value ⇓ `Value.Bool value` ``` ] --- ```scala enum Expr: case Num(value: Int) case Add(lhs: Expr, rhs: Expr) case Cond(pred: Expr, onT: Expr, onF: Expr) ​ ​ ``` ```scala ​ ​ Bool value ⇓ Value.Bool value ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) * `case Bool()` case Add(lhs: Expr, rhs: Expr) case Cond(pred: Expr, onT: Expr, onF: Expr) ​ ``` ] ```scala ​ ​ ​`Bool` value ⇓ Value.Bool value ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) * case Bool(`value: Boolean`) case Add(lhs: Expr, rhs: Expr) case Cond(pred: Expr, onT: Expr, onF: Expr) ​ ``` ] ```scala ​ ​ Bool `value` ⇓ Value.Bool value ``` --- ```scala 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) ​ ​ ``` ```scala ​ ​ Bool value ⇓ Value.Bool value ``` --- .diff-add[ ```scala 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) ​ ``` ] ```scala ​ ​ ​`Bool value` ⇓ Value.Bool value ``` --- .diff-rm[ ```scala 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) ​ ``` ] ```scala ​ ​ Bool value ⇓ `Value.Bool value` ``` --- .diff-add[ ```scala 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) ​ ``` ] ```scala ​ ​ Bool value ⇓ `Value.Bool value` ``` --- ```ocaml if true then 1 else 2 ``` ```scala val expr = ??? ​ ​ ​ ​ ``` ```scala interpret(expr) ``` --- ```ocaml ​`if` true then 1 else 2 ``` .diff-rm[ ```scala *val expr = `???` ​ ​ ​ ​ ``` ] ```scala interpret(expr) ``` --- ```ocaml ​`if` true then 1 else 2 ``` .diff-add[ ```scala *val expr = `Cond(` *​`)` ​ ​ ​ ``` ] ```scala interpret(expr) ``` --- ```ocaml if `true` then 1 else 2 ``` .diff-add[ ```scala val expr = Cond( * `pred = Bool(true)` ) ​ ​ ``` ] ```scala interpret(expr) ``` --- ```ocaml if true `then 1` else 2 ``` .diff-add[ ```scala val expr = Cond( * pred = Bool(true)`,` * `onT = Num(1)` ) ​ ``` ] ```scala interpret(expr) ``` --- ```ocaml if true then 1 `else 2` ``` .diff-add[ ```scala val expr = Cond( pred = Bool(true), onT = Num(1)`,` * `onF = Num(2)` ) ``` ] ```scala interpret(expr) ``` --- ```ocaml if true then 1 else 2 ``` ```scala val expr = Cond( pred = Bool(true), onT = Num(1), onF = Num(2) ) ``` ```scala interpret(expr) // val res2: Value = Num(1) ``` --- ## [Key takeaways](#conclusion) -- * Conditionals are straightforward to support -- * They forced us to support multiple types of values -- * Friends don't let friends implement truthiness --- class: center, middle name: bindings # Naming things --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 ​ x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml ​`let` x = 1 ​ x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml x ​ let x = 1 ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 `in` x + 2 ​ ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let `x = 1` in x + 2 ​ ``` --- .diff-add[ ```ocaml *​`x = 1` ​ ``` ] <hr/> ```ocaml let `x = 1` in x + 2 ​ ``` --- ```ocaml x = 1 ​ ``` <hr/> ```ocaml let x = 1 in `x + 2` ​ ``` --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in `x` + 2 ​ ``` ] --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `1` + 2 ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * `1 + 2` ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `3` ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> .diff-rm[ ```ocaml *​`let x = 1 in` * `3` ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> .diff-add[ ```ocaml *​`3` ​ ​ ``` ] --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 + 2 in if true then 1 else x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let `x = 1 + 2` in if true then 1 else x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 + 2 in if `true` then 1 else x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 + 2 in if true then `1` else x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 + 2 in if true then 1 else `x` ``` --- ```ocaml ​ ​ ``` <hr/> .diff-rm[ ```ocaml *let x = `1 + 2` in if true then 1 else x ``` ] --- ```ocaml ​ ​ ``` <hr/> .diff-add[ ```ocaml *let x = `3` in if true then 1 else x ``` ] --- ```ocaml ​ ​ ``` <hr/> ```ocaml let `x = 3` in if true then 1 else x ``` --- .diff-add[ ```ocaml *​`x = 3` ​ ``` ] <hr/> ```ocaml let `x = 3` in if true then 1 else x ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 in x + (let x = 2 in x) ​ ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let `x = 1` in x + (let x = 2 in x) ​ ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 in `x` + (let x = 2 in x) ​ ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 in x + (let `x = 2` in x) ​ ``` --- ```ocaml ​ ​ ``` <hr/> ```ocaml let x = 1 in x + (let x = 2 in `x`) ​ ``` --- ```ocaml ​ ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * `x` + `(let x = 2 in x)` ​ ``` ] --- ```ocaml ​ ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `(let x = 2 in x)` + `x` ​ ``` ] --- ```ocaml ​ ​ ``` <hr/> ```ocaml let `x = 1` in (let x = 2 in x) + x ​ ``` --- .diff-add[ ```ocaml ​`x = 1` ​ ``` ] <hr/> ```ocaml let x = 1 in `(let x = 2 in x) + x` ​ ``` --- ```ocaml x = 1 ​ ``` <hr/> ```ocaml let x = 1 in (let `x = 2` in x) + x ​ ``` --- .diff-rm[ ```ocaml *x = `1` ​ ``` ] <hr/> ```ocaml let x = 1 in (let `x = 2` in x) + x ​ ``` --- .diff-add[ ```ocaml *x = `2` ​ ``` ] <hr/> ```ocaml let x = 1 in (let `x = 2` in x) + x ​ ``` --- ```ocaml ​`x = 2` ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * (let x = 2 in `x`) + x ​ ``` ] --- ```ocaml ​`x = 2` ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * (let x = 2 in `2`) + x ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * `(let x = 2 in 2)` + x ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `2` + x ​ ``` ] --- ```ocaml ​`x = 2` ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * 2 + `x` ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * 2 + `2` ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * `2 + 2` ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `4` ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-rm[ ```ocaml *​`let x = 1 in` * `4` ​ ``` ] --- ```ocaml x = 2 ​ ``` <hr/> .diff-add[ ```ocaml *​`4` ​ ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> ```ocaml let x = 1 in (let `x = 2` in x) + x ​ ``` --- .diff-add[ ```ocaml x = 1 ​`x = 2` ``` ] <hr/> ```ocaml let x = 1 in (let `x = 2` in x) + x ​ ``` --- ```ocaml x = 1 ​`x = 2` ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * (let x = 2 in `x`) + x ​ ``` ] --- ```ocaml x = 1 ​`x = 2` ``` <hr/> .diff-add[ ```ocaml let x = 1 in * (let x = 2 in `2`) + x ​ ``` ] --- .diff-rm[ ```ocaml x = 1 *​`x = 2` ``` ] <hr/> .diff-rm[ ```ocaml let x = 1 in * `(let x = 2 in 2)` + x ​ ``` ] --- ```ocaml x = 1 ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in * `2` + x ​ ``` ] --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in * 2 + `x` ​ ``` ] --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in 2 + `1` ​ ``` ] --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-rm[ ```ocaml let x = 1 in `2 + 1` ​ ``` ] --- ```ocaml ​`x = 1` ​ ``` <hr/> .diff-add[ ```ocaml let x = 1 in `3` ​ ``` ] --- .diff-rm[ ```ocaml *​`x = 1` ​ ``` ] <hr/> .diff-rm[ ```ocaml *​`let x = 1 in` * `3` ​ ``` ] --- ```ocaml ​ ​ ``` <hr/> .diff-add[ ```ocaml *​`3` ​ ​ ``` ] --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Let` ⇓ ??? ``` ```ocaml ​`let` x = 1 in x + 2 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Let `name` ⇓ ??? ``` ] ```ocaml let `x` = 1 in x + 2 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Let name `value` ⇓ ??? ``` ] ```ocaml let x = `1` in x + 2 ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Let name value `body` ⇓ ??? ``` ] ```ocaml let x = 1 in `x + 2` ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name `value` body ⇓ ??? ``` ```ocaml let x = `1` in x + 2 ``` --- .diff-add[ ```scala *​`value ⇓ v₁` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name value body ⇓ ??? ``` ] ```ocaml let x = `1` in x + 2 ``` --- ```scala value ⇓ v₁ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name value `body` ⇓ ??? ``` ```ocaml let x = 1 in `x + 2` ``` --- .diff-add[ ```scala *​`e |-` value ⇓ v₁ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * `e |-` Let name value body ⇓ ??? ``` ] ```ocaml let x = 1 in x + 2 ``` --- ```scala ​`e |- value ⇓ v₁` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ ??? ``` ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala *e |- value ⇓ v₁ `??? |- body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ ??? ``` ] ```ocaml let x = 1 in `x + 2` ``` --- .diff-rm[ ```scala e |- value ⇓ v₁ `???` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ ??? ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala *e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ ??? ``` ] ```ocaml let `x = 1` in x + 2 ``` --- .diff-rm[ ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Let name value body ⇓ `???` ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Let name value body ⇓ `v₂` ``` ] ```ocaml let x = 1 in x + 2 ``` --- ```scala ​ ​ e |- `Ref` ⇓ ??? ``` ```ocaml let x = 1 in `x` + 2 ``` --- .diff-add[ ```scala ​ ​ *e |- Ref `name` ⇓ ??? ``` ] ```ocaml let x = 1 in `x` + 2 ``` --- .diff-rm[ ```scala ​ ​ *​e |- Ref name ⇓ `???` ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala ​ ​ *​e |- Ref name ⇓ `lookup(e, name)` ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala enum Expr: case Num(value: Int) case Bool(value: Boolean) case Add(lhs: Expr, rhs: Expr) case Cond(pred: Expr, onT: Expr, onF: Expr) ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Let name value body` ⇓ v₂ ``` --- .diff-add[ ```scala 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()` ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Let` name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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`) ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let `name` value body ⇓ v₂ ``` --- .diff-add[ ```scala 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`) ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name `value` body ⇓ v₂ ``` --- .diff-add[ ```scala 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`) ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value `body` ⇓ v₂ ``` --- ```scala 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) ​ ``` ```scala ​ ​ e |- `Ref name` ⇓ lookup(e, name) ``` --- .diff-add[ ```scala 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()` ``` ] ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Ref` name ⇓ lookup(e, name) ``` --- .diff-add[ ```scala 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`) ``` ] ```scala ​ ​ e |- Ref `name` ⇓ lookup(e, name) ``` --- ```scala 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`) ``` ```scala ​ ​ e |- Ref name ⇓ lookup(e, name) ``` --- ```scala 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) ``` ```scala ​ ​ ​`e` |- Ref name ⇓ lookup(e, name) ``` --- ```scala case class Env(): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala ​ ​ ​ ``` --- .diff-add[ ```scala *case class Env(`env: List[???]`): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-rm[ ```scala *case class Env(env: List[`???`]): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala *case class Env(env: List[`Env.Binding`]): ​ *​`object Env:` * `case class Binding()` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala case class Env(env: List[Env.Binding]): ​ object Env: * case class Binding(`name: String`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala case class Env(env: List[Env.Binding]): ​ object Env: * case class Binding(name: String`, value: Value`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala case class Env(env: List[Env.Binding]): * `def lookup(name: String) = ???` ​ object Env: case class Binding(name: String, value: Value) ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-rm[ ```scala case class Env(env: List[Env.Binding]): * def lookup(name: String) = `???` ​ object Env: case class Binding(name: String, value: Value) ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-add[ ```scala case class Env(env: List[Env.Binding]): def lookup(name: String) = * `env.find(_.name == name)` ​ object Env: case class Binding(name: String, value: Value) ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-add[ ```scala 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) ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-add[ ```scala 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) ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-add[ ```scala 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) ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-rm[ ```scala 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) ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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)` ``` ] ```scala ​ ​ ​ ``` --- ```scala 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) ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala ​ ​ ​ ``` --- .diff-add[ ```scala *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`) ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala 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) => ???` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Let name value body` ⇓ v₂ ``` --- .diff-rm[ ```scala 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) => `???` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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)` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- ```scala def let(name: String, value: Expr, body: Expr, e: Env) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-rm[ ```scala *def let(name: String, value: Expr, body: Expr, e: Env) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala def let(name: String, value: Expr, body: Expr, e: Env) = * `val v1 = interpret(value, e)` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`e |- value ⇓ v₁` bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala def let(name: String, value: Expr, body: Expr, e: Env) = val v1 = interpret(value, e) * `val v2 = interpret(body, ???)` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- `body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-rm[ ```scala def let(name: String, value: Expr, body: Expr, e: Env) = val v1 = interpret(value, e) * val v2 = interpret(body, `???`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala def let(name: String, value: Expr, body: Expr, e: Env) = val v1 = interpret(value, e) * val v2 = interpret(body, `e.bind(name, v1)`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ `bind(e, name, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ v₂ ``` --- .diff-add[ ```scala def let(name: String, value: Expr, body: Expr, e: Env) = val v1 = interpret(value, e) val v2 = interpret(body, e.bind(name, v1)) ​ * `v2` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- value ⇓ v₁ bind(e, name, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Let name value body ⇓ `v₂` ``` --- ```scala 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) ​ ​ ​ ​ ​ ​ ​ ``` ```scala ​ ​ e |- `Ref name` ⇓ lookup(e, name) ``` --- .diff-add[ ```scala 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) => ???` ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- `Ref name` ⇓ lookup(e, name) ``` --- .diff-rm[ ```scala 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) => `???` ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- .diff-add[ ```scala 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)` ​ ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ e |- Ref name ⇓ `lookup(e, name)` ``` --- ```ocaml let x = 1 in (let x = 2 in x) + x ``` ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml ​`let` x = 1 in (let x = 2 in x) + x ``` .diff-rm[ ```scala *val expr = `???` ​ ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml ​`let` x = 1 in (let x = 2 in x) + x ``` .diff-add[ ```scala *val expr = `Let(` *​`)` ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let `x = 1 in` `(let x = 2 in x) + x` ``` .diff-add[ ```scala val expr = Let( * `[...]` ) ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let x = 1 in (let x = 2 in x) + x ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // val res3: Value = Num(3) ``` --- ## [Key takeaways](#conclusion) -- * Local bindings have a scope that can be analyzed statically -- * They can shadowed, but not overwritten -- * Their interpretation requires an environment --- class: center, middle name: functions # Reusing Code --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let x = 1 in x + 2 ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let x = 1 in `x + 2` ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let `x = 1` in x + 2 ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> .diff-rm[ ```ocaml *​`let x = 1 in` * `x + 2` ​ ​ ``` ] --- ```ocaml ​ ​ ​ ``` <hr/> .diff-add[ ```ocaml *​`(x -> x + 2) 1` ​ ​ ​ ``` ] --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml ​`(x -> x + 2)` 1 ​ ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml (x -> x + 2) `1` ​ ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> .diff-rm[ ```ocaml *​`(x -> x + 2) 1` ​ ​ ​ ``` ] --- .diff-add[ ```ocaml *​`x = 1` ​ ​ ``` ] <hr/> .diff-add[ ```ocaml *​`x + 2` ​ ​ ​ ``` ] --- ```ocaml ​`x = 1` ​ ​ ``` <hr/> .diff-rm[ ```ocaml *​`x` + 2 ​ ​ ​ ``` ] --- ```ocaml ​`x = 1` ​ ​ ``` <hr/> .diff-add[ ```ocaml *​`1` + 2 ​ ​ ​ ``` ] --- ```ocaml x = 1 ​ ​ ``` <hr/> .diff-rm[ ```ocaml *​`1 + 2` ​ ​ ​ ``` ] --- ```ocaml x = 1 ​ ​ ``` <hr/> .diff-add[ ```ocaml *​`3` ​ ​ ​ ``` ] --- ```ocaml ​ ​ ​ ``` <hr/> .diff-add[ ```ocaml let f = x -> x + 2 in f 1 ​ ​ ``` ] --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let f = `x -> x + 2` in f 1 ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let `f` = x -> x + 2 in f 1 ​ ​ ``` --- ```ocaml ​ ​ ​ ``` <hr/> ```ocaml let f = x -> x + 2 in `f 1` ​ ​ ``` --- ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) ​ ``` ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) * `case Fun()` ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) * case Fun(`param: String`) ``` ] ```ocaml let f = `x` -> x + 2 in f 1 ``` --- .diff-add[ ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) * case Fun(param: String`, body: Expr`) ``` ] ```ocaml let f = x -> `x + 2` in f 1 ``` --- ```ocaml ​ ​ ​ ​ ``` <hr/> ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` --- ```ocaml ​ ​ ​ ​ ``` <hr/> ```ocaml let `y = 1` in let f = x -> x + y in let y = 2 in f 3 ``` --- ```ocaml ​ ​ ​ ​ ``` <hr/> ```ocaml let y = 1 in let `f = x -> x + y` in let y = 2 in f 3 ``` --- ```ocaml ​ ​ ​ ​ ``` <hr/> ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in `f 3` ``` --- ```ocaml ​ ​ ​ ​ ``` <hr/> ```ocaml let `y = 1` in let f = x -> x + y in let y = 2 in f 3 ``` --- .diff-add[ ```ocaml *​`y = 1` ​ ​ ​ ``` ] <hr/> ```ocaml let `y = 1` in let f = x -> x + y in let y = 2 in f 3 ``` --- ```ocaml y = 1 ​ ​ ​ ``` <hr/> ```ocaml let y = 1 in let `f = x -> x + y` in let y = 2 in f 3 ``` --- .diff-add[ ```ocaml y = 1 *​`f = x -> x + y` ​ ​ ``` ] <hr/> ```ocaml let y = 1 in let `f = x -> x + y` in let y = 2 in f 3 ``` --- ```ocaml y = 1 f = x -> x + y ​ ​ ``` <hr/> ```ocaml let y = 1 in let f = x -> x + y in let `y = 2` in f 3 ``` --- .diff-add[ ```ocaml y = 1 f = x -> x + y *​`y = 2` ​ ``` ] <hr/> ```ocaml let y = 1 in let f = x -> x + y in let `y = 2` in f 3 ``` --- ```ocaml y = 1 f = x -> x + y y = 2 ​ ``` <hr/> .diff-rm[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `f 3` ``` ] --- .diff-add[ ```ocaml y = 1 f = x -> x + y y = 2 *​`x = 3` ``` ] <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `x + y` ``` ] --- .diff-rm[ ```ocaml y = 1 f = x -> x + y y = 2 *​`x = 3` ``` ] <hr/> .diff-rm[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `x` + y ``` ] --- ```ocaml y = 1 f = x -> x + y y = 2 ​ ``` <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `3` + y ``` ] --- ```ocaml y = 1 f = x -> x + y ​`y = 2` ​ ``` <hr/> .diff-rm[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * 3 + `y` ``` ] --- ```ocaml y = 1 f = x -> x + y ​`y = 2` ​ ``` <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * 3 + `2` ``` ] --- ```ocaml y = 1 f = x -> x + y y = 2 ​ ``` <hr/> .diff-rm[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `3 + 2` ``` ] --- ```ocaml y = 1 f = x -> x + y y = 2 ​ ``` <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in * `5` ``` ] --- .diff-rm[ ```ocaml y = 1 f = x -> x + y *​`y = 2` ​ ``` ] <hr/> .diff-rm[ ```ocaml let y = 1 in let f = x -> x + y in * `let y = 2 in` * `5` ``` ] --- .diff-rm[ ```ocaml y = 1 f = x -> x + y ​ ​ ``` ] <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in * `5` ​ ``` ] --- .diff-rm[ ```ocaml y = 1 *​`f = x -> x + y` ​ ​ ``` ] <hr/> .diff-rm[ ```ocaml let y = 1 in * `let f = x -> x + y in` * `5` ​ ``` ] --- .diff-rm[ ```ocaml y = 1 ​ ​ ​ ``` ] <hr/> .diff-add[ ```ocaml let y = 1 in * `5` ​ ​ ``` ] --- .diff-rm[ ```ocaml *​`y = 1` ​ ​ ​ ``` ] <hr/> .diff-rm[ ```ocaml *​`let y = 1 in` * `5` ​ ​ ``` ] --- .diff-rm[ ```ocaml ​ ​ ​ ​ ``` ] <hr/> .diff-add[ ```ocaml *​`5` ​ ​ ​ ``` ] --- ```ocaml y = 1 f = x -> x + y y = 2 x = 3 ``` <hr/> .diff-add[ ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` ] --- ```ocaml ​`y = 1` f = x -> x + y y = 2 x = 3 ``` <hr/> ```ocaml let `y = 1` in let f = x -> x + y in let y = 2 in f 3 ``` --- ```ocaml y = 1 ​`f = x -> x + y` y = 2 x = 3 ``` <hr/> ```ocaml let y = 1 in let `f = x -> x + y` in let y = 2 in f 3 ``` --- ```ocaml y = 1 f = x -> x + y ​`y = 2` x = 3 ``` <hr/> ```ocaml let y = 1 in let f = x -> x + y in let `y = 2` in f 3 ``` --- ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) case Fun(param: String, body: Expr) ``` --- .diff-add[ ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) * case Fun(param: String, body: Expr`, env: Env`) ``` ] --- ```scala ​ ​ ​ e |- `Fun` ⇓ ??? ``` ```ocaml let `f = x -> x + 2` in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun `param` ⇓ ??? ``` ] ```ocaml let f = `x` -> x + 2 in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun param `body` ⇓ ??? ``` ] ```ocaml let f = x -> `x + 2` in f 1 ``` --- .diff-rm[ ```scala ​ ​ ​ *e |- Fun param body ⇓ `???` ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun param body ⇓ `Value.Fun` ``` ] ```ocaml let f = `x -> x + 2` in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun param body ⇓ Value.Fun `param` ``` ] ```ocaml let f = `x` -> x + 2 in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun param body ⇓ Value.Fun param `body` ``` ] ```ocaml let f = x -> `x + 2` in f 1 ``` --- .diff-add[ ```scala ​ ​ ​ *e |- Fun param body ⇓ Value.Fun param body `e` ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply ⇓ ??? ``` ```ocaml let f = x -> x + 2 in `f 1` ``` --- .diff-add[ ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply `fun` ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in `f` 1 ``` --- .diff-add[ ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun `arg` ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f `1` ``` --- .diff-add[ ```scala *​`e |- fun ⇓ ???` ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in `f` 1 ``` --- .diff-rm[ ```scala *e |- fun ⇓ `???` ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in `f` 1 ``` --- .diff-add[ ```scala *e |- fun ⇓ `Value.Fun param body eʹ` ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in `f` 1 ``` --- .diff-add[ ```scala *e |- fun ⇓ Value.Fun param body eʹ `e |- arg ⇓ v₁` ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f `1` ``` --- .diff-add[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ *​`??? |- body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> `x + 2` in f 1 ``` --- .diff-rm[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ *​`???` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ *​`eʹ` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- ```scala e |- fun ⇓ Value.Fun `param` body eʹ e |- arg ⇓ v₁ eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ```ocaml let f = `x` -> x + 2 in f 1 ``` --- ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ `v₁` eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ```ocaml let f = x -> x + 2 in f `1` ``` --- .diff-rm[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ *​`eʹ` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ *​`bind(eʹ, param, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ ??? ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-rm[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Apply fun arg ⇓ `???` ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- .diff-add[ ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Apply fun arg ⇓ `v₂` ``` ] ```ocaml let f = x -> x + 2 in f 1 ``` --- ```scala 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) ​ ​ ``` ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Fun param body` ⇓ Value.Fun param body E ``` --- .diff-add[ ```scala 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()` ​ ``` ] ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Fun` param body ⇓ Value.Fun param body E ``` --- .diff-add[ ```scala 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`) ​ ``` ] ```scala ​ ​ ​ e |- Fun `param` body ⇓ Value.Fun param body E ``` --- .diff-add[ ```scala 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`) ​ ``` ] ```scala ​ ​ ​ e |- Fun param `body` ⇓ Value.Fun param body E ``` --- ```scala 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) ​ ``` ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Apply fun arg` ⇓ v₂ ``` --- .diff-add[ ```scala 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()` ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Apply` fun arg ⇓ v₂ ``` --- .diff-add[ ```scala 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`) ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply `fun` arg ⇓ v₂ ``` --- .diff-add[ ```scala 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`) ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun `arg` ⇓ v₂ ``` --- ```scala 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) ​ ​ ``` ```scala ​ ​ ​ e |- `Fun param body` ⇓ Value.Fun param body E ``` --- .diff-add[ ```scala 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) => ???` ​ ``` ] ```scala ​ ​ ​ e |- `Fun param body` ⇓ Value.Fun param body E ``` --- .diff-rm[ ```scala 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) => `???` ​ ``` ] ```scala ​ ​ ​ e |- Fun param body ⇓ Value.Fun param body E ``` --- .diff-add[ ```scala 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)` ​ ``` ] ```scala ​ ​ ​ e |- Fun param body ⇓ `Value.Fun param body e` ``` --- ```scala 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) ​ ``` ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Apply fun arg` ⇓ v₂ ``` --- .diff-add[ ```scala 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) => ???` ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Apply fun arg` ⇓ v₂ ``` --- .diff-rm[ ```scala 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) => `???` ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala 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)` ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- ```scala def apply(fun: Expr, arg: Expr, e: Env) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-rm[ ```scala *def apply(fun: Expr, arg: Expr, e: Env) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala def apply(fun: Expr, arg: Expr, e: Env) = * `interpret(fun, e) match` * `case Value.Fun(param, body, eʹ) => ???` ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`e |- fun ⇓ Value.Fun param body eʹ` e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-rm[ ```scala def apply(fun: Expr, arg: Expr, e: Env) = interpret(fun, e) match * case Value.Fun(param, body, eʹ) => `???` ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ `e |- arg ⇓ v₁` bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala def apply(fun: Expr, arg: Expr, e: Env) = interpret(fun, e) match case Value.Fun(param, body, eʹ) => * `val v1 = interpret(arg, e)` ​ ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ `e |- arg ⇓ v₁` bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala 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, ???)` ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- `body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-rm[ ```scala 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, `???`) ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ ​`bind(eʹ, param, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala 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)`) ​ ​ ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ ​`bind(eʹ, param, v₁)` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- .diff-add[ ```scala 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` ​ ​ ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ `v₂` ``` --- .diff-add[ ```scala 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")` ``` ] ```scala e |- fun ⇓ Value.Fun param body eʹ e |- arg ⇓ v₁ bind(eʹ, param, v₁) |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Apply fun arg ⇓ v₂ ``` --- ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml ​`let` y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` .diff-rm[ ```scala *val expr = `???` ​ ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml ​`let` y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` .diff-add[ ```scala *val expr = `Let(` *​`)` ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let `y = 1 in` `let f = x -> x + y in` `let y = 2 in` `f 3` ``` .diff-add[ ```scala val expr = Let( * `[...]` ) ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let y = 1 in let f = x -> x + y in let y = 2 in f 3 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // val res4: Value = Num(4) ``` --- ```ocaml let add = ??? in add 1 2 ​ ​ ``` ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- .diff-rm[ ```ocaml *let add = `???` in add 1 2 ​ ​ ``` ] ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- .diff-add[ ```ocaml *let add = `x -> ???` in add 1 2 ​ ​ ``` ] ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- .diff-rm[ ```ocaml *let add = x -> `???` in add 1 2 ​ ​ ``` ] ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- .diff-add[ ```ocaml *let add = x -> `y -> x + y` in add 1 2 ​ ​ ``` ] ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml let add = x -> y -> x + y in add 1 2 ​ ​ ``` .diff-rm[ ```scala *val expr = `???` ​ ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let add = x -> y -> x + y in add 1 2 ​ ​ ``` .diff-add[ ```scala *val expr = `Let(` * `[...]` *​`)` ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let add = x -> y -> x + y in add 1 2 ​ ​ ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // val res5: Value = Num(3) ``` --- ## [Key takeaways](#conclusion) -- * Functions are values -- * They _close_ over their environment -- * Yes, unary functions are sufficient --- class: center, middle name: recursion # Repeating actions --- ```ocaml let `sumFor` = lower -> upper -> var acc = 0 for i = lower to upper do acc = acc + i acc in sumFor 1 10 ​ ​ ``` --- ```ocaml let sumFor = `lower -> upper` -> var acc = 0 for i = lower to upper do acc = acc + i acc in sumFor 1 10 ​ ​ ``` --- ```ocaml let sumFor = lower -> upper -> `var acc = 0` for i = lower to upper do acc = acc + i acc in sumFor 1 10 ​ ​ ``` --- ```ocaml let sumFor = lower -> upper -> var acc = 0 `for i = lower to upper do` acc = acc + i acc in sumFor 1 10 ​ ​ ``` --- ```ocaml let sumFor = lower -> upper -> var acc = 0 for i = lower to upper do `acc = acc + i` acc in sumFor 1 10 ​ ​ ``` --- ```ocaml let sumFor = lower -> upper -> var acc = 0 for i = lower to upper do acc = acc + i `acc` in sumFor 1 10 ​ ​ ``` --- .diff-rm[ ```ocaml *let `sumFor` = lower -> upper -> var acc = 0 for i = lower to upper do acc = acc + i acc * in `sumFor` 1 10 ​ ​ ``` ] --- .diff-add[ ```ocaml *let `sumWhile` = lower -> upper -> var acc = 0 for i = lower to upper do acc = acc + i acc * in `sumWhile` 1 10 ​ ​ ``` ] --- ```ocaml let sumWhile = lower -> upper -> var acc = 0 for `i = lower to upper` do acc = acc + i acc in sumWhile 1 10 ​ ​ ``` --- .diff-add[ ```ocaml let sumWhile = lower -> upper -> var acc = 0 * `var i = lower` for i = lower to upper do acc = acc + i acc in sumWhile 1 10 ​ ``` ] --- .diff-add[ ```ocaml 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 ``` ] --- .diff-rm[ ```ocaml 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 ``` ] --- .diff-add[ ```ocaml 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 ``` ] --- .diff-rm[ ```ocaml *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 ``` ] --- .diff-add[ ```ocaml *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 ``` ] --- ```ocaml 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 ``` --- .diff-rm[ ```ocaml 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 ``` ] --- .diff-add[ ```ocaml 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 ``` ] --- .diff-rm[ ```ocaml 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 ``` ] --- .diff-add[ ```ocaml 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 ​ ​ ``` ] --- .diff-rm[ ```ocaml 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 ​ ​ ``` ] --- .diff-add[ ```ocaml 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 ​ ​ ``` ] --- .diff-rm[ ```ocaml *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 ​ ​ ``` ] --- .diff-add[ ```ocaml *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 ​ ​ ``` ] --- .diff-rm[ ```ocaml 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 ​ ​ ``` ] --- .diff-add[ ```ocaml let sum = lower -> upper -> * `if lower > upper then 0` * `else lower + (sum (lower + 1) upper)` in sum 1 10 ​ ​ ​ ​ ``` ] --- ```ocaml let sum = lower -> upper -> `if lower > upper then 0` else lower + (sum (lower + 1) upper) in sum 1 10 ​ ​ ​ ​ ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else `lower` + (sum (lower + 1) upper) in sum 1 10 ​ ​ ​ ​ ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + `(sum (lower + 1) upper)` in sum 1 10 ​ ​ ​ ​ ``` --- ```ocaml let sum = lower -> upper -> if lower `>` upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ​ ​ ​ ​ ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt ⇓ ??? ``` ```ocaml if 1 `>` 2 then false else true ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Gt `lhs` ⇓ ??? ``` ] ```ocaml if `1` > 2 then false else true ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Gt lhs `rhs` ⇓ ??? ``` ] ```ocaml if 1 > `2` then false else true ``` --- .diff-add[ ```scala *​`e |- lhs ⇓ Value.Num v₁` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ ??? ``` ] ```ocaml if `1` > 2 then false else true ``` --- .diff-add[ ```scala *e |- lhs ⇓ Value.Num v₁ `e |- rhs ⇓ Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ ??? ``` ] ```ocaml if 1 > `2` then false else true ``` --- .diff-rm[ ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Gt lhs rhs ⇓ `???` ``` ] ```ocaml if `1 > 2` then false else true ``` --- .diff-add[ ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- Gt lhs rhs ⇓ `Value.Bool (v₁ > v₂)` ``` ] ```ocaml if `1 > 2` then false else true ``` --- ```scala 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) ​ ``` ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Gt lhs rhs` ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Gt` lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt `lhs` rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs `rhs` ⇓ Value.Bool (v₁ > v₂) ``` --- ```scala 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) ​ ``` ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Gt lhs rhs` ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala 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) => ???` 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `Gt lhs rhs` ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-rm[ ```scala 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) => `???` 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala 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) ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- ```scala def gt(lhs: Expr, rhs: Expr, e: Env) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-rm[ ```scala *def gt(lhs: Expr, rhs: Expr, e: Env) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-add[ ```scala def gt(lhs: Expr, rhs: Expr, e: Env) = * `(interpret(lhs, e), interpret(rhs, e)) match` * `case (Value.Num(v1), Value.Num(v2)) => ???` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`e |- lhs ⇓ Value.Num v₁` `e |- rhs ⇓ Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- ```scala def gt(lhs: Expr, rhs: Expr, e: Env) = (`interpret(lhs, e)`, interpret(rhs, e)) match case (`Value.Num(v1)`, Value.Num(v2)) => ??? ​ ​ ​ ​ ​ ​ ​ ``` ```scala ​`e |- lhs ⇓ Value.Num v₁` e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- ```scala def gt(lhs: Expr, rhs: Expr, e: Env) = (interpret(lhs, e), `interpret(rhs, e)`) match case (Value.Num(v1), `Value.Num(v2)`) => ??? ​ ​ ​ ​ ​ ​ ​ ``` ```scala e |- lhs ⇓ Value.Num v₁ `e |- rhs ⇓ Value.Num v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- .diff-rm[ ```scala def gt(lhs: Expr, rhs: Expr, e: Env) = (interpret(lhs, e), interpret(rhs, e)) match * case (Value.Num(v1), Value.Num(v2)) => `???` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ `Value.Bool (v₁ > v₂)` ``` --- .diff-add[ ```scala 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)` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ `Value.Bool (v₁ > v₂)` ``` --- .diff-add[ ```scala 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")` ​ ​ ​ ​ ​ ​ ``` ] ```scala e |- lhs ⇓ Value.Num v₁ e |- rhs ⇓ Value.Num v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- Gt lhs rhs ⇓ Value.Bool (v₁ > v₂) ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ```scala val expr = ??? ​ ​ ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` .diff-rm[ ```scala *val expr = `???` ​ ​ ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` .diff-add[ ```scala *val expr = `Let(` * `[...]` *​`)` ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // ⛔ Unbound variable: sum ``` --- ```ocaml let `sum` = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // ⛔ Unbound variable: sum ``` --- ```ocaml let sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // ⛔ Unbound variable: sum ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (`sum` (lower + 1) upper) in sum 1 10 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) // ⛔ Unbound variable: sum ``` --- ```scala ​ ​ ​ ​ ``` .diff-rm[ ```ocaml ​`let` sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ] --- ```scala ​ ​ ​ ​ ``` .diff-add[ ```ocaml *​`let rec` sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ] --- ```scala enum Value: case Num(value: Int) case Bool(value: Boolean) case Fun(param: String, `body: Expr, env: Env`) ``` ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- ```scala ​ ​ ​ ​ ``` ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `LetRec` ⇓ ??? ``` ```ocaml ​`let rec` sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-add[ ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- LetRec `name` ⇓ ??? ``` ] ```ocaml let rec `sum` = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-add[ ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- LetRec name `value` ⇓ ??? ``` ] ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala ​ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- LetRec name value `body` ⇓ ??? ``` ] ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-add[ ```scala *​`e |- value ⇓ v₁` ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- ```scala ​`e` |- value ⇓ v₁ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala *​`eʹ = bind(e, name, ∅);` e |- value ⇓ v₁ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-rm[ ```scala *eʹ = bind(e, name, ∅); `e` |- value ⇓ v₁ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala *eʹ = bind(e, name, ∅); `eʹ` |- value ⇓ v₁ ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = `lower -> upper ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ * `eʹ |- body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ `eʹ` |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-add[ ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ * `update(eʹ, name, v₁);` eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ ??? ``` ] ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-rm[ ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- LetRec name value body ⇓ `???` ``` ] ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-add[ ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * e |- LetRec name value body ⇓ `v₂` ``` ] ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- ```scala 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) ​ ``` ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `LetRec name value body` ⇓ v₂ ``` --- .diff-add[ ```scala 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) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `LetRec` name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec `name` value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name `value` body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value `body` ⇓ v₂ ``` --- ```scala 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) ``` ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ `update(eʹ, name, v₁)`; eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- ```scala 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) ​ ​ ​ ​ ``` --- .diff-add[ ```scala 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) ​ ​ ``` ] --- .diff-rm[ ```scala 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) ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ``` ] --- .diff-add[ ```scala 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) ``` ] --- .diff-rm[ ```scala 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) ``` ] --- .diff-add[ ```scala 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) ``` ] --- ```scala 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) ​ ``` ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `LetRec name value body` ⇓ v₂ ``` --- .diff-add[ ```scala 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) => ???` case Ref(name) => e.lookup(name) case Fun(param, body) => Value.Fun(param, body, e) case Apply(fun, arg) => apply(fun, arg, e) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- `LetRec name value body` ⇓ v₂ ``` --- .diff-rm[ ```scala 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) => `???` case Ref(name) => e.lookup(name) case Fun(param, body) => Value.Fun(param, body, e) case Apply(fun, arg) => apply(fun, arg, e) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala 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) ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- ```scala def letRec(name: String, value: Expr, body: Expr, e: Env) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-rm[ ```scala *def letRec(name: String, value: Expr, body: Expr, e: Env) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala ​def letRec(name: String, value: Expr, body: Expr, e: Env) = * `val eʹ = e.bind(name, null)` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`eʹ = bind(e, name, ∅)`; eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala ​def letRec(name: String, value: Expr, body: Expr, e: Env) = val eʹ = e.bind(name, null) * `val v1 = interpret(value, eʹ)` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala eʹ = bind(e, name, ∅); `eʹ |- value ⇓ v₁` update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala ​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)` ​ ​ ​ ​ ​ ​ ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ `update(eʹ, name, v₁)`; eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala ​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ʹ)` ​ ​ ​ ​ ​ ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); `eʹ |- body ⇓ v₂` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ v₂ ``` --- .diff-add[ ```scala ​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` ​ ​ ​ ``` ] ```scala eʹ = bind(e, name, ∅); eʹ |- value ⇓ v₁ update(eʹ, name, v₁); eʹ |- body ⇓ v₂ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ e |- LetRec name value body ⇓ `v₂` ``` --- ```ocaml let sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ```scala val expr = Let( [...] ) ``` ```scala interpret(expr, Env.empty) ``` --- .diff-rm[ ```ocaml *​`let` sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ] .diff-rm[ ```scala *val expr = `Let`( [...] ) ``` ] ```scala interpret(expr, Env.empty) ``` --- .diff-add[ ```ocaml *​`let rec` sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ] .diff-add[ ```scala *val expr = `LetRec`( [...] ) ``` ] ```scala interpret(expr, Env.empty) ``` --- ```ocaml let rec sum = lower -> upper -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ```scala val expr = LetRec( [...] ) ``` ```scala interpret(expr, Env.empty) // val res6: Value = Num(55) ``` --- ## [Key takeaways](#conclusion) -- * Loops are implemented as recursive functions -- * Recursive functions need special syntax... -- * ... and a mutable environment --- class: center, middle name: typechecking # Identifying invalid programs --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml 1 `+` true ``` ```scala val expr = `Add`( Num(1), Bool(true) ) ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml ​`1` + true ``` ```scala val expr = Add( `Num(1)`, Bool(true) ) ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml 1 + `true` ``` ```scala val expr = Add( Num(1), `Bool(true)` ) ``` ```scala interpret(expr, Env.empty) ``` --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala interpret(expr, Env.empty) // ⛔ Type error in add ``` --- ```scala def typeCheck(expr: Expr): ??? = ??? ``` --- ```scala def typeCheck(`expr: Expr`): ??? = ??? ``` --- .diff-rm[ ```scala *def typeCheck(expr: Expr): `???` = ??? ``` ] --- .diff-add[ ```scala *def typeCheck(expr: Expr): `Boolean` = ??? ``` ] --- .diff-rm[ ```scala *def typeCheck(expr: Expr): Boolean = `???` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = * `expr match` * `case Num(value) => ???` ``` ] --- .diff-rm[ ```scala def typeCheck(expr: Expr): Boolean = expr match * case Num(value) => `???` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = expr match * case Num(value) => `true` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true * `case Bool(value) => ???` ``` ] --- .diff-rm[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true * case Bool(value) => `???` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true * case Bool(value) => `true` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true case Bool(value) => true * `case Add(lhs, rhs) => ???` ``` ] --- .diff-rm[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true case Bool(value) => true * case Add(lhs, rhs) => `???` ``` ] --- .diff-add[ ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true case Bool(value) => true * case Add(lhs, rhs) => `typeCheck(lhs) && typeCheck(rhs)` ``` ] --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala interpret(expr, Env.empty) ​ ``` --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` .diff-rm[ ```scala *​`interpret(expr, Env.empty)` ​ ``` ] --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` .diff-add[ ```scala *​`typeCheck(expr)` ​ ``` ] --- ```ocaml 1 + true ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala typeCheck(expr) // val res7: Boolean = true ``` --- ```scala def typeCheck(expr: Expr): Boolean = expr match case Num(value) => true case Bool(value) => true case Add(lhs, rhs) => `typeCheck(lhs) && typeCheck(rhs)` ``` --- ```scala def typeCheck(expr: Expr): `Boolean` = expr match case Num(value) => true case Bool(value) => true case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs) ``` --- ```scala enum Type: ​ ​ ​ ​ ``` --- .diff-add[ ```scala enum Type: * `case Num` ​ ​ ​ ``` ] --- .diff-add[ ```scala enum Type: case Num * `case Bool` ​ ​ ``` ] --- .diff-rm[ ```scala *def typeCheck(expr: Expr): `Boolean` = expr match case Num(value) => true case Bool(value) => true case Add(lhs, rhs) => typeCheck(lhs) && typeCheck(rhs) ``` ] --- .diff-add[ ```scala *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) ``` ] --- ```scala 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) ``` --- ```scala Num value : ??? ``` ```scala 1 ``` --- ```scala ​`Num value` : ??? ``` ```scala 1 ``` --- ```scala Num value `:` ??? ``` ```scala 1 ``` --- .diff-rm[ ```scala *Num value : `???` ``` ] ```scala 1 ``` --- .diff-add[ ```scala *Num value : `Type.Num` ``` ] ```scala 1 ``` --- .diff-rm[ ```scala 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) ``` ] ```scala Num value : `Type.Num` ``` --- .diff-add[ ```scala 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) ``` ] ```scala Num value : `Type.Num` ``` --- ```scala 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) ``` ```scala ​ ``` --- ```scala Bool value : ??? ``` ```ocaml true ``` --- .diff-rm[ ```scala *Bool value : `???` ``` ] ```ocaml true ``` --- .diff-add[ ```scala *Bool value : `Type.Bool` ``` ] ```ocaml true ``` --- .diff-rm[ ```scala 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) ``` ] ```scala Bool value : `Type.Bool` ``` --- .diff-add[ ```scala 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) ``` ] ```scala Bool value : `Type.Bool` ``` --- ```scala 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)` ``` ```scala ​ ``` --- ```scala Add lhs rhs : ??? ​ ​ ``` ```ocaml 1 + 2 ``` --- .diff-add[ ```scala *​`lhs : Type.Num` Add lhs rhs : ??? ​ ``` ] ```ocaml ​`1` + 2 ``` --- .diff-add[ ```scala *lhs : Type.Num `rhs : Type.Num` Add lhs rhs : ??? ​ ``` ] ```ocaml 1 + `2` ``` --- .diff-add[ ```scala lhs : Type.Num rhs : Type.Num *​`⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯` Add lhs rhs : ??? ``` ] ```ocaml 1 + 2 ``` --- .diff-rm[ ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Add lhs rhs : `???` ``` ] ```ocaml ​`1 + 2` ``` --- .diff-add[ ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Add lhs rhs : `Type.Num` ``` ] ```ocaml ​`1 + 2` ``` --- .diff-rm[ ```scala 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)` ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala 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)` ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- ```scala def checkAdd(lhs: Expr, rhs: Expr) = ??? ​ ​ ​ ​ ​ ``` ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- ```scala def checkAdd(lhs: Expr, rhs: Expr) = ??? ​ ​ ​ ​ ​ ``` ```scala ​`lhs : Type.Num` rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- ```scala def expect() = ??? ​ ​ ​ ​ ​ ``` ```scala ​`lhs : Type.Num` rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala *def expect(`expr: Expr`) = ??? ​ ​ ​ ​ ​ ``` ] ```scala ​`lhs` : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala *def expect(expr: Expr`, expected: Type`) = ??? ​ ​ ​ ​ ​ ``` ] ```scala lhs : `Type.Num` rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-rm[ ```scala *def expect(expr: Expr, expected: Type) = `???` ​ ​ ​ ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def expect(expr: Expr, expected: Type) = * `typeCheck(expr).flatMap: observed =>` ​ ​ ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def expect(expr: Expr, expected: Type) = typeCheck(expr).flatMap: observed => * `if observed == expected then Right(())` ​ ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def expect(expr: Expr, expected: Type) = typeCheck(expr).flatMap: observed => if observed == expected then Right(()) * `else Left(s"Expected $expected, found $observed")` ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- ```scala def checkAdd(lhs: Expr, rhs: Expr) = ??? ​ ​ ​ ​ ​ ``` ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-rm[ ```scala *def checkAdd(lhs: Expr, rhs: Expr) = `???` ​ ​ ​ ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def checkAdd(lhs: Expr, rhs: Expr) = * `for _ <- expect(lhs, Type.Num)` ​ ​ ​ ​ ``` ] ```scala ​`lhs : Type.Num` rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def checkAdd(lhs: Expr, rhs: Expr) = for _ <- expect(lhs, Type.Num) * `_ <- expect(rhs, Type.Num)` ​ ​ ​ ``` ] ```scala lhs : Type.Num `rhs : Type.Num` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : Type.Num ``` --- .diff-add[ ```scala def checkAdd(lhs: Expr, rhs: Expr) = for _ <- expect(lhs, Type.Num) _ <- expect(rhs, Type.Num) * `yield Type.Num` ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Add lhs rhs : `Type.Num` ``` --- .diff-add[ ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : ??? ``` ] ```ocaml 1 > 2 ``` --- .diff-add[ ```scala *​`lhs : Type.Num` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : ??? ``` ] ```ocaml ​`1` > 2 ``` --- .diff-add[ ```scala *lhs : Type.Num `rhs : Type.Num` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : ??? ``` ] ```ocaml 1 > `2` ``` --- .diff-rm[ ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Gt lhs rhs : `???` ``` ] ```ocaml ​`1 > 2` ``` --- .diff-add[ ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Gt lhs rhs : `Type.Bool` ``` ] ```ocaml ​`1 > 2` ``` --- ```scala 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) ​ ``` ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-add[ ```scala 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) => ???` ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Gt lhs rhs` : Type.Bool ``` --- .diff-rm[ ```scala 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) => `???` ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-add[ ```scala 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)` ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- ```scala def checkGt(lhs: Expr, rhs: Expr) = ??? ​ ​ ​ ​ ​ ``` ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-rm[ ```scala *def checkGt(lhs: Expr, rhs: Expr) = `???` ​ ​ ​ ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-add[ ```scala *def checkGt(lhs: Expr, rhs: Expr) = * `for _ <- expect(lhs, Type.Num)` ​ ​ ​ ​ ``` ] ```scala ​`lhs : Type.Num` rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-add[ ```scala def checkGt(lhs: Expr, rhs: Expr) = for _ <- expect(lhs, Type.Num) * `_ <- expect(rhs, Type.Num)` ​ ​ ​ ``` ] ```scala lhs : Type.Num `rhs : Type.Num` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : Type.Bool ``` --- .diff-add[ ```scala def checkGt(lhs: Expr, rhs: Expr) = for _ <- expect(lhs, Type.Num) _ <- expect(rhs, Type.Num) * `yield Type.Bool` ​ ​ ``` ] ```scala lhs : Type.Num rhs : Type.Num ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Gt lhs rhs : `Type.Bool` ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ```ocaml if true then 1 else 2 ``` --- .diff-add[ ```scala *​`pred : Type.Bool` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ] ```ocaml if `true` then 1 else 2 ``` --- .diff-add[ ```scala *pred : Type.Bool `onT : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ] ```ocaml if true then `1` else 2 ``` --- .diff-add[ ```scala *pred : Type.Bool onT : X `onF : ???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ] ```ocaml if true then 1 else `2` ``` --- .diff-rm[ ```scala *pred : Type.Bool onT : X onF : `???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ] ```ocaml if true then 1 else `2` ``` --- .diff-add[ ```scala *pred : Type.Bool onT : X onF : `X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : ??? ``` ] ```ocaml if true then 1 else `2` ``` --- .diff-rm[ ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF : `???` ``` ] ```ocaml ​`if true then 1` `else 2` ``` --- .diff-add[ ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Cond pred onT onF : `X` ``` ] ```ocaml ​`if true then 1` `else 2` ``` --- ```scala 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) ​ ``` ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala 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) => ???` ``` ] ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ `Cond pred onT onF` : X ``` --- .diff-rm[ ```scala 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) => `???` ``` ] ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala 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)` ``` ] ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- ```scala def checkCond(pred: Expr, onT: Expr, onF: Expr) = ??? ​ ​ ​ ​ ​ ​ ``` ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-rm[ ```scala *def checkCond(pred: Expr, onT: Expr, onF: Expr) = `???` ​ ​ ​ ​ ​ ​ ``` ] ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala def checkCond(pred: Expr, onT: Expr, onF: Expr) = * `for _ <- expect(pred, Type.Bool)` ​ ​ ​ ​ ​ ``` ] ```scala ​`pred : Type.Bool` onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala def checkCond(pred: Expr, onT: Expr, onF: Expr) = for _ <- expect(pred, Type.Bool) * `x <- typeCheck(onT)` ​ ​ ​ ​ ``` ] ```scala pred : Type.Bool `onT : X` onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala def checkCond(pred: Expr, onT: Expr, onF: Expr) = for _ <- expect(pred, Type.Bool) x <- typeCheck(onT) * `_ <- expect(onF, x)` ​ ​ ​ ``` ] ```scala pred : Type.Bool onT : X `onF : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : X ``` --- .diff-add[ ```scala def checkCond(pred: Expr, onT: Expr, onF: Expr) = for _ <- expect(pred, Type.Bool) x <- typeCheck(onT) _ <- expect(onF, x) * `yield x` ​ ​ ``` ] ```scala pred : Type.Bool onT : X onF : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Cond pred onT onF : `X` ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name value body : ??? ``` ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala *​`value : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name value body : ??? ``` ] ```ocaml let x = `1` in x + 2 ``` --- .diff-add[ ```scala *value : X `body : Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Let name value body : ??? ``` ] ```ocaml let x = 1 in `x + 2` ``` --- .diff-add[ ```scala *​`Γ |-` value : X `Γ |-` body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * `Γ |-` Let name value body : ??? ``` ] ```ocaml let x = 1 in x + 2 ``` --- ```scala ​`Γ |- value : X` Γ |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : ??? ``` ```ocaml let x = 1 in x + 2 ``` --- .diff-rm[ ```scala *Γ |- value : X `Γ` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : ??? ``` ] ```ocaml let `x = 1` in x + 2 ``` --- .diff-add[ ```scala *Γ |- value : X `Γ[name <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : ??? ``` ] ```ocaml let `x = 1` in x + 2 ``` --- .diff-rm[ ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- Let name value body : `???` ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- Let name value body : `Y` ``` ] ```ocaml let x = 1 in x + 2 ``` --- ```scala ​ ​ Γ |- Ref name : ??? ``` ```ocaml let x = 1 in x + 2 ``` --- .diff-rm[ ```scala ​ ​ *Γ |- Ref name : `???` ``` ] ```ocaml let x = 1 in x + 2 ``` --- .diff-add[ ```scala ​ ​ *Γ |- Ref name : `Γ(name)` ``` ] ```ocaml let x = 1 in x + 2 ``` --- ```scala ​ ​ ​`Γ` |- Ref name : Γ(name) ``` ```ocaml let x = 1 in x + 2 ``` --- ```scala case class TypeEnv(): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` --- .diff-add[ ```scala *case class TypeEnv(`env: List[???]`): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-rm[ ```scala *case class TypeEnv(env: List[`???`]): ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala *case class TypeEnv(env: List[`TypeEnv.Binding`]): *​ *​`object TypeEnv:` * `case class Binding()` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala case class TypeEnv(env: List[TypeEnv.Binding]): ​ object TypeEnv: * case class Binding(`name: String`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala case class TypeEnv(env: List[TypeEnv.Binding]): ​ object TypeEnv: * case class Binding(name: String`, tpe: Type`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala case class TypeEnv(env: List[TypeEnv.Binding]): * `def lookup(name: String) = ???` ​ object TypeEnv: case class Binding(name: String, tpe: Type) ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-rm[ ```scala case class TypeEnv(env: List[TypeEnv.Binding]): * def lookup(name: String) = `???` ​ object TypeEnv: case class Binding(name: String, tpe: Type) ​ ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala case class TypeEnv(env: List[TypeEnv.Binding]): def lookup(name: String) = * `env.find(_.name == name)` ​ object TypeEnv: case class Binding(name: String, tpe: Type) ​ ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ​ ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ​ ``` ] --- .diff-rm[ ```scala 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) ​ ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ``` ] --- .diff-add[ ```scala 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) ​ ​ ``` ] --- .diff-add[ ```scala 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)` ``` ] --- ```scala 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) ​ ​ ``` ```scala ​ ​ ​ ``` --- .diff-add[ ```scala *def typeCheck(expr: Expr`, e: 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`, e`) * case Gt(lhs, rhs) => checkGt(lhs, rhs`, e`) * case Cond(pred, onT, onF) => checkCond(pred, onT, onF`, e`) ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) * `case Let(name, value, body) => ???` ​ ``` ] ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `Let name value body` : Y ``` --- .diff-rm[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) * case Let(name, value, body) => `???` ​ ``` ] ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) * case Let(name, value, body) => `checkLet(name, value, body, e)` ​ ``` ] ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = ??? ​ ​ ​ ​ ​ ​ ​ ``` ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-rm[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = * `???` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`Γ |- value : X` Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-add[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = * `for x <- typeCheck(value, e)` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`Γ |- value : X` Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-add[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = for x <- typeCheck(value, e) * `y <- typeCheck(body, ???)` ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- value : X `Γ[name <- X] |- body : Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-rm[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = for x <- typeCheck(value, e) * y <- typeCheck(body, `???`) ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- value : X `Γ[name <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-add[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = for x <- typeCheck(value, e) * y <- typeCheck(body, `e.bind(name, x)`) ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- value : X `Γ[name <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : Y ``` --- .diff-add[ ```scala def checkLet(name: String, value: Expr, body: Expr, e: TypeEnv) = for x <- typeCheck(value, e) y <- typeCheck(body, e.bind(name, x)) * `yield y` ​ ​ ​ ​ ​ ``` ] ```scala Γ |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Let name value body : `Y` ``` --- ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) ​ ``` ```scala ​ ​ Γ |- `Ref name` : Γ(name) ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) * `case Ref(name) => ???` ``` ] ```scala ​ ​ Γ |- `Ref name` : Γ(name) ``` --- .diff-rm[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) * case Ref(name) => `???` ``` ] ```scala ​ ​ Γ |- Ref name : `Γ(name)` ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) * case Ref(name) => `e.lookup(name)` ``` ] ```scala ​ ​ Γ |- Ref name : `Γ(name)` ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-add[ ```scala * `Γ |- body : ???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ] ```ocaml let f = x -> `x + 1` in f 2 ``` --- ```scala `Γ` |- body : ??? ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-add[ ```scala * `Γ[param <- X]` |- body : ??? ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ] ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-rm[ ```scala * Γ[param <- X] |- body : `???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ] ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-add[ ```scala * Γ[param <- X] |- body : `Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : ??? ``` ] ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-rm[ ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Γ |- Fun param body : `???` ``` ] ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-add[ ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Γ |- Fun param body : `X -> Y` ``` ] ```ocaml let f = x -> x + 1 in f 2 ``` --- ```scala Γ[param <- `X`] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun param body : X -> Y ``` ```ocaml let f = x -> x + 1 in f 2 ``` --- .diff-rm[ ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Γ |- Fun `param` body : X -> Y ``` ] .diff-rm[ ```ocaml *let f = `x` -> x + 1 in f 2 ``` ] --- .diff-add[ ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ *Γ |- Fun `(param : X)` body : X -> Y ``` ] .diff-add[ ```ocaml *let f = `(x: Num)` -> x + 1 in f 2 ``` ] --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : ??? ``` ```ocaml let f = (x: Num) -> x + 1 in f 2 ``` --- .diff-add[ ```scala *​`Γ |- fun : ???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : ??? ``` ] ```ocaml let f = (x: Num) -> x + 1 in `f` 2 ``` --- .diff-rm[ ```scala *​Γ |- fun : `???` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : ??? ``` ] ```ocaml let f = (x: Num) -> x + 1 in `f` 2 ``` --- .diff-add[ ```scala *​Γ |- fun : `X -> Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : ??? ``` ] ```ocaml let f = (x: Num) -> x + 1 in `f` 2 ``` --- .diff-add[ ```scala *Γ |- fun : X -> Y `Γ |- arg : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : ??? ``` ] ```ocaml let f = (x: Num) -> x + 1 in f `2` ``` --- .diff-rm[ ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- Apply fun arg : `???` ``` ] ```ocaml let f = (x: Num) -> x + 1 in `f 2` ``` --- .diff-add[ ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- Apply fun arg : `Y` ``` ] ```ocaml let f = (x: Num) -> x + 1 in `f 2` ``` --- ```scala 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) ``` ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : `X`) body : X -> Y ``` --- .diff-add[ ```scala 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) ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : `X`) body : X -> Y ``` --- ```scala enum Type: case Num case Bool ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : `X -> Y` ``` --- .diff-add[ ```scala enum Type: case Num case Bool * `case Fun()` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : `X -> Y` ``` --- .diff-add[ ```scala enum Type: case Num case Bool * case Fun(`from: Type`) ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : `X` -> Y ``` --- .diff-add[ ```scala enum Type: case Num case Bool * case Fun(from: Type`, to: Type`) ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> `Y` ``` --- .diff-add[ ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) *​ *​`extension (from: Type) def ->(to: Type) = Type.Fun(from, to)` ​ ​ ​ ​ ​ ``` ] ```scala ​ ​ ​ ``` --- .diff-add[ ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) ​ extension (from: Type) def ->(to: Type) = Type.Fun(from, to) ​ ​ ​ ​ ​ ``` ] .diff-add[ ```scala *​`Type.Num -> Type.Bool` ​ ​ ``` ] --- .diff-add[ ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) *​ *​`object ->:` * `def unapply(tpe: Type): Option[(Type, Type)] = tpe match` * `case Type.Fun(from, to) => Some((from, to))` * `case other => None` ​ extension (from: Type) def ->(to: Type) = Type.Fun(from, to) ``` ] .diff-add[ ```scala Type.Num -> Type.Bool ​ ​ ``` ] --- ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) ​ object ->: def unapply(tpe: Type): Option[(Type, Type)] = tpe match case Type.Fun(from, to) => Some((from, to)) case other => None ​ extension (from: Type) def ->(to: Type) = Type.Fun(from, to) ``` .diff-add[ ```scala *Type.Num -> Type.Bool `match` * `case x -> y => s"Function: $x -> $y"` * `case _ => "Not a function!"` ``` ] --- ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) ​ object ->: def unapply(tpe: Type): Option[(Type, Type)] = tpe match case Type.Fun(from, to) => Some((from, to)) case other => None ​ extension (from: Type) def ->(to: Type) = Type.Fun(from, to) ``` ```scala Type.Num -> Type.Bool match `case x -> y` => s"Function: $x -> $y" case _ => "Not a function!" ``` --- ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) ​ ​ ``` ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `Fun (param : X) body` : X -> Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) * `case Fun(param, x, body) => ???` ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `Fun (param : X) body` : X -> Y ``` --- .diff-rm[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) * case Fun(param, x, body) => `???` ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) * case Fun(param, x, body) => `checkFun(param, x, body e)` ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- ```scala def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-rm[ ```scala *def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-add[ ```scala def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = * `for y <- typeCheck(body, ???)` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- `body : Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-rm[ ```scala def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = * for y <- typeCheck(body, `???`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala `Γ[param <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-add[ ```scala def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = * for y <- typeCheck(body, `e.bind(param, x)`) ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala `Γ[param <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : X -> Y ``` --- .diff-add[ ```scala def checkFun(param: String, x: Type, body: Expr, e: TypeEnv) = for y <- typeCheck(body, e.bind(param, x)) * `yield x -> y` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[param <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Fun (param : X) body : `X -> Y` ``` --- ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Fun(param, pType, body) => checkFun(param, pType, body, e) ​ ``` ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `Apply fun arg` : Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Fun(param, pType, body) => checkFun(param, pType, body, e) * `case Apply(fun, arg) => ???` ``` ] ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `Apply fun arg` : Y ``` --- .diff-rm[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Fun(param, pType, body) => checkFun(param, pType, body, e) * case Apply(fun, arg) => `???` ``` ] ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Fun(param, pType, body) => checkFun(param, pType, body, e) * case Apply(fun, arg) => `checkApply(fun, arg, e)` ``` ] ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = ??? ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-rm[ ```scala *def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = `???` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`Γ |- fun` : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-add[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = * `typeCheck(fun, e).flatMap:` ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`Γ |- fun` : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-add[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = typeCheck(fun, e).flatMap: * `case x -> y =>` ??? ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- fun : `X -> Y` Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-rm[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = typeCheck(fun, e).flatMap: * case x -> y => `???` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- fun : X -> Y `Γ |- arg : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-add[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = typeCheck(fun, e).flatMap: * case x -> y => `expect(arg, x, e)` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- fun : X -> Y `Γ |- arg : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- .diff-add[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = typeCheck(fun, e).flatMap: case x -> y => expect(arg, x, e) * `.map(_ => y)` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : `Y` ``` --- .diff-add[ ```scala def checkApply(fun: Expr, arg: Expr, e: TypeEnv) = typeCheck(fun, e).flatMap: case x -> y => expect(arg, x, e) .map(_ => y) * `case other => Left(s"Expected function, found $other")` ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ |- fun : X -> Y Γ |- arg : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- Apply fun arg : Y ``` --- ```scala ​ ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-add[ ```scala *​`??? |- value : X` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = `(lower: Num) -> (upper: Num) ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-rm[ ```scala *​`???` |- value : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = `(lower: Num) -> (upper: Num) ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala *​`Γ[name <- X]` |- value : X ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = `(lower: Num) -> (upper: Num) ->` `if lower > upper then 0` `else lower + (sum (lower + 1) upper)` in sum 1 10 ``` --- .diff-add[ ```scala *Γ[name <- X] |- value : X `??? |- body : Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-rm[ ```scala *Γ[name <- X] |- value : X `???` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-add[ ```scala *Γ[name <- X] |- value : X `Γ[name <- X]` |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : ??? ``` ] ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in `sum 1 10` ``` --- .diff-rm[ ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- LetRec name value body : `???` ``` ] ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-add[ ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- LetRec name value body : `Y` ``` ] ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- ```scala Γ[name <- `X`] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name value body : Y ``` ```scala let rec sum = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` --- .diff-rm[ ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- LetRec name `value` body : Y ``` ] .diff-rm[ ```scala *let rec `sum` = (lower: Num) -> (upper: Num) -> if lower > upper then 0 else lower + (sum (lower + 1) upper) in sum 1 10 ``` ] --- .diff-add[ ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ * Γ |- LetRec name `(value : X)` body : Y ``` ] .diff-add[ ```scala *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 ``` ] --- ```scala 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) ​ ​ ``` ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : `X`) body : Y ``` --- .diff-add[ ```scala 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) ​ ​ ``` ] ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : `X`) body : Y ``` --- ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Apply(fun, arg) => checkApply(fun, arg, e) case Fun(param, pType, body) => checkFun(param, pType, body, e) ​ ​ ``` ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Apply(fun, arg) => checkApply(fun, arg, e) case Fun(param, pType, body) => checkFun(param, pType, body, e) * `case LetRec(name, value, x, body) => ???` ​ ``` ] ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- `LetRec name (value : X) body` : Y ``` --- .diff-rm[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Apply(fun, arg) => checkApply(fun, arg, e) case Fun(param, pType, body) => checkFun(param, pType, body, e) * case LetRec(name, value, x, body) => `???` ​ ``` ] ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def typeCheck(expr: Expr, e: 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, e) case Gt(lhs, rhs) => checkGt(lhs, rhs, e) case Cond(pred, onT, onF) => checkCond(pred, onT, onF, e) case Let(name, value, body) => checkLet(name, value, body, e) case Ref(name) => e.lookup(name) case Apply(fun, arg) => checkApply(fun, arg, e) case Fun(param, pType, body) => checkFun(param, pType, body, e) case LetRec(name, value, x, body) => * `checkLetRec(name, value, x, body, e)` ``` ] ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- ```scala def checkLetRec(name: String, value: Expr, x: Type, body: Expr, e: TypeEnv) = ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def checkLetRec(name: String, value: Expr, x: Type, body: Expr, e: TypeEnv) = * `val eʹ = e.bind(name, x)` ​ ​ ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala ​`Γ[name <- X]` |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def checkLetRec(name: String, value: Expr, x: Type, body: Expr, e: TypeEnv) = val eʹ = e.bind(name, x) ​ * `for _ <- expect(value, x, eʹ)` ​ ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[name <- X] |- `value : X` Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def checkLetRec(name: String, value: Expr, x: Type, body: Expr, e: TypeEnv) = val eʹ = e.bind(name, x) ​ for _ <- expect(value, x, eʹ) * `y <- typeCheck(body, eʹ)` ​ ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[name <- X] |- value : X `Γ[name <- X] |- body : Y` ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : Y ``` --- .diff-add[ ```scala def checkLetRec(name: String, value: Expr, x: Type, body: Expr, e: TypeEnv) = val eʹ = e.bind(name, x) ​ for _ <- expect(value, x, eʹ) y <- typeCheck(body, eʹ) * `yield y` ​ ​ ​ ​ ​ ​ ``` ] ```scala Γ[name <- X] |- value : X Γ[name <- X] |- body : Y ⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Γ |- LetRec name (value : X) body : `Y` ``` --- ```ocaml 1 + true ​ ​ ​ ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala typeCheck(expr, TypeEnv.empty) ​ ``` --- ```ocaml 1 + true ​ ​ ​ ``` ```scala val expr = Add( Num(1), Bool(true) ) ``` ```scala typeCheck(expr, TypeEnv.empty) // val res9: Either[String, Type] = Left(Expected Num, found Bool) ``` --- ```ocaml 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 ``` ```scala val expr = LetRec( [...] ) ​ ``` ```scala typeCheck(expr, TypeEnv.empty) ​ ``` --- ```ocaml 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 ``` ```scala val expr = LetRec( [...] ) ​ ``` ```scala typeCheck(expr, TypeEnv.empty) ​ ``` --- ```ocaml 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 ``` ```scala val expr = LetRec( `[...]` ) ​ ``` ```scala typeCheck(expr, TypeEnv.empty) ​ ``` --- ```ocaml 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 ``` ```scala val expr = LetRec( [...] ) ​ ``` ```scala typeCheck(expr, TypeEnv.empty) // val res10: Either[String, Type] = Right(Num) ``` --- ## [Key takeaways](#conclusion) -- * Type checking is very similar to interpretation -- * It follows the same "formalise / implement" logic -- * We're still allowing illegal programs though... --- class: center, middle name: conclusion # In closing --- ## If you only remember 1 slide... -- * Programs are represented as ASTs -- * We use formal semantics to reason about them -- * Implementation is then relatively straightforward --- class: center, middle name: questions [<img src="img/qr-code.svg" width="50%" height="50%"/>][Slides] [Nicolas Rinaudo] • [@NicolasRinaudo@functional.cafe] --- class: center, middle # Typed Expression --- ```scala 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] ``` --- ```scala enum Type: case Num case Bool case Fun(from: Type, to: Type) object Type: type Num = Type.Num.type type Bool = Type.Bool.type ``` --- ```scala 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] ``` --- ```scala 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] ``` --- ```scala 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] ``` --- ```scala 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))) ``` --- ```scala val expr: TypedExpr[Type.Bool -> Type.Num] = Fun( param = "x", body = Add(Ref("x"), Num(1)) ) ``` --- ## TOC * [Representing code](#ast) * [Taking decisions](#conditionals) * [Naming things](#bindings) * [Reusing Code](#functions) * [Repeating actions](#recursion) * [Identifying invalid programs](#typechecking) [@NicolasRinaudo@functional.cafe]:https://functional.cafe/@NicolasRinaudo [Nicolas Rinaudo]:https://nrinaudo.com/ [Slides]:https://nrinaudo.com/writing-pl/