This is an old revision of the document!
Type Judgments for the Type Checking Lab
Here are the type judgments we went over in class translated into English form instead of the notation we used in class:
* numeric literal: always results in a number
* boolean literal (true / false): always results in a boolean
* addition / subtraction: if both are numbers, results in a number
* iszero: if input is a number, result is a boolean
* id: look it up in the type environment to find out its type
* with: results in the type resulting from the body after adding to the type environment that the type of the identifier is the type of the initialization expression
* if: if the type of the conditional is boolean and the types of the two possible branches are the same, results in the type of either branch
* lambda: results in a function from the declared type of the input parameter to the return type of the body after adding to the type environment that the formal parameter is the declared type
* app: if the operator is a function (t1 → t2), and if the type of the actual parameter is type t1, results in type t2.
