alms: a practical affine language

This is a prototype implementation of Alms, an affine language with
modules and subtyping.

Please see http://www.ccs.neu.edu/home/tov/pubs/alms/ for more
information.

CONTENTS

 * GETTING STARTED
 * WHAT TO TRY
 * PAPER SYNTAX VERSUS ASCII SYNTAX
 * EDITLINE TROUBLE


GETTING STARTED

  Alms requires GHC to build.  It is known to work with GHC 6.12.1 and
  6.10.4, and likely no longer works with GHC 6.8.

  Provided that a 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 -l libsocketcap

  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 = Cons of `a * `a list | Nil
        -- built-in
    module Exn
        -- defined at "lib/libbasis.alms" (line 2, col. 3 to line 23, col. 3)
    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                           -o           (affine arrow)
  \to^{\hat\alpha}                -[a]>        (arrow with qualifier)
  \sqcup \sqcap                   \/ /\        (qualifier join and meet)
  \pm \baro + -                   = * + -      (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

   - Use readline instead:

       % make clean; make FLAGS=readline

   - 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.