1 of 93

1

Programming Languages and Compilers (CS 421)

Talia Ringer (they/them)

4218 SC, UIUC

https://courses.grainger.illinois.edu/cs421/fa2023/

Based heavily on slides by Elsa Gunter, which were based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul Agha

2 of 93

Last class, we covered recursive datatypes, emphasizing how they can represent the syntax of programs for transformations
We also teased mutually recursive and nested recursive datatypes
Today, we will cover mutually recursive and nested recursive datatypes in more detail
We will then start talking about types and type checking—another very useful thing we need to do when writing compilers and interpreters

Objectives for Today

2

3 of 93

Last class, we covered recursive datatypes, emphasizing how they can represent the syntax of programs for transformations
We also teased mutually recursive and nested recursive datatypes
Today, we will cover mutually recursive and nested recursive datatypes in more detail
We will then start talking about types and type checking—another very useful thing we need to do when writing compilers and interpreters

Objectives for Today

3

4 of 93

4

Questions from last week?

5 of 93

5

Mutually Recursive Datatypes

6 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

6

Mutually Recursive Datatypes

7 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

7

Mutually Recursive Datatypes

8 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

8

Mutually Recursive Datatypes

9 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

9

Mutually Recursive Datatypes

10 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

10

Mutually Recursive Datatypes

11 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

11

Mutually Recursive Datatypes

12 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

12

Mutually Recursive Datatypes

13 of 93

Mutually Recursive Types

type 'a tree =

TreeLeaf of 'a | TreeNode of 'a treeList

and 'a treeList =

Last of 'a tree | More of ('a tree * 'a treeList)

*

13

Mutually Recursive Datatypes

14 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7))))))

5 7

3 2

*

14

Mutually Recursive Datatypes

15 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

15

Mutually Recursive Datatypes

16 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

16

Mutually Recursive Datatypes

17 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

17

Mutually Recursive Datatypes

18 of 93

Mutually Recursive Types - Values

5 7

3 2

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

*

18

Mutually Recursive Datatypes

19 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

19

Mutually Recursive Datatypes

20 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

20

Mutually Recursive Datatypes

21 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

21

Mutually Recursive Datatypes

22 of 93

Mutually Recursive Types - Values

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

22

Mutually Recursive Datatypes

23 of 93

Mutually Recursive Types - Values

TreeNode

More More Last

TreeLeaf TreeNode TreeLeaf

5 More Last 7

TreeLeaf TreeLeaf

3 2

*

23

Mutually Recursive Datatypes

24 of 93

Mutually Recursive Functions

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

24

Mutually Recursive Datatypes

25 of 93

Mutually Recursive Functions

TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

5 7

3 2

*

25

Mutually Recursive Datatypes

26 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

26

Mutually Recursive Datatypes

27 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

27

Mutually Recursive Datatypes

28 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

28

Mutually Recursive Datatypes

29 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

29

Mutually Recursive Datatypes

30 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

30

Mutually Recursive Datatypes

31 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

31

Mutually Recursive Datatypes

32 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

32

Mutually Recursive Datatypes

33 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

33

Mutually Recursive Datatypes

34 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

34

Mutually Recursive Datatypes

35 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

35

Mutually Recursive Datatypes

36 of 93

Mutually Recursive Functions

let rec fringe tree =

match tree with

| TreeLeaf x -> [x]

| TreeNode list -> list_fringe list

and list_fringe tree_list =

match tree_list with

| Last tree -> fringe tree

| More (tree, list) ->

(fringe tree) @ (list_fringe list)

*

36

Mutually Recursive Datatypes

37 of 93

Mutually Recursive Functions

5 7

3 2

# let tree = TreeNode

(More (TreeLeaf 5,

(More

(TreeNode (More (TreeLeaf 3, Last (TreeLeaf 2))),

Last (TreeLeaf 7)))))

in fringe tree;;

: int list = [5; 3; 2; 7]

*

37

Mutually Recursive Datatypes

38 of 93

38

Questions so far?

39 of 93

39

Nested Recursive Datatypes

40 of 93

Nested Recursive Types

(* Alt. def, allowing empty lists & values anywhere *)

type 'a labeled_tree =

TreeNode of ('a * 'a labeled_tree list);;

*

40

Nested Recursive Datatypes

41 of 93

Nested Recursive Types - Values

(* Alt. def, allowing empty lists & values anywhere *)

type 'a labeled_tree =

TreeNode of ('a * 'a labeled_tree list);;

TreeNode

(5,

[TreeNode (3, []);

TreeNode

(2, [TreeNode (1, []); TreeNode (7, [])]);

TreeNode (5, [])])

*

41

Nested Recursive Datatypes

42 of 93

Nested Recursive Types - Values

(* A simpler definition, allowing empty lists *)

type 'a labeled_tree =

TreeNode of ('a * 'a labeled_tree list);;

TreeNode

(5,

[TreeNode (3, []);

TreeNode

(2, [TreeNode (1, []); TreeNode (7, [])]);

TreeNode (5, [])])

5

3 2 5

1 7

*

42

Nested Recursive Datatypes

43 of 93

Nested Recursive Types - Values

ltree = TreeNode(5)

:: :: :: [ ]

TreeNode(3) TreeNode(2) TreeNode(5)

[ ] :: :: [ ] [ ]

TreeNode(1) TreeNode(7)

[ ] [ ]

*

43

Nested Recursive Datatypes

44 of 93

Mutually Recursive Functions

let rec flatten_tree labtree =

match labtree with

| TreeNode (x, ts) -> x :: flatten_tree_list ts

and flatten_tree_list ts =

match ts with

| [] -> []

| labtree :: labtrees ->

flatten_tree labtree @ flatten_tree_list labtrees

*

44

Nested Recursive Datatypes

45 of 93

Mutually Recursive Functions

let rec flatten_tree labtree =

match labtree with

| TreeNode (x, ts) -> x :: flatten_tree_list ts

and flatten_tree_list ts =

match ts with

| [] -> []

| labtree :: labtrees ->

flatten_tree labtree @ flatten_tree_list labtrees

*

45

Nested recursive types lead to

mutually recursive functions!

Nested Recursive Datatypes

46 of 93

Mutually Recursive Functions

let rec flatten_tree labtree =

match labtree with

| TreeNode (x, ts) -> x :: flatten_tree_list ts

and flatten_tree_list ts =

match ts with

| [] -> []

| labtree :: labtrees ->

flatten_tree labtree @ flatten_tree_list labtrees

*

46

Nested recursive types lead to

mutually recursive functions!

Nested Recursive Datatypes

Can get around if clever, but nontrivial.

47 of 93

Mutually Recursive Functions

let rec flatten_tree labtree =

match labtree with

| TreeNode (x, ts) -> x :: flatten_tree_list ts

and flatten_tree_list ts =

match ts with

| [] -> []

| labtree :: labtrees ->

flatten_tree labtree @ flatten_tree_list labtrees

*

47

Nested recursive types lead to

mutually recursive functions!

Nested Recursive Datatypes

And we need polymorphism to work around!

48 of 93

48

Types and Type Checking

49 of 93

49

Questions so far?

50 of 93

Why Types?

Types play a key role in:

Data abstraction in the design of programs

Keeping track of important information for you
Abstracting away irrelevant details

Type checking in the analysis of programs

e.g., ruling out entire classes of bugs

Compile-time code generation in the translation and execution of programs

Data layout (how many words; which are data and which are pointers) dictated by type

*

50

Types and Type Checking

51 of 93

No Really, Why Types?

https://www.destroyallsoftware.com/talks/wat

*

51

Types and Type Checking

52 of 93

Terminology

Type: A type T defines possible data values

For the sake of this class, it’s enough to imagine it as being a set of possible data values
e.g., short in C is {x | 2¹⁵ - 1 ≥ x ≥ -2¹⁵}
A value (or term) in this set is said to have type T

Type system: rules of a language assigning types to expressions

One can view a type system as ruling out possibly “bad” expressions in a language
Deeply and beautifully connected to logics

*

52

Types and Type Checking

53 of 93

Terminology

Type: A type T defines possible data values

For the sake of this class, it’s enough to imagine it as being a set of possible data values
e.g., short in C is {x | 2¹⁵ - 1 ≥ x ≥ -2¹⁵}
A value (or term) in this set is said to have type T

Type system: rules of a language assigning types to expressions

One can view a type system as ruling out possibly “bad” expressions in a language
Deeply and beautifully connected to logics

*

53

Types and Type Checking

54 of 93

Types as Specifications

Types describe properties of programs
Different type systems describe different properties, e.g.,

Data is read-write versus read-only
Operation has authority to access data
Data came from “right” source

With fancy types, can prove theorems by writing programs whose types represent those theorems
Common type systems focus on types describing same data layout and access properties

*

54

Types and Type Checking

55 of 93

Sound Type System

A type system is sound if in that system, whenever an expression is assigned type T, and it evaluates to value v, then v is in the set of values defined by T
Informally, if the type checker says a term has a given type, then when you actually run the program it’s going to have that type still, no matter what weird thing you do to the term
OCaml, Scheme, and Rust have sound type systems
Most implementations of C and C++ do not

*

55

Types and Type Checking

56 of 93

Strongly Typed Language

When no application of an operator to arguments can lead to a runtime type error, the language is said to be strongly typed

Eg: 1 + 2.3;;

What this actually implies depends on the definition of “type error,” which varies by language

*

56

Types and Type Checking

57 of 93

Strongly Typed Language

C++ claimed to be “strongly typed”, but

Union types allow creating a value at one type and using it at another
Type coercions may cause unexpected (undesirable) effects
No array bounds check (in fact, no runtime checks at all)

SML, OCaml “strongly typed” but still must do dynamic array bounds checks, runtime type case analysis, and other checks
Coq, Lean, Agda, Idris can do really fancy checks

*

57

Types and Type Checking

58 of 93

Static vs. Dynamic Types

Static type: type assigned to an expression at compile time
Dynamic type: type assigned to a storage location at run time
Statically typed language: static type assigned to every expression at compile time
Dynamically typed language: type of an expression determined at run time
Gradually typed language: continuum of languages between dynamic and static typing

*

58

Types and Type Checking

59 of 93

Static vs. Dynamic Types

Static type: type assigned to an expression at compile time
Dynamic type: type assigned to a storage location at run time
Statically typed language: static type assigned to every expression at compile time
Dynamically typed language: type of an expression determined at run time
Gradually typed language: continuum of languages between dynamic and static typing

*

59

Gradual types are not explicitly covered in class

Types and Type Checking

60 of 93

Type Checking

When is op(arg1 , … , argn) allowed?
Type checking assures operations are applied to the right number of arguments of the right types

“Right type” may mean same type as was specified, or may mean that there is a predefined implicit coercion that will be applied

Used to resolve overloaded operations

*

60

Types and Type Checking

61 of 93

Type Checking

When is op(arg1 , … , argn) allowed?
Type checking assures operations are applied to the right number of arguments of the right types

“Right type” may mean same type as was specified, or may mean that there is a predefined implicit coercion that will be applied

Used to resolve overloaded operations

*

61

Types and Type Checking

62 of 93

Type Declarations & Type Inference

Type declarations: explicit assignment of types to terms in source code

Must be checked in a strongly typed language
Often not necessary for strong typing or even static typing (depends on the type system)

Type inference: a program analysis to assign a type to a term in its context

Fully static type inference first introduced by Robin Miller in ML
Haskell, OCaml, SML all use type inference

Records are a problem for type inference

*

62

63 of 93

63

Questions so far?

64 of 93

64

Types and Type Checking

65 of 93

Type Checking

When is op(arg1 , … , argn) allowed?
Type checking assures operations are applied to the right number of arguments of the right types

“Right type” may mean same type as was specified, or may mean that there is a predefined implicit coercion that will be applied

Used to resolve overloaded operations

*

65

Types and Type Checking

66 of 93

Type Checking

Type checking may be done statically at compile time or dynamically at run time
Dynamically typed languages (e.g., LISP, Prolog) do only dynamic type checking
Statically typed languages can do most type checking statically
Real life does not like binary discrete categories of things so much (consider Python with mypy)

*

66

Types and Type Checking

67 of 93

Dynamic Type Checking

Dynamic type checking is performed at run-time before each operation is applied
Types of variables and operations left unspecified until run-time

Same variable may be used at different types

Data object must contain type information
Errors aren’t detected until violating application is executed (maybe years after the code was written)

*

67

Types and Type Checking

68 of 93

Dynamic Type Checking

Dynamic type checking is performed at run-time before each operation is applied
Types of variables and operations left unspecified until run-time

Same variable may be used at different types

Data object must contain type information
Errors aren’t detected until violating application is executed (maybe years after the code was written)

*

68

Types and Type Checking

69 of 93

Static Type Checking

Static type checking is performed after parsing, before code generation
Type of every variable and signature of every operator must be known at compile time
Can eliminate need to store type information in data object if no dynamic type checking is needed
Catches many programming errors at earliest point
Can’t check types that depend on dynamically computed values

e.g., array bounds, unless your type system is very fancy (dependent types)

*

69

Types and Type Checking

70 of 93

Static Type Checking

Static type checking is performed after parsing, before code generation
Type of every variable and signature of every operator must be known at compile time
Can eliminate need to store type information in data object if no dynamic type checking is needed
Catches many programming errors at earliest point
Can’t check types that depend on dynamically computed values

e.g., array bounds, unless your type system is very fancy (dependent types)

*

70

Types and Type Checking

71 of 93

Static Type Checking

Static type checking is performed after parsing, before code generation
Type of every variable and signature of every operator must be known at compile time
Can eliminate need to store type information in data object if no dynamic type checking is needed
Catches many programming errors at earliest point
Can’t check types that depend on dynamically computed values

e.g., array bounds, unless your type system is very fancy (dependent types)

*

71

Types and Type Checking

72 of 93

Static Type Checking

Static type checking is performed after parsing, before code generation
Type of every variable and signature of every operator must be known at compile time
Can eliminate need to store type information in data object if no dynamic type checking is needed
Catches many programming errors at earliest point
Can’t check types that depend on dynamically computed values

e.g., array bounds, unless your type system is very fancy (dependent types)

*

72

Dependent types are not explicitly covered in class, but I’m obsessed with them, so please ask in office hours or something

Types and Type Checking

73 of 93

Static Type Checking

Typically places restrictions on languages

Garbage collection, usually (except Rust!)
References instead of pointers (Rust has both!)
All variables initialized when created
Variable only used at one type

Union types allow for work-arounds, but effectively introduce dynamic type checks

*

73

Types and Type Checking

74 of 93

74

Type Judgments

75 of 93

Format of Type Judgments

A type judgement has the form Γ ⊢ t : T
Informally: “in gamma, t has type T”
Γ ($\Gamma$ in latex) is a typing environment

Maps terms (variables, and function names when function names are not variables) to types
Γ is a set of the form { t₁ : T₁ , … , t_n : T_n }
For any t_i at most one T_i such that (t_i : T_i ∈ Γ)

t is a term (program expression)
T is a type to be assigned to t
⊢ pronounced “turnstile” or “entails” ($\vdash$)

*

75

Type Judgments

76 of 93

Format of Type Judgments

A type judgement has the form Γ ⊢ t : T
Informally: “in gamma, t has type T”
Γ ($\Gamma$ in latex) is a typing environment

Maps terms (variables, and function names when function names are not variables) to types
Γ is a set of the form { t₁ : T₁ , … , t_n : T_n }
For any t_i at most one T_i such that (t_i : T_i ∈ Γ)

t is a term (program expression)
T is a type to be assigned to t
⊢ pronounced “turnstile” or “entails” ($\vdash$)

*

76

Type Judgments

77 of 93

Format of Type Judgments

A type judgement has the form Γ ⊢ t : T
Informally: “in gamma, t has type T”
Γ ($\Gamma$ in latex) is a typing environment

Maps terms (variables, and function names when function names are not variables) to types
Γ is a set of the form { t₁ : T₁ , … , t_n : T_n }
For any t_i at most one T_i such that (t_i : T_i ∈ Γ)

t is a term (program expression)
T is a type to be assigned to t
⊢ pronounced “turnstile” or “entails” ($\vdash$)

*

77

Type Judgments

78 of 93

Format of Type Judgments

A type judgement has the form Γ ⊢ t : T
Informally: “in gamma, t has type T”
Γ ($\Gamma$ in latex) is a typing environment

Maps terms (variables, and function names when function names are not variables) to types
Γ is a set of the form { t₁ : T₁ , … , t_n : T_n }
For any t_i at most one T_i such that (t_i : T_i ∈ Γ)

t is a term (program expression)
T is a type to be assigned to t
⊢ pronounced “turnstile” or “entails” ($\vdash$)

*

78

Type Judgments

79 of 93

Axioms – Constants (Monomorphic)

Γ ⊢ n : int (assuming n is an integer constant)

Γ ⊢ true : bool Γ ⊢ false : bool

These rules are true with any typing environment
Γ, n are metavariables

*

79

Type Judgments

80 of 93

Axioms – Variables (Monomorphic Rule)

Notation: Let Γ(v) = T if v : T ∈ Γ

Note: if such T exits, its unique

Variable axiom:

Γ ⊢ v : T if Γ(v) = T

*

80

Type Judgments

81 of 93

Simple Rules – Arithmetic (Mono)

Primitive Binary operators (⊕ ∈ { +, -, *, …}):

Γ ⊢ t₁: T₁ Γ ⊢ t₂: τ₂ (⊕) : T₁ → T₂ → T₃

Γ ⊢ t₁ ⊕ t₂ : T₃

Special case: Relations (~ ∈ { < , > , =, <=, >= }):

Γ ⊢ t₁ : T Γ ⊢ t₂ : T (~) : T → T → bool

Γ ⊢ t₁ ~t₂ :bool

For the moment, think T is int

*

81

Type Judgments

82 of 93

Simple Rules – Arithmetic (Mono)

Primitive Binary operators (⊕ ∈ { +, -, *, …}):

Γ ⊢ t₁: T₁ Γ ⊢ t₂: τ₂ (⊕) : T₁ → T₂ → T₃

Γ ⊢ t₁ ⊕ t₂ : T₃

Special case: Relations (~ ∈ { < , > , =, <=, >= }):

Γ ⊢ t₁ : T Γ ⊢ t₂ : T (~) : T → T → bool

Γ ⊢ t₁ ~t₂ :bool

For the moment, think T is int

*

82

Type Judgments

83 of 93

Simple Rules – Arithmetic (Mono)

Primitive Binary operators (⊕ ∈ { +, -, *, …}):

Γ ⊢ t₁: T₁ Γ ⊢ t₂: τ₂ (⊕) : T₁ → T₂ → T₃

Γ ⊢ t₁ ⊕ t₂ : T₃

Special case: Relations (~ ∈ { < , > , =, <=, >= }):

Γ ⊢ t₁ : T Γ ⊢ t₂ : T (~) : T → T → bool

Γ ⊢ t₁ ~t₂ :bool

For the moment, think T is int

*

83

Type Judgments

84 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

???

{x : int} ⊢ x + 2 = 3 : bool

*

84

What do we need to show first?

Bin

Type Judgments

85 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

{x : int} ⊢ x + 2 : int {x : int} ⊢ 3 : int

{x : int} ⊢ x + 2 = 3 : bool

*

85

What do we need to show first?

Bin

Type Judgments

86 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

???

{x : int} ⊢ x + 2 : int {x : int} ⊢ 3 : int

{x : int} ⊢ x + 2 = 3 : bool

*

86

Left-hand side?

Bin

Type Judgments

87 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

{x : int} ⊢ x : int {x : int} ⊢ 2:int

{x : int} ⊢ x + 2 : int {x : int} ⊢ 3 : int

{x : int} ⊢ x + 2 = 3 : bool

*

87

Left-hand side?

Bin

Type Judgments

88 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

{x : int} ⊢ x : int {x : int} ⊢ 2:int

{x : int} ⊢ x + 2 : int {x : int} ⊢ 3 : int

{x : int} ⊢ x + 2 = 3 : bool

*

88

How to finish?

Bin

Type Judgments

89 of 93

Example: { x : int } ⊢ x + 2 = 3 : bool

{x : int} ⊢ x : int {x : int} ⊢ 2:int

{x : int} ⊢ x + 2 : int {x : int} ⊢ 3 : int

{x : int} ⊢ x + 2 = 3 : bool

*

89

Complete proof (type derivation)

Bin

Var

Const

Type Judgments

90 of 93

90

Questions?

91 of 93

We saw mutual and nested recursive datatypes in more detail than last time. Both lead to mutually recursive functions.
It’s possible to work around mutual recursion if you�want—thanks to higher-order functions and polymorphism.
Types can be useful for many things.
Γ ⊢ t : T means that a term t has type T in type context Γ.
Such a judgment can be checked statically or dynamically (or, IRL, sometimes a mix).

Takeaways

91

92 of 93

We saw mutual and nested recursive datatypes in more detail than last time. Both lead to mutually recursive functions.
It’s possible to work around mutual recursion if you�want—thanks to higher-order functions and polymorphism.
Types can be useful for many things.
Γ ⊢ t : T means that a term t has type T in type context Γ.
Such a judgment can be checked statically or dynamically (or, IRL, sometimes a mix).

Next Class: More Type Checking

92

93 of 93

EC1 graded!

It’s really hard to catch bugs in language-model-generated code! (~25% missed bugs in final generated code that I caught)
Also impacted me when I tried it … traditional expertise doesn’t translate directly here

EC2 is late, but coming
WA4 will be due Thursday
Quiz 3 on MP5 is next Tuesday
All deadlines can be found on course website
Use office hours and class forums for help

Next Class

93