Types 2
Table of Contents
1. Type Checker
A type checker is a proof system that proves that a program when run will not result in a “type error”
<expr>::= <num>
| <str>
| {+ <expr> <expr>}
| <id>
| {([<id> : tow]) => <exprc>}
| {<expr> <expr>}
(tow)types::= num
| str
| tow -> tow
1.1. Typing Rules
`<num> : num`
`<str> : str`
given: E1 : num………E2 : num
we have: {+ E1 E2} : num
given: E1: tow1 -> tow2….E2: t1
we have: {E1 E2} : t2
given: lookup(x) = tow
we have: type-env x : tow
given: extendenv[x -> tow1] E : t2
whe have: {([x : tow1]) => E} tow1 -> tow2
- when we have to look at type of x thisi s where we extend the type environment
1.2. Ex
1 : num 2 : num………3 : num 4 : num
{+ 1 2}: num ………..{+ 3 4}:num
{+ {+ 1 2} {+ 3 4}}:num
1.3. Gentzon-style natural reduction
Given p->q p we have q