This environment construction is performed by the function module-env , which is defined below. The Iota type system has two special types, none and unit , which do not appear in the syntax of the language. The none type is the type of expressions or statements which do not return control to their enclosing context. The unit type is the type of expressions or statements which return control to the enclosing context, but produce no value. The function module-env performs the gathering of information about variables and functions that are visible at the top level, and can be defined recursively.
Function definitions are less trivial.
These rules say that to check the type safety of a function definition, we check that the the body of the function, E, has the expected type T r that is the declared return type of the function. In the case of a function that does not return a value, the expression E may have any type T r , since its value, if any, is discarded. The type of the expression E is determined in an environment that includes all of the argument variables a i of the function, bound to their corresponding types T i , which is necessary because E may mention these variables. The addition of two environments is the union of those environments as long as the two environments do not contain any definitions with the same name. If two environments contain definitions with the same name, the addition of the environments is undefined.