--------------------------------------------------------------------------------
--              Interpreters for Wadler's language's CP and GV                --
--------------------------------------------------------------------------------

This provides a small interpreter for Wadler's language CP and GV (although see later notes on
syntax and differences.)

Building
========

Building the CP and GV interpreters requires GHC and the following packages from
Hackage (all of which should be obtainable using cabal-install):

  alex
  happy
  wl-pprint
  haskeline

If you are building on Linux, the latter will probably require you to install
ncurses headers.  Once you have the necessary packages, the interpreters can be
built by running

  make

CP
==

Using
-----

The tool is primarily interactive (although you can, of course, redirect stdin
to avoid retyping long commands).  Commands can be any of the following, where
words in all upper-case are placeholders.

> type NAME = TYPE
> type NAME(VARS) = TYPE

Defines NAME to be an abbreviation for TYPE.  In the second case, if the VARS
are X1,X2,..., then NAME(T1,T2,...) abbreviates TYPE{T1/X1, T2/X2, ...}.
Variables must begin with an uppercase letter.

> def NAME = PROC
> def NAME(VARS) = PROC

Defines NAME to be an appreciation for process expression PROC.  In the second
case, substitution is as for types.  Variables can be either begin with an
uppercase letter, in which case they stand in for entire expressions, or a
lowercase letter, in which case they stand in for a name.

> PROC |- x1:TYPE, x2:TYPE, ...

Checks whether process expression PROC has the behavior given by x1:TYPE, ...,
and, if it does, attempts to find the normal form of PROC.

> :q

Exits the interpreter

An example session:
$ ./cpi
> type Church = forall X.?(X * ~X) || (~X || X)
> def Zero(x) = x(X).x(s).x(z).z<->x
> def Ping(x,y,w) = x[1].x[s].(!s(f).f(a).a().?y[u].u().f[].0 | x[z].(z[].0 | x().w[].0))
> nu x:Church. (Zero(x) | Ping(x,y,w)) |- y:?bot,w:1
w [] . 0
> :q
$

Differences from Wadler's language
----------------------------------

The notation for linear duals and the par combinator is difficult to type.
Instead, the tool uses "~A" to indicate the dual of A, and "P || Q" for P par Q.
Selection is indicated with a slash instead of brackets to simplifying parsing.

The form "x.case()" is not sufficient to determine the structure of a proof, as
the top rule allows arbitrary further linear assumptions to be discharged.
Instead, the form must be written "x.case{x1,x2,...}()", where the x_i are the
names of the additional assumptions to be discharged.

GV
==

Differences from Wadler's language
----------------------------------

The current implementation of GV modifies the sepcified syntax to be more
explicit about linearity and types.  This avoids the need to do much type
inference, and clarifies several edge cases.  Such cases include (in the
original syntax):

 |- let f = \x.x in f unit : Unit

There are (at least) two typings of this, one that assigns f the type Unit ->
Unit, and one that assigns it the type Unit -@ Unit.

 |- let f = \x.x in f (f unit) : Unit

There is only one typing of this, assigning f the type Unit -> Unit, but the
need for f to be unlimited is not apparent until its usage.

 |- let f = \x.x in \y. f y : Unit -> Unit

Again, there is only one typing.  Here, the need is expressed not by f being
used multiple times, but by '\y. f y' having an unlimited type, and thus only
have access to the unlimited environment.

Similar conundrums arise from the channel in 'with..connect..to'.  For example:

 |- with c connect
      let (f, c) = receive c in send (f unit) c
    to
      terminate (receive (send (\x.x) c))
  : Unit

Again, this types either with f having linear or unlimited type.

For the time being, I've avoided this problem by adding a number of annotations
to the syntax.  They are:

  Original
  --------
    \x.M    (either linear or unlimited functions, type of 'x' implicit)
  Modified
  --------
    \x:t.M  (linear, type of 'x' given by 't')
    !\x:t.M (unlimited, type of 'x' given by 't')

  Original
  --------
    with c connect M to N    (type of 'c' implicit)
  Modified
  --------
    with c:t connect M to N  (type of 'c' given by 't'; as in the original c has
                              type '~t' in N)