Garland +

误 编程语言初探



Expressions and Variable Bindings

An ML program is a sequence of bindings. Each binding gets type-checked and then (assuming it type-checks) evaluated. What type (if any) a binding has depends on a static environment, which is roughly the types of the preceding bindings in the file. How a binding is evaluated depends on a dynamic environment, which is roughly the values of the preceding bindings in the file.

val x = e;

Here, val is a keyword, x can be any variable, and e can be any expression.

some expression defination

Integer constants:




Boolean constants:

Less-than comparison:

Function Bindings

Function is something that is called with arguments and has a body that produces a result. but no this, no return statement。

fun pow (x:int, y:int) = (* correct only for y >= 0 *)
    if y=0
    then 1
    else x * pow(x,y-1)


fun x0 (x1 : t1, ..., xn : tn) = e

This is a binding for a function named x0. It takes n arguments x1, … xn of types t1, …, tn and has an expression e for its body.


To type-check a function binding,first type-check the body e in a static environment that maps x1 to t1, ... xn to tn and x0 to t1 * ... * tn -> t. Because x0 is in the environment, we can make recursive function calls,For the function binding to type-check, the body e must have the type t.

After a function binding, x0 is added to the static environment with its type. The arguments are not added to the top-level static environment — they can be used only in the function body.


A function is a value — we simply add x0 to the environment as a function that can be called later. As expected for recursion, x0 is in the dynamic environment in the function body and for subsequent bindings