In Proc. 38th ACM Symposium on Principles of Programming Languages (POPL’11), January 2011
Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard’s linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while maximizing polymorphism between affine and unlimited types.
A key feature of Alms is the ability to introduce abstract affine types via ML-style signature ascription. In Alms, an interface can impose stiffer resource usage restrictions than the principal usage restrictions of its implementation. This form of sealing allows the type system to naturally and directly express a variety of resource management protocols from special-purpose type systems.
We present two pieces of evidence to demonstrate the validity of our design goals. First, we introduce a prototype implementation of Alms and discuss our experience programming in the language. Second, we establish the soundness of the core language. We also use the core model to prove a principal kinding theorem.
Alms is also available on Hackage, but as it does not build with current versions of GHC, that is probably not what you want. The next section describes how to try Alms using a Docker image.
Alms is no longer maintained and does not build with the latest GHC. In particular, it is known to work with GHC 7.6.3, and and likely no longer works with GHC 6. It also does not work with GHC 8.
Thus, the recommended way to try out Alms is via a Docker image, jessetov/alms. If you have Docker installed, you can get a shell with:
% docker run -it --rm jessetov/alms
That will give you a root shell in the
/alms directory, which will
alms interpreter executable, which you can run:
# ./alms Alms, version 0.6.9 #- fun (a, b) -> (a, a) it : ∀ 'a `b. 'a * `b → 'a * 'a = #<fn (λ (a, b) → (a, a))> #-
Examples from the paper and several more are in the
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 our 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:
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
The language as presented in the paper is faithful to the language as implemented, except for issues of pretty printing:
|When the paper says . . . ,||then type . . . .|
|∀ ∃ λ μ||
||(unlimited type variables)|
|± ⌽ + –||
||(affine type variables)|
||(unlimited & one-use arrows)|
|→⟨α̂⟩ ⊔ ⟨β̂⟩||
||(arrow with qualifier expression)|
Alms requires GHC to build. It is known to work with GHC 7.4.1, and likely no longer works with GHC 6. (If you want to try it and can’t run GHC 7, let me know and I may be able to get it to work with 6.10.)
Provided that a recent
ghc is in your path, to build on UNIX it ought
to be be sufficient to type:
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
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:
% make clean; make FLAGS=-editlineor
% cabal install --flags=-editline alms
% make clean; make FLAGS=readlineor
% cabal install --flags=readline alms
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-devNote that libeditline is a completely different library, and installing that will not help.
“Practical Affine Types” paper © 2011 ACM. This is the author’s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. ACM SIGPLAN–SIGACT 2011 Symposium on Principles of Programming Languages 46:447–458, 2011. http://doi.acm.org/10.1145/1925844.1926436