type checking

Variables and functions are bound to their types in a symbol table which we use in type checking. Let us take an example where variables and functions have separate namespaces. Then we will need two symbol tables. Let us say variables are bound to integers and booleans only. Functions are bound by the type of the arguments and the type of the results. The symbol tables for variables and functions are inherited attributes for expressions.The type of the expression is returned as synthesized attributes. We generally use an abstract syntax tree for presentation. To retrieve the attributes we assume there are predefined functions for each terminal type. For each non-terminal, we define one or more functions that take an abstract syntax subtree and inherited attributes as arguments and return the synthesized attributes. Let us assume the symbol table for variables is given by the parameter vtable  and the symbol table for the function is given by the parameter ftable. Let us say the function error returns a type error. Since more than one errors could be reported, we let the error reporting to return. The type checker can guess what type to return and allow the reporting to return.
The type checking function evaluates based on the expression, vtable and ftable as parameters. Based on a switch case construct for the expression, we do the following:
1) if it's a numerical expression and an identifier we lookup the type of the identifier based on the vtable, name(id)  and if its bound it passes the type check or an error is returned.
2) if the expression is an addition, we call the type checker for each of the operands and return an int else we call error.
3) if the expression is a comparision, then we repeat the step of 2) and return a boolean
4) if the expression is a branch with if-then-else we call the type checker on each of the operations and return a bool as per the condition else we  return an error
5) if the expession is a method expression, the function name is looked up for the number and type of arguments and the return type. If this matches the expected, the resulting type is the return type but if the function is not found in the ftable or the vtable
6) a let expression declares a new variable and the return type is that of the expression.The symbol table is extended using bind and this is used for checking the body expression and finding the type.
This is how we type check expressions.
For function declarations, type checking is done by building a symbol table for variables and used for matching the result type of the function to the type of the body. The type check function for functions just checks for errors.
Similarly, a program can be considered a list of functions and is deemed type-correct if all the functions are type correct.
(text from Mogensen)