Semantics of Monte¶
This is a brief specification of the evaluation semantics of Monte.
Monte is an object-based expression language which computes by delivering messages to objects. During computation, expressions are evaulated, resulting in either success or failure; successful evaluation yields an object, while failing evaluation yields an exceptional state.
The Monte language as seen by the programmer has the rich set of syntactic conveniences expected of a modern scripting language. However, to be secure, Monte must have a simple analyzable semantics. We reconcile these by defining a subset of the full language called Kernel-Monte, and only this subset need be given a rigorous semantics. The rest of Monte is defined by syntactic expansion to this subset.
We define Full-Monte as the complete AST of Monte, and canonical expansion as the syntactic expansion which expands Full-Monte to Kernel-Monte while preserving the intended semantics.
Full-Monte should get its own page and have all of its rich semantics spelled out in gory detail.
Monte as a Tree¶
Kernel-Monte is specified as an AST. Each node in the tree is either an expression or a pattern. Expressions can be evaluated to product an object; patterns do not produce values but unify with values (i.e. objects) to introduce names into scopes.
Along with every node, there is a static scope, a compile-time constant mapping of names to declaration and usage sites. For every expression, it is known which names are visible and whether they were declared with def or var.
Computation proceeds by tree evaluation; the root of the tree is evaluated, which in turn can provoke evaluation of various branch and leaf nodes as required.
Recursion in a Monte AST is possible via self-reference; all object patterns are visible within their corresponding script’s scope.
Scope Introduction & Dismissal¶
Many expressions, during evaluation, introduce scopes. When this is done, names declared after scope introduction are said to be visible within the scope. An expression must pair every scope introduction with a scope dismissal. After a scope has been dismissed, the names declared within the scope are no longer visible.
This scoping rule is often called “lexical scoping” and should be familiar to users of other lexically-scoped languages.
Names: Nouns, Slots, and References¶
Monte has a complex system underlying names.
A noun is an identifier which refers to a value (an object). There are three senses of reference from nouns to values, each at a different level of abstraction.
At the simplest level, nouns refer directly to values. Identifiers in patterns match values, and nouns in expressions evaluate to the values to which they were matched.
To represent mutable state, we indirect via slots. Slots are objects
that contain values and may be updated over time (much like pointers in
C). Slots can be accessed and manipulated with slot patterns and slot
expressions. A final slot acts as though nouns refer directly to values, while
a var slot has a
put operation that updates its value.
A binding is a slot along with a guard that constrains the values in the slot. Bindings are essential to auditors.
To allow references across turns and vats, we indirect via references.
A Monte expression can yield either a successful result or an exceptional state. Exceptional states are intentionally vague; they are usually represented as panics in virtual machines or stack unwinders in interpreters.
While in an exceptional state, most expressions evaluate to that same exceptional state. A TryExpr can replace an exceptional state with a successful result. A FinallyExpr can perform some side computation despite an exceptional state.
When an error is thrown, the computation switches to an exceptional state and the thrown error is sealed in an implementation-dependent manner.
Produces an object which passes
Char and corresponds to the Unicode
codepoint of the CharExpr.
Produces an object which passes
Double and corresponds to the IEEE 754
double-precision floating-point number of the DoubleExpr.
Implementations may, at their discretion, substitute any higher-precision IEEE 754 number for the given one.
Produces an object which passes
Int and corresponds to the integer of the
Produces an object which passes
Str and corresponds to the sequence of
Unicode codepoints of the StrExpr. .
The string of codepoints is not normalized; it corresponds one-to-one with the codepoints in the Monte source literal.
Produces the binding for the given noun.
Produces the value in the slot of the given noun.
An AssignExpr has a name and an expression. The expression is evaluated and the result is both assigned to the name as a noun in the current scope and the produced value.
If the name’s slot is not assignable, an error is thrown.
A DefExpr has a pattern, an (optional) exit expression, and a specimen expression. The specimen is evaluated, followed by the exit (if present). The specimen is unified with the pattern, defining names into the surrounding scope. The produced value is the specimen.
If unification fails, the result of the exit expression is used as an ejector to escape; if ejecting fails, then an error is thrown.
A HideExpr has a single subexpression which is evaluated in a fresh scope. The produced value of the subexpression is used as the produced value.
A CallExpr has a receiver expression, a verb (string), some argument expressions, and some named argument expressions. The receiver is evaluated, then each argument, and then each named argument. Then, a message consisting of the verb, arguments, and named arguments is passed to the receiver. The value returned from the receiver is the produced value.
discuss sameness and doctest _equalizer
An EscapeExpr has a pattern and inner expression and, optionally, a catch pattern and catch expression (not to be confused with Try/catch expressions).
An ejector is created and a scope is introduced. The ejector is unified with the pattern and then the inner expression is evaluated.
If the ejector was not called during evaluation of the inner expression, the scope is then dismissed and the produced value from the inner expression is used as the produced value of the entire EscapeExpr.
If the ejector is called within the inner expression, then control immediately leaves the inner expression and the scope is dismissed; if there is no catch pattern/expression, then the value passed to the ejector is immediately used as the produced value. Otherwise, the value passed to the ejector is used as a specimen and unified with the catch pattern in a freshly-introduced scope, and then the catch expression is evaluated. Finally, the catch scope is dismissed and the produced value from the catch expression is used as the produced value of the escape-expr.
A FinallyExpr contain two expressions. The first expression is evaluated in a fresh scope and its resulting object or failing state is retained. Then, the second expression is evaluated in a fresh scope. Finally, the retained state from the first expression, success or failure, is the produced value of the entire finally-expr.
The second expression is evaluated regardless of whether the first expression returns an exceptional state; its state is discarded. It is implementation-dependent whether exceptional states are chained together.
This table shows the possible states:
An IfExpr has a test expression, a consequent expression, and an alternative
expression. A scope is introduced, and then the test expression is evaluated,
producing a value which passes
Bool. Either the consequent or the
alternative is evaluated and used as the produced value, depending on whether
the test produced
false. Finally, the scope is dismissed.
If the test’s produced value does not conform to
Bool, an error is thrown.
A SequenceExpr contains zero or more expressions.
If a SequenceExpr contains zero expressions, then it evaluates to null.
Otherwise, a SequenceExpr evaluates each of its inner expressions in sequential order, using the final expression’s produced value as the produced value of the entire sequence.
A TryExpr has an expression and a catch pattern and expression. The first expression is evaluated in a fresh scope and used as the produced value.
If an error is thrown in the first expression, then the scope is dismissed, a new scope is introduced, the error is unified with the catch pattern, and the catch expression is evaluated and used as the produced value.
Evaluation of a message sent to an object proceeds as follows.
A matcher has a pattern and an expression. A scope is introduced and incoming messages are unified with the pattern. If the unification succeeds, the expression is evaluated and its produced value is returned to the caller.
A method has a verb, a list of argument patterns, a list of named argument patterns, a guard expression, and a body expression. When a message matches the verb of the method, a scope is introduced and each pattern is unified against the message. Each argument pattern is unified against each argument, and then each named argument pattern is unified against each named argument.
If the number of arguments in the message differs from the number of argument patterns in the method, an error is thrown. Informally, the method and message must have the same arity.
If unification fails, an error is thrown.
After unification, the guard expression is evaluated and its produced value is stored for return value guarding. The body expression is evaluated and its produced value is given as a specimen to the return value guard. The returned prize from the guard is returned to the caller.
If the return value guard fails, an error is thrown.
The return value guard is evaluated before the body, but called after the body.
An ObjectExpr has a pattern, a list of auditor expressions, a list of methods, and a list of matchers. When evaluated, a new object with the methods and matchers is created. That object is audited by each auditor in sequential order. Finally, the object is unified with its pattern in the surrounding scope, and the first auditor, if present, is used as the guard for the binding.
Objects close over all of the names which are visible in their scope. Additionally, objects close over the names defined in the pattern of the ObjectExpr.
Pattern evaluation is a process of unification. During unification, patterns are given a specimen and an ejector. Patterns examine the specimens and create names in the surrounding scope. When patterns fail to unify, the ejector is fired. If the ejector fails to leave control, then an error is thrown.
An IgnorePatt coerces its specimen with a guard.
A BindingPatt coerces its specimen with the
Binding guard and binds the
resulting prize as a binding.
A FinalPatt coerces its specimen with a guard and binds the resulting prize into a final slot.
A VarPatt coerces its specimen with a guard and binds the resulting prize into a var slot.
A ListPatt has a list of subpatterns. It coerces its specimen to a
and matches the elements of the specimen to each subpattern, in sequential
If the ListPatt and specimen are different lengths, then unification fails.
A ViaPatt contains an expression and a subpattern. The specimen and ejector are passed to the expression’s produced value, and the result is unified with the subpattern.