Procedure definitions are program-level constructs for defining functions and other global constants.
In common usage, the term “procedure” is synonymous with “function definition”, because most procedures define functions. Mars also lets you use procedures to specify other global constants.
All procedures create a global constant, which is just a non-modifiable variable with a type and a value. The nature of the global constant depends on the form of the procedure.
There are two forms of procedure:
A computable global constant is not necessarily not a function. It may have a function type, if the procedure itself returns a function value.
Procedure definitions have the following syntax:
proceduredef ::= proc_head ":" NEWLINE INDENT var_decl* statement+ DEDENT | proc_head "=" expression
The procedure header provides the public interface to the procedure:
proc_head ::= "def" proc_name [proc_params] "::" type proc_params ::= "(" [proc_param ("," proc_param)*] ")" proc_param ::= param_name "::" type proc_name ::= lower_identifier param_name ::= lower_identifier
The procedure header specifies the following information:
Functions may optionally have zero or more parameters.
A procedure without parameters (a computable global constant) has a head of the following form:
def f :: t
This defines a global constant of type t. The constant’s value is the result of evaluating the procedure. The time at which the procedure is evaluated is unspecified. It may be evaluated once at load time, once when it is first used, or upon each usage (depending on the implementation).
Because of the fact that the evaluation time is undefined, computable global constant definitions should not perform side-effects or produce errors. If a zero-parameter procedure is to perform side-effects, it should be declared as a function with zero arguments (a nullary function), thereby making its evaluation time explicit.
A procedure with parameters (a function definition) has a head of the following form:
def f(a1 :: t1, a2 :: t2, ..., an :: tn) :: t
where n >= 0.
This defines a global constant of type (t1, t2, ..., tn) -> t. The constant’s value is a function object which executes the body of the procedure when all arguments are applied.
Unlike computable global constants, the body of a function definition is not executed until it is explicitly applied.
A function with zero arguments is a nullary function.
It is legal, and useful, to define a nullary function (with a head of the form def f() :: t). This is distinct from a computable global constant, because it will have type () -> t, not just t, and will require explicit application, of the form f().
The names a1, a2, ..., an are the names of the function’s formal parameters. These names are not part of the function’s interface (they make no difference to the caller). They are used in the function body, as the names of local-scoped variables of the specified type, and take the value of the corresponding actual parameter at runtime.
It is a compiler error for two parameters to have the same name.
There are two ways to define a procedure – as a single expression, or with a full body.
The “full body” syntax is the most general, and allows for procedures with local variables, and an arbitrary number of statements. It is written in the form:
def f(args) :: rettype: declaration 1 ... declaration n statement 1 ... statement n
The “single expression” syntax is a short-hand notation, only allowing procedures with no local variables, and a single expression to be evaluated. It is written in the form:
def f(args) :: rettype = expression
This is syntactic sugar for:
def f(args) :: rettype: return expression
Mars distinguishes between local and global variables. All local variables are scoped to the entire procedure body (there is no block scope). A name refers to a local variable if and only if it:
Local variables may be given the same name as a global constant or function. In this case, the local variable shadows the global constant of the same name.
Local variables may optionally be explicitly declared. For simplicity, all declarations must appear before any statements. Declarations have the following syntax:
var_decl ::= "var" var_name "::" type NEWLINE var_name ::= lower_identifier
Note that formal parameters are considered local variables, and must not be re-declared. It is a compiler error if a variable is declared with the same name as a formal parameter, or if two local variables are declared with the same name.
It is currently an error to declare a local variable with a type which includes a type variable not found in the procedure header. This is generally not a useful thing (since type variables are monomorphic; see type unification), but if it is desired, the variable cannot be explicitly declared.
Local variables (other than parameters) are not initialised with any particular value. The compiler is required to guarantee that variables are not used uninitialised (see semantic errors).
The evaluation of procedures is the heart of the Mars execution model. Mars procedures are evaluated eagerly, and arguments are passed by-value.
If a global constant is named in a variable reference expression, the expression must evaluate to a first-class value.
If the constant is a computable global constant, that value must be the result of evaluating the procedure (which should be a constant ). The time at which the procedure is evaluated, and the number of times it is evaluated, is unspecified, and left up to the implementation. Implementations may (but are not limited to) choose one or more of the following evaluation strategies:
If the constant was defined with a function definition, the expression’s value is a function object which will call the specified function when applied with all parameters.
A function object is an opaque first-class value of type (t1, t2, ..., tm) -> t, where m >= 0. Internally, function objects have n formal parameters, the first n - m of which are bound to actual values, and the remaining m of which are unbound (where 0 <= m <= n).
Since Mars features partial function application, a mechanism known as currying takes place. This mechanism is as follows:
When a function is partially applied (using the ... notation), it is applied to i parameters, where i <= m. No evaluation takes place. Instead, the result is of the application is the given function object, but with its first i unbound formal parameters bound to the given actual parameters. The result has type (ti+1, ti+2, ..., tm) -> t.
When a function is fully applied, it must be applied to exactly m parameters. The result of the application is the evaluation of the function with the final m formal parameter bound to the given actual parameters. The result has type t.
Functions have n formal parameters. A formal parameter is a special local variable, which is bound to a value before the execution of the function’s body. The value which a formal parameter is bound to is called the actual parameter.
Formal parameters may be bound well in advance of the actual evaluation of the function, due to the currying mechanism outlined above. The bound values must be stored in an implementation-defined manner.
As Mars is a call-by-value language, actual parameters are evaluated before being bound to formal parameters. The binding process is to first evaluate the actual parameter expression, and then bind its value to the formal parameter name. The binding is the same as for an assignment statement – it is shallow, and the formal parameter has the same identity as the actual parameter.
The call-by-value mechanism guarantees that direct modification of the value will not affect the caller. Specifically, if the callee re-assigns one of its formal parameters with a new value, that change shall not affect the original value from which the parameter was derived. Nor shall it affect the binding in the callee’s function object (so subsequent uses of the same function object will keep the original binding).
This does not hold up for indirect modification of a value. Mars allows impure constructs such as array element and field update. Since the formal parameter has the same identity as the original actual parameter, making destructive updates to a record or array in the formal parameter will also update the actual parameter, along with any other aliases.
The evaluation of a procedure is a matter of executing each statement in the procedure’s body sequentially, according to the execution rules for that kind of statement, until a return statement is encountered.
The return statement’s expression is evaluated, and its value is used as the result of the expression which caused the procedure to be evaluated.
There are several cases which cause a procedure to be rejected at compilation time:
This second rule is perhaps over-zealous, as it forbids control-flow paths which raise errors but do not return values. A more detailed analysis should be proposed, including noting which procedures always produce errors.
|||The result of a computable global constant should be a constant, but might not be, if the procedure performs side-effects such as user input. The behaviour of computable global constants with side-effects is undefined, so for all intents and purposes, “computable global constants” may indeed simply be treated as constants.|
|||Implementors are to keep in mind that compilation must terminate in a finite amount of time, while computable global constants may not terminate. Therefore, this evaluation strategy must only be employed conservatively, if evaluation is guaranteed to terminate.|