|
||
---|---|---|
.github/workflows | ||
docs | ||
examples | ||
src | ||
tests | ||
.clippy.toml | ||
.gitignore | ||
.rustfmt.toml | ||
Cargo.lock | ||
Cargo.toml | ||
cspell.json | ||
justfile | ||
README.md | ||
rust-toolchain.toml |
HVM-Lang
HVM-Lang is a lambda-calculus based language and serves as an Intermediate Representation for HVM-Core, offering a higher level syntax for writing programs based on the Interaction-Calculus.
Compilers that want to target the HVM should compile the source language to HVM-lang, which takes care of converting interaction calculus into the underlying interaction networks.
Note that HVM-lang is untyped and does not guarantee correctness or soundness. Compilers that don't want to implement the necessary check can instead transpile to the Kind language, which compiles to HVM-lang and implements type-level checking.
Programmers looking for an HVM-based programming language should also use Kind, which is designed to be user-interfacing.
Installation
With the nightly version of rust installed, clone the repository:
git clone https://github.com/HigherOrderCO/hvm-lang.git
cd hvm-lang
Install using cargo:
cargo install --path . --locked
Usage
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, use the run
argument:
hvml run <file>
It will show the number 5.
Adding the --stats
option displays some runtime stats like time and rewrites.
To limit the runtime memory, use the --mem <size> option.
The default is 1GB:
hvml --mem 65536 run <file>
You can specify the memory size in bytes (default), kilobytes (k), megabytes (m), or gigabytes (g), e.g., --mem 200m.
To compile a program use the compile
argument:
hvml compile <file>
This will output the compiled file to stdout.
There are compiler options through the CLI. Click here to learn about them.
Syntax
HVM-Lang files consists of a series of definitions, which bind a name to a term. Terms include lambda-calculus abstractions and applications, numbers, tuples, among others.
Here's a lambda where the body is the variable x
:
id = λx x
Lambdas can also be defined using @
.
To discard the variable and not bind it to any name, use *
:
True = @t @* t
False = λ* λf f
Applications are enclosed by (
)
.
(λx x λx x λx x)
This term is the same as:
(((λx x) (λx x)) (λx x))
Parentheses around lambdas are optional. Lambdas have a high precedence
(λx a b) == ((λx a) b) != (λx (a b))
*
can also be used to define an eraser term.
It compiles to an inet
node with only one port that deletes anything that’s plugged into it.
era = *
A let term binds some value to the next term, in this case (* result 2)
:
let result = (+ 1 2); (* result 2)
The use
term inlines clones of some value to the next term:
use result = (+ 1 2); (* result result)
// Equivalent to
(* (+ 1 2) (+ 1 2))
The same term with let
duplicates the value:
let result = (+ 1 2); (* result result)
// Equivalent to
let {result_1 result_2} = (+ 1 2); (* result_1 result_2)
Duplications efficiently share the same value between two locations, only cloning a value when it's actually needed, but their exact behaviour is slightly more complicated than that and escapes normal lambda-calculus rules. You can read more about it in Dups and sups.
It is possible to define tuples:
tup = (2, 2)
And destructuring tuples with let
:
let (x, y) = tup; (+ x y)
Strings are delimited by "
"
and support Unicode characters.
main = "Hello, 🌎"
A string is desugared to a String data type containing two constructors, String.cons
and String.nil
.
// These two are equivalent
StrEx1 = "Hello"
data String = (String.cons head tail) | String.nil
StrEx2 = (String.cons 'H' (String.cons 'e', (String.cons 'l' (String.cons 'l', (String.cons 'o' String.nil)))))
Characters are delimited by '
'
and support Unicode escape sequences. They have a numeric value associated with them.
main = '\u{4242}'
Lists are delimited by [
]
and elements can be optionally separated by ,
.
ids = [3, 6, 9 12 16]
A list is desugared to a List data type containing two constructors, List.cons
and List.nil
.
// These two are equivalent
ListEx1 = [1, 2, 3]
data List = (List.cons head tail) | (List.nil)
ListEx2 = (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))
Hvm-lang supports pattern matching through match
and switch
terms.
match
pattern matches on constructors declared with data
.
data Option = (Some val) | None
// 'match' implicitly binds a variable for each field in the constructor.
// The name of the bound variable depends on the name of the argument.
map f x = match x {
Some: (Some (f x.val))
None: None
}
// You can give a name to the match argument to access its fields.
TakeErr fallible_fn x errs =
match res = (fallible_fn x) {
// We can now access res.val.
// If no name is given, it will be inaccessible.
Result.ok: ((Some res.val), errs)
Result.err: (None, (List.cons res.val errs))
}
switch
pattern matches on native numbers:
match x = 4 {
// From '0' to n, ending with the default case '_'.
0: "zero"
1: "one"
2: "two"
// The default case binds the name <arg>-<n>
// where 'arg' is the name of the argument and 'n' is the next number.
// In this case, it's 'x-3', which will have value (4 - 3) = 1
_: (String.concat "other: " (String.from_num x-3))
}
Which is the equivalent of nesting match terms:
match x = 4 {
0: "zero"
_: match x-1 {
0: "one"
_: use x-2 = x-1-1; match x-2 {
0: "two"
_: use x-3 = x-2-1; (String.concat "other: " (String.from_num x-3))
}
}
}
More features
Key:
- 📗: Basic resources
- 📙: Intermediate resources
- 📕: Advanced resources
Other features are described in the following documentation files:
- 📗 Lazy definitions: Making recursive definitions lazy
- 📗 Data types: Defining data types
- 📗 Pattern matching: Pattern matching
- 📗 Native numbers and operations: Native numbers
- 📗 Builtin definitions: Builtin definitions
- 📗 CLI arguments: CLI arguments
- 📙 Duplications and superpositions: Dups and sups
- 📙 Scopeless lambdas: Using scopeless lambdas
- 📙 Tagged lambdas and applications: Automatic vectorization with tagged lambdas
- 📕: Fusing functions: Writing fusing functions
Further reading
- 📙 Compilation and readback
- 📙 Old HVM wiki learning material. It is outdated, but it can still teach you some of the basics.