We start with a very simple but complete Kernel/CORE program, unat.k.
Contents |
Usually a program starts with a brief description of what it does. In our case we have:
/* Example of unary encoding of natural number with
addition (add) and multiplication (mult) */
In Kernel/CORE, any text between /* ... */ or (* ... *) and any line starting with "--", "%", "//", or "#" is a comment which is ignored by the compiler/interpreter.
Unlike most of programming languages, Kernel/CORE does not have any predefined types. That means that in order to manipulate any data, we first have to define the syntax for the data. In Kernel/CORE, every value is typed; a textual representation of a value makes sense only if we know the type of the value.
-- recursive type definition <type> unat <is> ['o, 'i unat ] ;
Every Kernel/CORE statment ends by a semicolon. The above statement introduces a type called unat and, at the same time, it defines the syntax for the textual representation of values of that type. Square brackets represent variants, i.e., disjoint union of the elements listed between the square brackets. Thus a unat value is:
-- few natural numbers in our encoding unat zero = 'o ; unat one = 'i'o ; unat two = 'i'i'o ; unat three = 'i'i'i'o ; unat four = 'i three ;
Kernel/CORE relations are binary, i.e., they take one value as an argument and return one value as a result. We introduce a new type upair being a pair of unat's. The type will be the argument for relations add (addition) and mult (multiplication).
<type> upair <is> {'x unat, 'y unat};
Curly brackets introduce records, i.e., product types.
Actually, in Kernel/CORE we have only those two type constructions, namely union (variant) and product (record). These two constructions introduce labels. The labels can be seen as field names. In order to distinguish the labels from other identifiers (such as types names or relation names), the labels are prefixed by a quote, such as 'x or 'i . A very special type is the empty product, called unit and denoted by {}. There is only one value of unit type. This value is also denoted by {}. The type expression ['o, 'i unat ] in the recursive definition of unat is in fact an abbreviation of ['o {}, 'i unat ], and the value written as 'o is an abbreviation of 'o {}.
Relation add, for addition, is defined recursively, as the union (merge) of relations:
(upair -> unat) add = [ -- if 'x = 0 and 'y is of any value (represented by "..."), then 'y. ($arg {'x 'o , 'y ...} -> $arg.y), -- if 'x = 1 + z, then return (1 + (z + y)). Notice, that -- the default name of the argument is the empty string, -- thus we write $.y in order to refer to the field "y" of -- the actual argument. ({'x 'i ..., ...} -> 'i [{'x $.x.i, 'y $.y} :: add] ) -- A list of relations within square brackets represents in -- general the union of the relations. However, we can use -- the square brackets around a single relation to force a -- particular grouping (i.e., as parenthesis). -- -- An expression ['i f :: g] is parsed as [['i f] :: g] -- since label constructor binds stronger than composition. ];
A statement defining a relation starts with description of the relation type, e.g., (upair -> unat), where upair is the type of the argument and unat is the type of the result. The type description is followed by the name of the relation, here add. By convention, a relation type description such as ({} -> res_type) rel_name = ... can be abbreviated by res_type rel_name = ..., and ({} -> {}) rel_name = ... by rel_name = ... (see the definitions of relations zero, one, ... of type ({} -> unat) above, and of main of type ({} -> {}) below).
The actual expression defining the relation follows the sign =. In our case, relation add is defined as the union (the meaning of the square brackets) of two auxiliary relations:
In both cases the expressions define anonymous relations using abstraction, i.e., construct of the form ($x Pattern -> Expression). Intuitively, relation ($x Pattern -> Expression) is defined for argument values matching pattern Pattern, returning as the result the evaluation of Expression in which every free occurrence of $x is substituted by the actual value of the argument. The first expression is defined when the field 'x of the argument equals 'o (i.e., zero). In that case, the relation returns the value of the field 'y of the argument ($arg.y). The second expression uses the value construction via label constructor 'i [...]. The argument of the label constructor, i.e., {'x $.x.i, 'y $.y} :: add, corresponds to the relation composition (::) of a constant relation {'x $.x.i, 'y $.y} and relation add.
Definition of the multiplication is very similar to the addition. Notice, that here we use an anonymous type {'x unat, 'y unat} as the argument instead of upair. The both types are strictly equivalent.
({'x unat, 'y unat} -> unat) mult = [
({'x 'o , ...} -> 'o),
( ... -> {'x [{'x $.x.i , 'y $.y} :: mult], 'y $.y}) :: add
];
The following relation test takes a natural number n and produces a 4-uplet consisting of {'x=n, 'twice=n+n, 'four_times=n+n+n+n, 'square=n*n }.
<type> test <is> {'x unat, 'twice unat, 'four_times unat, 'square unat}; (unat -> test) test = ( ... -> {'x $, 'twice {'x $, 'y $} :: add, 'four_times {'x @twice, 'y @twice} :: add, -- We may refer to the value of one of the previous -- fields using its name prefixed by "@". 'square {'x $, 'y $} :: mult} );
We communicate with a kernel program through unidirectional pipes, also called FIFOs (first-in-first-out). There are two kings of FIFOs: input and output. They are declared in the following way:
unat get_unat = <input>; -- input pipe which carries values of type "unat" (test -> {}) print_unat = <output>; -- output pipe of type "test"
By default, the top level (starting) relation is called main.
main = get_unat :: test :: print_unat;
By default under Linux, input and output pipes are just files in the current working directory. If file get_unat consists of
--- get_unat ------------------------------------------------- 'i'i'o; ---------------------------------------------------------------
then the execution of the program produces (or overwrites) file print_unat with the following content:
--- print_unat ------------------------------------------------ {'x 'i 'i 'o {}, 'twice 'i 'i 'i 'i 'o {}, 'four_times 'i 'i 'i 'i 'i 'i 'i 'i 'o {}, 'square 'i 'i 'i 'i 'o {}}; ---------------------------------------------------------------
Try by yourself. Create a new directory, e.g., by doing in your terminal
mkdir foo
Then download the interpreter, the Kernel/CORE program, and create the input file:
cd foo wget http://fraczak.dyndns.org/wojtek/CORE/k wget http://fraczak.dyndns.org/wojtek/CORE/Examples/unat.k echo "'i'i'o;" > get_unat
Check the file permissions and then run the program:
chmod a+rx k ./k < unat.k
A file "print_unat" should be created. You may look into it:
cat print_unat