sysf-i386
=========

sysf-i386 is an implementation of System F in i386 assembly language.

Building
--------

Type `make' to build the executable (named `sysf'). The executable is a Linux
ELF binary. Only a POSIX shell should be required for the build. (In
particular, an assembler is not required.)

The build process is a bit slow, it takes about a minute on my machine.

Syntax
------

Names are made up of Latin letters, digits, and underscores.

Function types are written with an arrow ->, which is right-associative,
i.e. a -> b -> c is the same as a -> (b -> c). Quantification is written
with an ASCII simplification of a forall symbol \/. There is no delimiter
between the quantified type variable and the body of the quantifier.

type ::= NAME
       | type '->' type
       | '\/' NAME type
       | '(' type ')'

Term lambda terms are written with an ASCII simplification of a lower case
lambda \. Type lambda terms are written with an ASCII simplification of an
upper case lambda /\. Application are implicit.

term ::= NAME
       | '\' NAME ':' type term   ; term lambda abstraction
       | '/\' NAME term           ; type lambda abstraction
       | term term                ; application
       | '(' term ')'

Application is left-associative, i.e. a b c is the same as (a b) c. Lambda
terms (both kinds) extend as far to the right as possible, i.e. (a \x:t b) c
is the same as (a (\x:t b)) c.

To make the requirement of explicit type annotations more bearable, type
macros are supported. A type macro is defined on a line of its own, starting
with an octothorpe:

#Bool \/X X->X->X

From this point on, Bool can be used as a type. Type macros can also be
parameterised:

#Function[x y] x->y

Now, for example, Function[Bool Bool] refers to a function from Bool to Bool.
Macros may be redefined, later definition override earlier ones. Macro
expansion is hygienic.

Comments start with a semicolon and continue until the end of the line.

Evaluation
----------

sysf-i386 uses call-by-need evalution. Since the implementation is not very
smart, major space leaks may occur.

Input and output
----------------

Input and output is done bit by bit, LSB first.

Effects are modeled by an algebra of actions. The type of actions is usually
denoted as IO. The following operators are available:

fix: \/X ((X->IO)->(X->IO))->(X->IO)
  A loop.
  fix T f reduces to f (fix T f).
read: IO -> IO -> IO -> IO
  Try to read a single bit of input. Then:
  - If no more input is available, run the first argument.
  - If a 0 bit was read, run the second argument
  - If a 1 bit was read, run the third argument
  Just like read(2), even if one read call indicates end of input, subsequent
  read calls may produce more input (e.g. if input is from a terminal).
write0 : IO -> IO
  Write a 0 bit, then run the argument.
write1 : IO -> IO
  Write a 1 bit, then run the argument.
exit : IO
  Exit the program.

These operators are supplied as functions. Accordingly, the type of the entire
program must be:

\/IO
  (\/X ((X->IO)->(X->IO))->(X->IO)) ->     ; fix
  (IO->IO->IO->IO) ->                      ; read
  (IO->IO) ->                              ; write0
  (IO->IO) ->                              ; write1
  IO ->                                    ; exit
  IO