@hackage alms0.6.9
a practical affine language
Categories
License
BSD-3-Clause
Maintainer
jesse@eecs.northwestern.edu
Links
Versions
Installation
Dependencies (0)
Dependents (1)
@hackage/acme-everything
Package Flags
unicode
(on by default)
Use Unicode symbols for pretty-printing
editline
(on by default)
Enable line editing using the editline package
parsec3
(on by default)
Use version 3 of the parsec package
readline
(off by default)
Enable line editing using the readline package
This is a prototype implementation of Alms, an affine language with modules and subtyping.
Please see http://users.eecs.northwestern.edu/~jesse/pubs/alms/ for more information.
CONTENTS
- GETTING STARTED
- WHAT TO TRY
- PAPER SYNTAX VERSUS ASCII SYNTAX
- EDITLINE TROUBLE
GETTING STARTED
Alms is no longer actively maintained, and does not build with the latest GHC. In particular, it is know to work with GHC 7.6.3, and and likely no longer works with GHC 6. It also does not work with GHC 8.
Provided that a not-too-recent ghc is in your path, to build on UNIX it ought to be be sufficient to type:
% make
This should produce an executable "alms" in the current directory,
If this fails, it may also be necessary to either install the editline package first or disable line editing (Please see EDITLINE TROUBLE).
On Windows, build with Cabal:
> runghc Setup.hs configure
> runghc Setup.hs build
This produces an executable in "dist\build\alms\alms".
Cabal should work on UNIX as well, but mixing Cabal and make leads to linker errors, so it's probably best to stick with one or the other.
WHAT TO TRY
Examples from the paper and several more are in the examples/ directory. The examples from section 2 of the POPL submission are in:
examples/ex60-popl-deposit.alms
examples/ex61-popl-AfArray.alms
examples/ex62-popl-AfArray-type-error.alms
examples/ex63-popl-CapArray.alms
examples/ex64-popl-CapLockArray.alms
examples/ex65-popl-Fractional.alms
examples/ex66-popl-RWLock.alms
Other notable examples include two implementations of session types, an implementation of Sutherland-Hodgman re-entrant polygon clipping (1974) using session types, and the tracked Berkeley Sockets API from our ESOP 2010 paper:
lib/libsessiontype.alms
lib/libsessiontype2.alms
examples/session-types-polygons.alms
lib/libsocketcap.alms
The echo server from the ESOP paper, which uses libsocketcap, is in examples/echoServer.alms. To try it, listening on port 10000, run:
% ./alms examples/echoServer.alms 10000
To connect to the echo server, you can run
% ./alms examples/netcat.alms localhost 10000
from another terminal.
The examples directory contains many more examples, many of which are small, but demonstrate type or contract errors -- the comment at the top of each example says what to expect. Run many of the examples with:
% make examples
Or run the examples as regression tests (quietly):
% make tests
Of course, you can also run the interpreter in interactive mode:
% ./alms
You can load libraries from the command line like this:
% ./alms -lsocketcap
Or from within the REPL like this:
#- #load "libsocketcap"
Finally, it may be helpful to know about the #i command for asking the REPL about identifiers:
#- #i list Exn *
type +`a list : `a = (::) of `a * `a list | ([]) -- built-in
module Exn -- defined at lib/libbasis.alms:198:1-32
type +`a * +`b : `a \/ `b -- built-in
val ( * ) : int -> int -> int -- built-in
PAPER SYNTAX VERSUS ASCII SYNTAX
The language as presented in the paper is faithful to the language as implemented, except for issues of pretty printing:
LaTeX (what the paper says) ASCII (what you type)
\forall \exists \lambda all ex fun (binders) \alpha 'a (unlimited type variable) \hat\alpha `a (affine type variable) \to^A -A> (affine arrow) \to^{\hat\alpha} -a> (arrow with qualifier) \sqcup / (qualifier join) \pm \baro + - = 0 + - (variances)
EDITLINE TROUBLE
Line editing is enabled in the REPL by default, which depends on the editline Cabal package. If make fails and says something about editline, then there are three options:
-
Disable line editing:
% make clean; make FLAGS=-editline
or
% cabal install --flags="-editline" alms
-
Use readline instead:
% make clean; make FLAGS=readline
or
% cabal install --flags="readline" alms
-
Try to install editline or readline . . .
Installing editline can be kind of touchy. On my system,
% cabal install editline
seemed to install it, but Cabal still couldn't find it when building this program. Installing editline globally made it work:
% sudo cabal install --global editline
(Likewise, readline didn't work until I installed it globally.)
At this point, older versions of Cabal may give the installed library bad permissions, so something like this may help, depending on where it installs things:
% sudo chmod -R a+rX /usr/local/lib/editline*
If the cabal installation of the GHC package fails, it may be necessary first to install the C library that it depends on. The source is available at http://www.thrysoee.dk/editline/. On my Debian system, I was able to install it with:
% sudo aptitude install libedit2 libedit-dev
Note that libeditline is a completely different library, and installing that will not help.