A foetus program consists of terms and definitions.
P | : : | empty program | |
---|---|---|---|
| | term; P | term to be evaluated | |
| | definition; P | definition for further use |
t | : : | x | variable |
---|---|---|---|
| | [x]t | lambda | |
| | tu | application | |
| | C(t) | constructor | |
| | case t of { C_{1}x_{1} t_{1}|...|C_{n}x_{n} t_{n} } | pattern matching | |
| | (C_{1} = t_{1},...,C_{n} = t_{n}) | tuple | |
| | t.C | projection | |
| | let x_{1} = t_{1},...,x_{n} = t_{n} in t | let | |
| | (t) | (extra parentheses) |
add = [x][y]case x of { O z => y | S x' => S(add x' y) }; one = S(O()); add one one;
Note that although O is a zero-argument-constructor the syntax forces us to supply a dummy variable z within the pattern definition and also empty tuple () in the definition of one.
t :
means ``in context term t is of type ''.
: : | -type | ||
---|---|---|---|
| | {C_{1} : |...|C_{n} : } | labeled sum type | |
| | (C_{1} : ,...,C_{n} : ) | labeled product type | |
| | {X} | polymorphic type | |
| | instantiation of polymorphic type | ||
| | Let X_{1} = ,...,X_{n} = in | recursive type |
Let = in [X_{1} : = Let = in X_{1};...;X_{n} : = Let = in X_{n}]
( = abbreviates X_{1} = ,...,X_{n} = ). Thus we can substitute congruent types:For ploymorphic types we have rules like in System F:
We here only briefly introduce the typing rules. For more detailed explanation, read a book about type theorie, e.g. [NPS90].
In foetus type checking is not yet implemented and it is assummed that all terms entered are well typed. Of course, only for well typed terms the termination check produces valid results.
f = [x]x x; a = f f;foetus output:
f passes termination check a passes termination checkRun example.