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.

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 can be lambdas, applications, or other terms.

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)

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 = '\u4242'

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)))

It's possible to match different kinds of terms. These three forms are equivalent:

match list {
  (List.cons hd tl):  (Some hd)
  List.nil:  None
}

// If we don't provide field bindings, it will implicitly use
// the fields of the declared data type
match list {
  List.cons:  (Some list.head)
  List.nil:  None
}

match bind = list {
  List.cons:  (Some bind.head)
  List.nil:  None
}

Match native numbers:

match 4 {
  0:  "zero"
  5:  "five"
  4:  "four"
  _:  "other"
}

Which is the equivalent of nesting match terms:

match 4 {
  0: "zero"
  1+a: match (- (+ a (+ 0 1)) 5) {
    0: "five"
    _:  ...
  }
}

Match multiple terms:

λa λb match a, b {
  (Some True) (x, y): (Some (x, y))
  (Some False) (x, y): (Some (y, x))
  None *: None
}

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.