INTRODUCTION
=================

This system is derived from linear type theory, such that for a value x with type A:

(x : A) means that x must be used exactly once.
(x : ?A) means that x may be used at most once, or forgotten.
(x : !A) means that x may be used multiple times, but at least once.
(x : ?!A) means that x may be used zero or more times.

? is read "why not", and ! is read "of course".

Additive means "there are two possibilities, but you only get one". In other words,
  in each branch of an additive relationship, all of the non-? variables in the
  context must be disposed of.
Multiplicative means "you get both of these at once". In other words, all of the
  non-? variables must be disposed of as a whole.
Conjunction means "both values exist at once".
Disjunction means "only one of these values exist at once".

Additive conjunction (a & b) means "you can use either a or b, it's up to you which".
Additive disjunction (a + b) means "I am going to give you an a or a b, and you must
  be prepared to deal with either, but not both at the same time."
Multiplicative conjunction (a * b) means "I am going to give you an a and a b, and
  you have to use both".
Multiplicative disjunction (a | b) means "you must be prepared to recieve both an a
  and a b, but ultimately only one will be used". If that's a bit confusing, that's alright.


AXIOM
=====

a | -a

where -a represents the dual of a, and | represents multiplicative disjunction.
This is the axiom of the excluded middle, meaning to "a is true or not true".
Its implementation is explained in "multiplicative disjunction". There are no
further axioms.


Duals:

While they're a general construct, the dual is actually only used for the
definition of the axiom, so I'll specify it here:

  -(-a) = a
  -(a & b) = -a + -b
  -(a * b) = -a | -b
  -Top = 0
  -1 = Bottom
  -(!a) = ?(-a)

and vice versa in all cases.


Distributivity:

This isn't actually related to the axiom, but I might as well while I'm at it.
None of these are built-in rules, they are just helpful notions provable within
the language itself. These are the distributive laws:

  a * (b + c) = (a * b) + (a * c)
  a | (b & c) = (a | b) & (a | c)
  a * 0 = 0
  a & Top = Top

notice how "exponentials" convert "addition" into "multiplication"-- hence the names:

  !(a & b) = !a * !b
  ?(a + b) = ?a | ?b
  !Top = 1
  ?0 = Bottom

and vice versa in all cases in both sets listed.


STRUCTURAL RULES
================

The weakening and contraction rules are specified twice since
I hope to extend this into an ordered logic, so I have to include
the exchange-requiring equivalents. This is also true for constructors and
eliminators in the computational rules. All of these can be implemented only
once, with the second rule being implemented in terms of the first via a swap
that /doesn't/ apply an unordered constraint. If I do not extend this to an
ordered logic, you can simply ignore all of the second rules.

Weakening: a -> ?b -> a ### const
           ?a -> b -> b ### flip const
Contraction: (a -> !a -> b) -> (!a -> b) ### join
             (!a -> a -> b) -> (!a -> b) ### join . flip
Exchange: (a -> b -> c) -> (b -> a -> c) ### flip
 (or equivalently (a * b) -> (b * a))

(todo: do I need a dual exchange rule for &?)


COMPUTATIONAL RULES
===================

These are the introduction and elimination rules for compound terms in the
language. Introduction terms are labeled with an i, elimination terms with an e.
When multiple introduction/elimination rules are required, they are each labelled
with a number.


Additive conjunction (with):

Topi1 : a -> a & Top
Topi2 : a -> Top & a
additively (all of the context is used in either branch of the options a and b),
    &i : a -> b -> a & b
&e1 : a & b -> a
&e2 : a & b -> b

The eliminators may be called "projections".

There is no elimination rule for Top, since it doesn't exist. It can only
be introducted in terms of the type signatures in Top1 and Top2, and the
only thing you can do with it is ignore it via the associated projection.
It doesn't have to exist because nothing using the projection for Top
can exist because it cannot be used for anything, nor weakened.

Additive conjunction can be interpreted as a pair of procedure pointers,
with the context enclosed inside. The projections are function calls that
choose which procedure to invoke to consume the context. A call to Top
is equivalent to nontermination, since Top doesn't exist.

The compiler could probably safely maybe automatically insert the
eliminators when the corresponding type is required, but I haven't totally
thought this through, and there are potential issues with e.g.
(a & b) & a, in the event that choice of a matters.


Additive disjunction (plus):

0e : 0 -> a
+i1 : a -> a + b
+i2 : b -> a + b
+e1 : (a -> c) & (b -> c) -> (a + b -> c)
+e2 : (b -> c) & (a -> c) -> (a + b -> c)

0, like Top, does not exist. It only exists as a fragment of the type
signature in disjunction introduction, because
  +i1 (x : A) : forall b. A + b
and 0 is simply an instanciation of b, taking the entire forall thing
far too literally, as shown in its eliminator. It is impossible to
have an actual instance of 0, because by definition, it is the type
not selected when you create a +. In terms of elimination, all eliminations
of an 0 + a type are equivalent to (e1 0e), with the exception of the fact
that you have to destroy anything in your context that cannot be weakened.
This can be trivially implemented as using 0e to generate a function type
that directly consumes all of the terms in the context, and returning a c.

The eliminators are rather intuitive. The choice of & is necessary because
each option must entirely dispose of its context, as is in the definition
of &i.

A value of a + b is trivial: it's just a tagged union, i.e. an indicator
of whether it's a or b, and the value a or b.


Multiplicative conjunction (times):

1i : 1
1e1 : 1 * a -> a
1e2 : a * a -> a
*i : a -> b -> a * b
*e1 : a * b -> (a -> b -> c) -> c
*e2 : (a -> b -> c) -> a * b -> c

1 does exist, and in fact its sole introduction rule is "1 exists", but
it holds no information, so in practice it doesn't have to be stored.
Formally it has only one elimination rule, 1 -> <nothing>, but a function
can't return nothing, so instead you have to eliminate it via its definition
as the identity element.

The rest of it is pretty intuitive. In memory, it's just a pair of values.


Multiplicative disjunction (par):

Bottomi1 : a -> a | Bottom
Bottomi2 : a -> Bottom | a
Bottome : Bottom -> a
|i : ?a * ?b -> a | b
|e1 : ?(a -> c) * ?(b -> c) -> a | b -> c
|e2 : a | b -> ?(a -> c) * ?(b -> c) -> c

Multiplicative disjunction is by far the least intuitive operator, corresponding
to delimited continuations and functions.

Bottom does not exist. Like with additive disjunction, it's just part of
the type signature, and it simply exists to not get chosen.

As you can see, |e produces only one c despite having two options, both
of which are provided in |i. That's because |e is inherently
nondeterministic. |i and |e are both entirely weakened because neither
choice will necessarily be chosen, yet they both must exist in full. This means
the entire closure that they are in must be somehow weakened, since it's
not possible to dispose of a full value in both branches at once, because
that would constitute double use. The use of the * in the signature is to
emphasize the relationship to multiplicative conjunction and that behavior,
just as additive disjunction is defined in terms of additive conjunction.

A par value is implemented in terms of a pair of function calls. In the
eliminator, either function may be invoked, and when the value is used,
the eliminator may choose to forget the function halfway through and jump
to the other option instead, making it equivalent to a continuation, the
functional equivalent to a goto.

The main use of par is in the sole axiom of the excluded middle, which encodes
the equivalent to functions and delimited continuations. For reference, the type
of a function is defined as (a -> b = -a | b). Essentially, the axiom can't pull
a value of type A out of thin air, so it is forced to choose the -a branch.
-a is equivalent to a -> Bottom, and therefore can only be used by providing a
value of type a, so instead of actually providing that Bottom, the function
simply jumps to the branch that demanded an a in the first place and returns
that result. Functions are implemented the same way, only kinda in reverse:
it runs the side that claims to have an extra a it needs to dispose of, and then
once it gets that hole, it produces the a in the other branch and terminates.
Implicitly in either case the context is consumed, which is equivalent to the
function returning. As you can see though, these are simply different
perspectives on the same axiom.

If you don't get it, that's fine, because it's super confusing, and I don't
understand it either.


TYPECLASSES & MODULES
=====================

I haven't really figured out typeclasses. Basically I intend for them to be
existential types (via dependent sums maybe?), but I need to figure out how to
make it practical first.

Requirements:
* It must be possible to use the instanced values without having to unwrap the
class implementation manually first.
* It must be possible to use the function instances equally easily, and without
having to declare the names at each usage point.
* They must permit non-unique instances.
* Instances must be stackable, the outermost one being used unless the inner one
is exposed within one of the instance type-contextual manipulations (e.g. functor).
This is important especially since Copy should implement !, but it should be
possible to rc a copiable variable and have it behave as expected. Copy is
described in more detail in Mutation.

Modules are essentially the same thing as typeclasses, and have similar
requirements. The answer to both probably lies in the same place. Lightweight
modules that are as easy to use as typeclasses would be a major plus too.

I don't suspect this problem will be all that hard to resolve.


As far as ! and ? go, they are essentially typeclasses. @ below is a typeclass
too. Essentially, these are the introduction rules for ! and ?, though these
are not possible to derive without external functions (for obvious reasons),
and being typeclasses, it's not appropriate to give them introduction rules.

To specify a !, you need a class instance satisfying either the contraction rule,
or equivalently, the following:
    !i : a -> !(() -> a)

To specify a ?, you need a class instance satisfying either the weakening rule,
or equivalently, the following:
   ?i : a -> ?(a -> ())

The reason these are essentially introduction rules is made more obvious if you
wrap the entire thing into a (-> !a) or (-> ?a) respectively.


MUTATION
========

@ means "mutable" to the compiler. Normal values are immutable, which means to
make changes, the entire object has to be deconstructed and reconstructed again.
Mutation allows direct modification to the data structure without concern.
Generally things are mutable by default, but this may not be the case with
external values, or internal values via pointers.

@ extends ?, which means a mutable pointer may be freed, but not !, so that
you cannot have multiple instances of a mutable pointer.

Losing mutation in favor of replication:
   rc : @a -> !?a, introducing a reference-counted pointer

Some values may implement Copy, allowing deep duplication. All composite
structures may automatically derive Copy whenever both of their constituents
are !. Copy, of course, is an implementation of !, though using (rc) anyway
may be desirable for performance reasons, especially for highly composite
structures.
   copy : Copy a => a -> @a

Generally, syntactic sugar should eliminate most of this crap such that the
programmer shouldn't have to deal with it most of the time.