Also see the ML Manual for Nuprl4.


next up previous contents index
Next: Using ML in Up: An Overview of Previous: Failures

Syntax and Semantics

Figure gif gives   a summary of the basic constructs needed for programming  in ML. An abstract syntax of ML expressions is summarized in figure gif, with expressions shown in order of decreasing precedence. These are essentially taken from [Gordon, Milner, & Wadsworth 79]. In addition to the expression forms shown in figure gif, ML contains the standard arithmetic and logical operatorsgif and the equality predicate written in the traditional infix form. The various let forms have corresponding where forms in which the expression and the binding surround the where. For example, instead of let x=3 in e one could write e where x=3. The where constructs bind more tightly than the let constructs.

  
Figure: Syntax of Basic ML Constructs

 

  
Figure: Syntax of ML Expressions

 

The semantics of ML can be given in terms of the store--environment model. Evaluation of expressions takes place in an environment, which is a mapping between identifiers and either values or locations; the store is a mapping between locations and values and is only needed to understand imperative constructs. Evaluating  an expression in an environment produces a value or a failure. In the latter case a failure token, which may be used as a value in the rest of the program, is produced.

A declaration  changes the environment. The general form of a declaration is let b , letref b or letrec b, where b is a binding  . (Bindings are described later.) If a let, is used the identifiers in b cannot be updated; if assignable variables are required then letref must be used. The letrec form must be used with recursively  defined functions. Bindings, like varstructs, have three general forms. There are simple bindings, function definitions and multiple bindings. The multiple binding is just an abbreviation for a sequence of simple bindings. In a simple binding a varstruct is equated to an expression. The form of the varstruct and of the expression are compared, and if they match structurally then the variables in the varstruct are bound to the corresponding substructures of the expression. The scope of the binding produced by an expression of the form let x= in e2 is the expression . A declaration of the form let x= has scope throughout the rest of the session until another declaration causes global rebinding of the variables in x. Type declarations are effected using the lettype, abstype and absrectype forms. The scope of the bindings associated with these terms mirrors that of data bindings described above; type bindings are described in more detail in [Gordon, Milner, & Wadsworth 79].

The evaluation  of expressions is more or less standard and will only be discussed briefly. The evaluation of a constant expression returns the value denoted by the constant. The evaluation of a simple variable returns the value to which the variable is bound. The evaluation of an application, f e, results in the evaluation of f, which must be a function, the subsequent evaluation of e and finally the evaluation of the resulting application. The evaluation of the logical  expressions e1 or e2 and e1 & e2 forces evaluation of e1 first and only causes the evaluation of e2 if the value of the logical expression is not determined by the value of e1. In a sequencing expression of the form e1;e2;e3...;en the expressions are evaluated in the given order and the value resulting from the evaluation of en is returned. The list construct is evaluated similarly; the evaluation of an expression of the form [e1;e2;...;en] results in the evaluation of the expressions e1 through en in that order, with the value returned being the list formed from the values of the expressions. The order of evaluation is not important unless assignable variables are being updated in the subexpressions. The evaluation of failwith e causes the evaluation of e first, after which a failure (rather than an ordinary value) with the value of e is returned. For operational descriptions of other ML constructs, see [Gordon, Milner, & Wadsworth 79].



next up previous contents index
Next: Using ML in Up: An Overview of Previous: Failures


Also see the ML Manual for Nuprl4.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995