Types 3
Table of Contents
1. How the type checker works with tree
Gamma(x) = num
Gamma(y) = num
From the type enviornment what is the type of x and y
Gamma|-x :
Gamma|-y :
Addition
[x->num][y->num]|-{+ x y} :
Lambda
[x->num]|-{([y : num]) => {+ x y}} :
Lambda
0|-([x : num]) => {([y : num]) => {+ x y}} :
0|-4 :
Function Call
0|-{([x : num]) => {([y : num]) => {+ x y}} 4}
0|-7
{{([x : num]) => {([y : num]) => {+ x y}} 4} 7} :
1.1. Now we can go back down the tree
we go back down the tree filling out the types
Gamma(x) = num
Gamma(y) = num
From the type enviornment what is the type of x and y
Gamma|-x : num
Gamma|-y : num
Addition
[x->num][y->num]|-{+ x y} : {num}
Lambda
[x->num]|-{([y : num]) => {+ x y}} : {num -> num}
Lambda
0|-([x : num]) => {([y : num]) => {+ x y}} : {num -> {num -> num}}
0|-4 : num
Function Call
0|-{([x : num]) => {([y : num]) => {+ x y}} 4} : {num -> num}
0|-7
{{([x : num]) => {([y : num]) => {+ x y}} 4} 7} : num