HVM-Lang is an Intermediate Representation for HVM-Core that provides a higher level syntax to write programs based on the Interaction-Calculus.
With the nightly version of rust installed, clone the repository:
git clone [email protected]:HigherOrderCO/hvm-lang.git
cd hvm-lang
Install with cargo:
cargo install --path .
First things first, let's write a basic program that adds the numbers 3 and 2.
main = (+ 3 2)
HVM-Lang searches for the main | Main
definitions as entrypoint of the program.
To run a program using hvm-lang you can use the argument run
, like below:
hvm-lang run <file>
It will show the number 5 and also some stats like time and rewrites.
You can pass the option --mem <size>
to limit the memory amount of the runtime. The default is 1GB.
hvm-lang --mem 65536 run <file>
To compile a program you can use the compile
argument:
hvm-lang compile <file>
It will output to stdout the compiled file.
HVM-Lang syntax consists in Terms and Definitions. A Term is something that holds value, it can be a Number, an Application, a Function, etc. A Definition points to a Term.
Here we have a definition 'two' to the number 2.
two = 2
Here we have a lambda, the lambda's body is the variable x.
id = λx x
Operations can handle just 2 terms at once.
some_val = (+ (+ 7 4) (* 2 3))
The current operations are: +, -, *, /, %, ==, !=, <, >, &, |, ^, ~, <<, >>
.
A let term, we use it to bind some value to the next term, in this case (* result 2)
.
let result = (+ 1 2); (* result 2)
It is possible to define tuples.
tup = (2, 2)
And pattern-match the tuple with the let.
let (x, y) = tup; (+ x y)
It is possible to duplicate terms using dup
.
// the number 2 in church encoding using dup.
ch2 = λf λx dup f1 f2 = f; (f1 (f2 x))
// the number 3 in church encoding using dup.
ch3 = λf λx dup f0 f1 = f; dup f2 f3 = f0; (f1 (f2 (f3 x)))
HVM-Lang has a match syntax for machine numbers. We match the case 0 and the case where the number is greater than 0, p binds the value of the matching number - 1.
to_church = λn match n {
0: λf λx x;
1+p: λf λx (f (to_church p f x))
}
Also, it is possible to use global lambdas, where the variable occurs outside it's body:
($a (λ$a 1 λb b))
This term will reduce to:
(λb b 1)
1
How terms are compiled into interaction net nodes?
HVM-Core has a bunch of useful nodes to write IC programs.
Every node contains one main
port 0
and two auxiliary
ports, 1
and 2
.
There are 6 kinds of nodes, Erased, Constructor, Reference, Number, Operation and Match.
A lambda λx x
compiles into a Constructor node.
An application ((λx x) (λx x))
also compiles into a Constructor node.
We differentiate then by using the ports.
0 - Points to the lambda occurrence 0 - Points to the function
| |
λ @
/ \ / \
1 2 - Points to the lambda body 1 2 - Points to the application occurrence
| |
Points to the lambda variable Points to the argument
So, if we visit a Constructor at port 0 it's a Lambda, if we visit at port 2 it's an Application.
Also, nodes have labels, we use the label to store data in the node's memory and also differentiate them.
The Number
node uses the label to store it's number.
An Op2
node uses the label to store it's operation.
And a Constructor
node can have a label too! The label is used for Dup
and Tuple
nodes.
Check HVM-Core to know more about.
The HVM-Core is an eager runtime, for both CPU and parallel GPU implementations. Because of that, is recommended to use supercombinator formulation to make terms be unrolled lazily, preventing infinite expansion in recursive function bodies.
Consider the code below:
Zero = λf λx x
Succ = λn λf λx (f n)
ToMachine = λn (n λp (+ 1 (ToMachine p)) 0)
The lambda terms without free variables are extracted to new definitions.
ToMachine0 = λp (+ 1 (ToMachine p))
ToMachine = λn (n ToMachine0 0)
Definitions are lazy in the runtime. Lifting lambda terms to new definitions will prevent infinite expansion.
Consider this code:
Ch_2 = λf λx (f (f x))
As you can see the variable f
is used more than once, so HVM-Lang optimizes this and generates a duplication tree.
Ch_2 = λf λx dup f0 f0_ = f; dup f1 f1_ = f0_ = (f0 (f1 x))
- Data types
- Pattern matching