diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 101 |
1 files changed, 101 insertions, 0 deletions
@@ -0,0 +1,101 @@ +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 |