Erda
ErdaRVM, ErdaRVMσ, ErdaC++, and ErdaGA constitute a family of small programming languages and implementations for experimenting with error handling mechanisms. We use the unqualified name Erda to refer to the language family as a whole, or any one member of the family where the languages are all alike in relevant respects.
The “concrete” syntax of Erda resembles that of Racket (and Scheme).
1 ErdaRVM
#lang erda/rvm | package: erda |
The ErdaRVM language is a dynamically typed language that includes an alerts mechanism for declarative error reporting, and transparently propagates errors as data values.
This document describes the syntax and semantics of a selection of the ErdaRVM-specific constructs.
The erda/rvm language also inherits a number of constructs directly from Racket, including the begin, begin0, let, let*, letrec, require, and provide syntactic forms, and the not function. These forms should therefore behave as described in the Racket documentation. Note, however, that functions may seemingly behave differently due to ErdaRVM’s different function application semantics.
1.1 Modules and Macros
The Racket require and provide forms (and associated sub-forms) may be used in Erda as normal to import modules and to define the interfaces exposed by modules.
Macros are not included in the language by default, but there is nothing preventing from require’ing macro support from Racket.
1.2 Defining Forms
syntax
(define id expr)
(define (id arg ...) maybe-alerts expr ...+) (define (id arg ...) #:handler maybe-alerts expr ...+) (define (id arg ...) #:direct expr ...+)
The semantics of the (define id expr) form is the same as in Racket. In ErdaRVM functions are not first class, and the language does not include a lambda form, and thus this form is intended only for defining variables (that do not name functions).
The second form, which is for defining “regular” ErdaRVM functions, binds id as a function that takes arguments arg .... The language enforces that the arguments will all have to be good, wrapped values (i.e., values for which the predicate good-result? holds); there is an implicit alert guarding against bad values. Explicit alerts may be specified according to the maybe-alerts grammar. The result of the function should be a single wrapped value (i.e., values for which result? holds). Indeed, ErdaRVM does not support multi-value returns, or more generally, multi-value expressions. The language enforces, on the single return value, the data invariant associated with its type; the function application will produce a bad value instead if the invariant does not hold. Explicit post-conditions are treated similarly. The invariants are not checked on bad results.
The #:handler variant of the define form is like the “regular” function definition form, but without the implicit alerts requiring good arguments, or the assumption that post-condition expressions require good free variables. That is, any pre-conditions get evaluated even if some of the arguments are bad, and if they hold, the function gets called. Similarly, any post-conditions (but not data invariant) are also checked on a bad result. The intention is for this kind of function definition to make it possible to implement “handler” functions able to process (and perhaps recover from) bad values.
The #:direct variant of the form defines a function that is called directly, without the language doing any pre- or post-processing on the incoming or outgoing values, which are still expected to be wrapped (no data invariants is checked either, so beware). This form of define is intended to allow for the implementation of ErdaRVM functions (such that they are aware of wrapped values) as Racket-based primitives, probably using Racket’s #%plain-app form as the “FFI” for implementing such primitives within the ErdaRVM language. Perhaps more likely, you’ll want to implement such functions in Racket, and instead merely declare them as #:direct.
The first declare form declares a Racket primitive that processes unwrapped values, and thus will get automatic unwrapping/wrapping at the application site. Alert clauses may be specified, with any test-expr evaluated with the arg (and value, as appropriate) identifiers bound to wrapped values; in other words, despite a primitive function being called, the conditional expressions are still written in ErdaRVM. As many existing Racket functions may throw exceptions, it is quite important to specify on-throw alert clauses as appropriate, as a way of converting from such a foreign error reporting mechanism.
The second declare form is like the #:direct define form, but without taking an implementation. An implementation must already be bound as the function id.
It is also possible to call undeclared Racket functions, as long as they are bound. Naturally, then, no explicit alerts have been specified, but goodness of arguments is nonetheless enforced, and arguments are unwrapped automatically; undeclared functions are expected to process unwrapped values. There is no catching of exceptions, but the data invariant of the result value is checked. A broken DI leads to the result being automatically wrapped as a bad value, whereas otherwise it is wrapped as a good value.
1.2.1 Alerts
The alert specification of a defined or declared function matches the following grammar.
maybe-alerts | = | ||||
| | #:alert (alert-clause ...) | ||||
alert-clause | = | (alert-id pre-when test-expr) | |||
| | (alert-id pre-unless test-expr) | ||||
| | (alert-id post-when test-expr) | ||||
| | (alert-id post-unless test-expr) | ||||
| | (alert-id on-throw pred-expr) |
where:
alert-id An alert name. The name of the alert to trigger if the corresponding test-expr holds, or if the corresponding pred-expr predicate holds for a thrown exception object.
test-expr An ErdaRVM expression, computing in wrapped values. The test-exprs of #:handler functions should probably be able to deal with bad values as well.
The expression is automatically negated for the pre-unless and post-unless cases.
For post-condition expressions, the result of the function application is bound as value.
pred-expr A Racket predicate expression, computing in bare values. The predicate should accept any bare exn structure (or a subtype) as an argument, and yield a bare value indicating whether the predicate holds.
1.3 Expressions
syntax
(#%datum . datum)
> 0 (Good 0)
syntax
(quote id)
> 'not-found (Good 'not-found)
syntax
syntax
(if test-expr then-expr else-expr)
syntax
(if-not test-expr then-expr else-expr)
syntax
(or expr ...)
syntax
(and expr ...)
syntax
(cond cond-clause ... else-clause)
cond-clause = (test-expr then-expr) else-clause = (else then-expr)
syntax
(let-direct ([arg expr] ...) body ...+)
syntax
(try body ...+ #:catch catch-clause maybe-catch-all)
catch-clause = ((id ...) then-expr ...+) maybe-catch-all =
| (_ then-expr ...+)
> (try (raise 'worst) #:catch [(bad worse still-worse) 1] [(worst) 2] [_ 3]) (Good 2)
> (try (raise 'bad) #:catch [(worse worst) 3]) (Bad bad raise)
> (try 1 #:catch [_ 3]) (Good 1)
> (try (raise 'bad) #:catch [_ 3]) (Good 3)
syntax
(::> try-expr ... fail-expr)
> (::> 'good 'alternative) (Good 'good)
> (::> (raise 'bad) 'alternative) (Good 'alternative)
> (::> (raise 'bad) (raise 'worse) 'alternative) (Good 'alternative)
> (::> (raise 'bad) (::> (raise 'nested-bad)) (raise 'no-good)) (Bad no-good raise)
syntax
(on-alert (handler-clause ...) body ...+)
handler-clause = ((id ...) expr ...+)
If any application of a function listed by id fails (with a bad result), then a matching clause’s expressions are evaluated, and the result of the last of them is substituted in place of the result of the failed function call.
This recovery mechanism does not apply to syntactic forms (even if named by id), nor will recovery happen within the body of an let-direct expression.
> (on-alert () 'nothing) (Good 'nothing)
> (on-alert ([(not) 'good]) (raise 'bad)) (Bad bad raise)
> (on-alert ([(raise) 'good]) (raise 'bad)) (Good 'good)
syntax
(block stat ... result-expr)
stat = (#:let id expr) | (#:when test-expr #:let id expr) | expr
The evaluation of the overall expression immediately stops with a bad value if a test-expr produces a bad value. Where there were no failures in conditionals, the overall result of the expression will be that of result-expr.
> (block 1 2 3) (Good 3)
> (block [#:let x 1] x) (Good 1)
> (block [#:let x 1] [#:let x 2] x) (Good 2)
> (block [#:let x 1] [#:when #t #:let x 2] x) (Good 2)
> (block [#:let x 1] [#:when #f #:let x 2] x) (Good 1)
> (block [#:let x (raise 'bad)] [#:when x #:let x 'good] x) (Bad bad-arg monadic-if)←(Bad bad raise)
1.4 Standard Library
This section lists a small selection of the ErdaRVM standard library.
The documented argument and result types (or predicates, rather) are only for informational purposes; they are not necessarily enforced using actual contracts (indeed ErdaRVM does not have support for contracts built-in). Also, the contracts we use here are informal, in that we may mix and match Erda and Racket predicates.
Some functions do have pre- and post-conditions specified with alert clauses, but these are not indicated in the signatures shown here; the signatures here reflect the functions’ own ability to handle inputs, as they have been implemented. The ErdaRVM language itself does further bad-value extension, at call sites; this is different to ErdaGA, where it is the functions that are extended, and thus become more capable at dealing with bad values, and this difference is reflected in their documented contracts.
procedure
(result? x) → good-result?
x : any/c
procedure
(good-result? x) → good-result?
x : any/c
procedure
(bad-result? x) → good-result?
x : any/c
> (bad-result? (raise 'worst)) (Good #t)
procedure
(alert-name? x) → good-result?
x : any/c
procedure
(raise alert-name) → bad-result?
alert-name : alert-name?
procedure
(raise-with-value alert-name v) → bad-result?
alert-name : alert-name? v : result?
procedure
(raise-with-cause alert-name cause) → bad-result?
alert-name : alert-name? cause : result?
> (raise-with-cause 'follow-up (raise 'cause)) (Bad follow-up raise-with-cause)⇐(Bad cause raise)
2 ErdaRVMσ
#lang erda/sigma-rvm | package: erda |
The ErdaRVMσ language is a variant of ErdaRVM such that it exports an assignment expression, and modified conditionals with optional cleanup actions. Only the additions are documented here.
ErdaRVMσ’s set! form (for variable assignment) is the same as in Racket. Bad values also get assigned.
The only conditionals available in ErdaRVMσ are if, when, and unless. The other conditionals from ErdaRVM are not available. More or less all other forms (e.g., define) and functions (e.g., raise) from ErdaRVM are also included in ErdaRVMσ.
syntax
(if test-expr then-expr else-expr maybe-cleanup)
maybe-cleanup =
| #:cleanup cleanup-expr ...
> (define failed? #f)
> (if (raise 'worse) 1 2 #:cleanup (set! failed? #t)) (Bad bad-arg monadic-if/cleanup)←(Bad worse raise)
> failed? (Good #t)
syntax
(when test-expr body ...+ maybe-cleanup)
Note that there is no when or unless in ErdaRVM, as having them makes little sense without side effects (such as assignment).
> (when 1 2 3) (Good 3)
syntax
(unless test-expr body ...+ maybe-cleanup)
3 ErdaC++
#lang erda/cxx | package: erda |
The ErdaC++ language is a statically typed language such that it includes an alerts mechanism for declarative error reporting, and transparently propagates errors as data values.
Provided that any referenced functions are implemented both for Racket and C++, the definitions appearing in a erda/cxx module (or collection thereof) may both be used directly from a Racket program, and translated into a C++ API and implementation usable from C++ programs. In contrast, the definitions appearing in a erda/rvm module are only intended for evaluation in the Racket VM.
While the ErdaC++ and ErdaRVM implementations are largely based on the same code, the former does somewhat more work at compile time. This is to keep the runtime requirements smaller, and thus facilitate translation into C++. The only C++ runtime requirements for the erda/cxx language itself are a small subset of the C and C++11 standard libraries, and the "erda.hpp" header file.
ErdaC++’s functions and variables are typed, whereas in ErdaRVM it is values that are typed. While the static types need not always be declared, the types of a program must be fully resolvable statically. For this purpose, the compiler features Hindley-Milner style type inference.
For declaring types and other details relating to translating ErdaC++ into C++, the language features support for various annotations (e.g., type, foreign, etc.) that may be specified for declarations; there are no such annotations in ErdaRVM.
Not everything from ErdaRVM has been brought over to ErdaC++; notably, some of the error recovery supporting forms are missing, as is most of the runtime library. The focus in ErdaC++ has been to include only the essentials in the language, and exclude more experimental features (such as try and on-alert). The idea is to improve and validate the design of these features in ErdaRVM first, before bringing them into other Erda variants.
This document describes the syntax and semantics a selection of those ErdaC++ constructs that have notable differences to ErdaRVM’s. Overall, ErdaC++’s syntactic constructs generally have the same semantics as in ErdaRVM, and we do not document them separately here.
syntax
(define #:type id maybe-annos)
(define id maybe-annos expr) (define (id arg ...) maybe-annos maybe-alerts expr ...+) (define (id arg ...) #:handler maybe-annos maybe-alerts expr ...+) (define (id arg ...) #:direct maybe-annos expr ...+)
These forms have the same semantics as for ErdaRVM’s define, with three notable exceptions. Firstly, there is a define #:type form, which is the same as for Magnolisp’s define. Second, ErdaC++ does not support the on-throw alert clause; the maybe-alerts grammar is otherwise the same as given in the Alerts section. Third, all the define variants accept optional annotations; the grammar for maybe-annos is as described in Annotations.
syntax
(declare #:type id maybe-annos)
(declare (id arg ...) maybe-annos maybe-alerts) (declare (id arg ...) #:direct maybe-annos)
See define for a description of the three notable differences between ErdaC++’s declare compared to ErdaRVM’s declare and Magnolisp’s declare, as these differences are the same for both define and declare.
3.1 C++ Translation Advising Annotations
Some of the ErdaC++ defining forms support a subset of the annotations that appear in the Magnolisp language. The supported annotations are: type, export, foreign, and literal. The purpose of these annotations is to instruct ErdaC++-to-C++ translation. Refer to Magnolisp documentation for more details about them.
4 ErdaGA
#lang erda/ga | package: erda |
The ErdaGA language is a dynamically typed functional language such that it includes an alerts mechanism for declarative error reporting, and transparently propagates errors as data values. A particular aim for ErdaGA is to adhere to the semantics of guarded algebras.
In ErdaGA functions are (wrapped) values, and hence may be passed around as such, enabling the definition of ErdaGA-native higher-order functions. An attempt to apply a bad function (or a non-function) will naturally fail, resulting in a bad value.
ErdaGA emits the necessary glue code for alert processing into function definition sites rather than call sites. Consequently, it is possible to support alerts also for anonymous functions.
In ErdaGA, all function arguments are evaluated before determining whether they are good arguments for the function. ErdaRVM’s argument evaluation is less eager.
ErdaGA records failed expression history in a manner that allows for “replay” of failed operations, using redo and related functions.
This document describes the syntax and semantics a selection of those ErdaGA constructs that have notable differences to ErdaRVM’s. Overall, ErdaGA’s constructs generally have the same syntax and semantics as those of ErdaRVM, and we do not document them separately here.
The significant difference between ErdaGA and ErdaRVM is that since in ErdaRVM error processing code is emitted into call sites, the same function can be applied in two modes, directly or with implicit error processing, with any alerts specified with ErdaRVM’s declare. In ErdaGA, on the other hand, “direct” and “Erda” functions have different bindings, and thus let-direct and related forms do not alter the error processing behavior of applications of declared functions.
syntax
(lambda args #:direct body ...+)
(lambda args #:handler maybe-alerts body ...+) (lambda (arg ...) #:primitive maybe-alerts body ...+) (lambda args maybe-alerts body ...+)
args = (arg ...) | (arg ... . rest-id) | rest-id
A #:direct function must have a body that is prepared to handle wrapped (good or bad) argument values, and will produce a wrapped value.
A #:handler is not protected from receiving bad values as arguments, unless alerts are specified to guard against that.
The body of a #:primitive lambda is protected against bad arguments, and it is assumed that the body processes bare values, and produces a bare value. Any alerts that are given must be in terms of wrapped values, however.
The “regular” lambda form produces a function that processes wrapped values, but its body can expect to see no bad arguments.
> ((lambda (x) #:alert ([bad-arg pre-when #t]) x) 42) (Bad bad-arg: <fun> 42)
> ((lambda (x) #:handler 42) (raise 'bad)) (Good 42)
syntax
(thunk rest ...+)
procedure
(function? x) → (Good/c rkt.boolean?)
x : any/c
syntax
(let-direct ([arg expr] ...) body ...+)
syntax
(direct-lambda (arg ...) maybe-alerts body ...+)
syntax
(define-direct (id arg ...) maybe-alerts body ...+)
procedure
cond-value : Result? then-thunk : (Result/c rkt.procedure?) else-thunk : (Result/c rkt.procedure?)
syntax
(cond cond-clause ... else-clause)
cond-clause = (test-expr then-expr ...+) else-clause = (#:else then-expr ...+)
> (::> (cond [#f 'false] [(raise 'bad) 'bad] [#:else 'otherwise]) 'cond-was-bad) (Good 'cond-was-bad)
syntax
(do sub-do ... expr)
sub-do = [x-id <- expr] | expr
> (define bad (raise 'bad))
> (do 42) (Good 42)
> (do bad 42) (Bad bad-arg: >>= (Bad bad: raise bad) <fun>)
> (do [x <- bad] 42) (Bad bad-arg: >>= (Bad bad: raise bad) <fun>)
ErdaGA’s raise-with-cause is like ErdaRVM’s raise-with-cause.
4.1 Inspecting and Using History
ErdaGA has result?, good-result?, and bad-result? predicates, which are like ErdaRVM’s result?, good-result?, and bad-result?.
For inspecting the contents of bad values, ErdaGA has functions such as bad-result-alert-name (which is also in ErdaRVM), bad-result-fun, and bad-result-args.
procedure
(bad-result-alert-name v) → (Result/c rkt.symbol?)
v : Result?
procedure
(bad-result-fun v) → Result?
v : Result?
procedure
(bad-result-args v) → (Result/c rkt.list?)
v : Result?
For argument list manipulation ErdaGA’s standard library includes the functions args-list?, args-list, args-cons, args-car, args-cdr, and args-list-set, which are similar to the Racket equivalents, but defined as handlers as necessary to be able to deal with bad values contained in argument lists.
ErdaGA is also able to “replay” failed operations with the redo, redo-apply, and redo-app functions, all of which are handlers so that they can accept a bad result as their first argument. The latter two redo functions make it possible to invoke the failed operation with different arguments.
> (redo bad) (Bad bad: raise bad)
procedure
(redo-apply v args) → Result?
v : Result? args : Result?
> (redo-apply bad (args-list 'worse)) (Bad worse: raise worse)
> (redo-app bad 'still-worse) (Bad still-worse: raise still-worse)
4.2 Contracts
(require erda/ga/contract) | package: erda |
In documenting ErdaGA functions, we state contracts for them as is usual for Racket documentation. These are stated so that they account for any bad-argument extension of the function, and are explicit about wrapped values. It is a programming error to call a function with arguments that do not adhere to the contract.
We specify the contracts for function arguments and results using predicates and predicate combinators, some of which come from Racket. Where we want to be explicit about our use of Racket primitives, we prefix them with rkt..
ErdaGA also has an internal API that includes some of its own predicates such as Result?, Good?, and Bad?, and some predicate combinators, which have a /c in their name, as is customary for contracts in Racket. These are only intended for internal use, documentation purposes, and perhaps for actually specifying enforced contracts.
We are presently not documenting alert declarations, which are different in their role. In particular, any bad conditions covered by declared alerts cannot be a programming error, since cases are handled implicitly.
procedure
(Result? x) → rkt.boolean?
x : any/c
procedure
(Good? x) → rkt.boolean?
x : any/c
procedure
(Bad? x) → rkt.boolean?
x : any/c
procedure
(Result/c p?) → (-> any/c rkt.boolean?)
p? : rkt.procedure?
procedure
(Good/c p?) → (-> any/c rkt.boolean?)
p? : rkt.procedure?
That is, calling Result/c or Good/c instantiates a Racket predicate which applies the specified Racket primitive predicate p? on any bare value inside a good value.
The difference between the two functions is that Result/c produces predicates that return #t for bad values, while Good/c’s predicates return #f for bad values.
5 Example Code
For sample ErdaRVM code, see the "i1-program.rkt" file of the Erda implementation codebase. For ErdaGA code, see "i3-program.rkt". Those programs should evaluate as is within the Racket VM; see the racket command of your Racket installation.
For sample ErdaC++ programs, see the "test-*.rkt" files and "program-*" projects in the "tests" directory of the codebase.
Most of the provided sample ErdaC++ programs will evaluate as is within the Racket VM. To instead translate said programs into C++, see the Magnolisp documentation, or look at the "Makefile"s in the "program-*" directories for example invocations of the mglc command-line tool.
6 Source Code
7 Installation
Racket. The primary implementation language of Erda. Version 6.3 (or higher) of Racket is required; a known-compatible version is 6.5, but versions 6.3–6.6 are all expected to work.
Magnolisp. A language and compiler serving as a basis for the implementation of ErdaC++. A known-compatible revision of Magnolisp is 191d529486e688e5dda2be677ad8fe3b654e0d4f.
The software and the documentation can be built from source, or installed using the Racket package manager. Racket is required for building and installation.
raco pkg install git://github.com/bldl/magnolisp#191d529
raco pkg install git://github.com/bldl/erda
The above commands should install the library, the command-line tool(s), and a HTML version of the manual.
8 License
Except where otherwise noted, the following license applies:
Copyright © 2014–2016 University of Bergen and the authors.
Authors: Tero Hasu
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.