Juvix

CI status

pages-build-deployment

LICENSE Juvix Mascot

Description

Juvix is a research programming language created by Heliax as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling validity predicates to the C language, which can be deployed to various distributed ledgers including Anoma.

The Juvix language and related tools are documented in the Juvix book. To write and test Juvix programs, you can use your favorite text editor and the juvix command line tool. However, we recommend using the juvix-mode in Emacs or the plugin in VSCode.

First examples of programs written in Juvix

The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running juvix html --recursive FileName.juvix.

The Juvix standard library contains common functions that can be used in Juvix programs.

Quick Start

Installing Juvix on MacOS

The easiest way to install Juvix on MacOS is by using Homebrew.

To install the homebrew-juvix tap, run:

brew tap anoma/juvix

To install Juvix, run:

brew install juvix

After installing Juvix, you might want to try our doctor to check your system setup:

juvix doctor

Helpful information on the shell can also be obtained by running:

brew info juvix

Building Juvix from the sources

To install Juvix from the sources, you must download the Github repository. Then, the program can be installed with the following commands. We assume have Stack installed.

git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install

If the installation succeeds, you must be able to run the Juvix command from any location. To get the complete list of commands, please run juvix --help.

On MacOS, you can alternatively run the following command for Homebrew. The flag --HEAD used below is optional, mostly to build the latest version of Juvix in the main branch on Github.

brew install --build-from-source --HEAD juvix --verbose

The Hello World Example

In the following example a Juvix file is compiled to Wasm. Please check out the documentation Installing dependencies for instructions on how to setup your environment for compiling Juvix. You can also run juvix doctor to check your system setup.

-- HelloWorld.juvix
module HelloWorld;

open import Stdlib.Prelude;

main : IO;
main ≔ putStrLn "hello world!";

end;

Then, run the following commands at the location folder of the file HelloWorld.juvix:

juvix compile HelloWorld.juvix
wasmer HelloWorld.wasm

You should see the output: hello world!

The Juvix programming language

Juvix allows us to write programs with a high degree of assurance. The Juvix compiler runs several static analyses during the compilation phase to guarantee no runtime errors. Analyses permormed during this phase include scope, termination, arity, and type checkiqng. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors.

Some of the language features in Juvix include:

  • unicode syntax
  • parametric polymorphism
  • inductive and parametric data types
  • higher-order functions
  • implicit arguments
  • holes in expressions
  • axioms for non-computable terms

Additionally, the foreign and compile blocks syntax enable developers to compile a program to different backends including the C language. The Juvix module system further permits splitting programs into several modules to build libraries which can be later documented by generating HTML files based on the codebase, see for example, the Juvix standard library's website. For futher details, please refer to the Juvix book which includes our latest updates.

Coming soon

For the language:

  • lambda expressions
  • let expressions
  • tail call optimization
  • inference for mutually recursive functions
  • compilation to circuits
  • coverage checking (i.e. exhaustiveness and useless clauses)

For the compiler:

  • Init command
  • Better documentation tool: juvix doc MyFile.juvix

Community

We would love to hear what you think of Juvix! Join us on the Anoma Discord.

Changelog

Juvix Mascot

v0.2.3 (2022-08-15)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.2 (2022-07-25)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.1 (2022-07-12)

Full Changelog

Implemented enhancements:

Fixed bugs:

Merged pull requests:

v0.2.0

(2022-06-28)

Full Changelog

Implemented enhancements:

Fixed bugs:

  • Fix: Ignore implicit patterns and arguments in termination checking #172 (janmasrovira)
  • Fix: pretty printing for terminating keyword #145 (jonaprieto)

Merged pull requests:

v0.1.4

(2022-05-30)

Full Changelog

Merged pull requests:

Implemented enhancements:

Fixed bugs:

  • Missing error messages when using throw/error #117
  • Fix highlight of comments #104
  • Fix juvix-mode coloring for projects with multiple modules #101
  • Fix highlight command for modules with import statements #102 (janmasrovira)

Closed issues:

  • Deprecate the class JuvixError #115
  • Add ToGenericError instance for the infix parsing errors #114
  • Compile to WASM without linking libc #112
  • Add the termination checker to the pipeline #109
  • Use clang + wasi-sdk instead of emcc to compile to WASM #103
  • Move developer tooling docs out of README #95
  • Add pre-commit checks to CI checks #94
  • Support higher order functions in C backend #90
  • Remove dev from the list of branches in the CI #89
  • Refactor warning related stuff #87
  • The Juvix website #51

v0.1.3

(2022-05-05)

Full Changelog

Closed issues:

  • Monomorphisation naming inconsistency #84
  • Remove BackendAgda #83
  • Change terminating keyword behavior #81
  • MonoJuvix ExpressionTyped is never used #79
  • Bump stackage nightly and delete allow-newer: true from stack.yaml #75
  • Generate automatically CHANGELOG and Github Release Notes #73
  • Make flag –show-name-ids global #61
  • Add C code generation backend #60
  • Add polymorphism #59
  • Add the compile keyword to the frontend syntax (support up to Scoping) #58
  • Error with undefined or underscores #54
  • Add support for other GHC and Stack stable version #52
  • Autodetect output ANSI support when prettyprinting #38
  • Terminating for type signatures #11

Merged pull requests:

v0.1.2

(2022-04-11)

Full Changelog

Closed issues:

  • Add en emacs mode with support for scoped highlighting #25
  • Add support for project root detection through a juvix.yaml file #24
  • Add CLI cmd to generate juvix autocompletion files for fish and zsh #23
  • Add pretty and typecheck subcommands to the microjuvix CLI #21
  • Translate identifiers from MicroJuvix to MiniHaskell (valid Haskell) #19
  • Implement the MiniHaskell to Haskell translation (prettyprinter) #18
  • Implementation of a typechecker for MicroJuvix #16
  • Add references to the Abstract AST to update compilation to MiniHaskell #12
  • Order in the house #10

Merged pull requests:

v0.1.1

(2022-03-25)

Full Changelog

  • Add support in the parser/scoper for Axiom backends
  • Add support for foreign keyword
  • Add flag --no-colors for the scope command
  • Upgrade to GHC 9.2.2
  • Improve resolution of local symbols in the scoper
  • Several new tests related to ambiguous symbols
  • Add --version flag
  • Add InfoTableBuilder effect for the scoper

Closed issues:

  • Add diff output to the test suite #9
  • Improve scoper ambiguity error messages #8

Quick Start

Juvix Mascot

To install Juvix, you can download its sources using Git from the Github repository. Then, the program can be downloaded and installed with the following commands. You will need to have Stack installed.

git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install

If the installation succeeds, you must be able to run the Juvix command from any location.

To get the complete list of commands, please run juvix --help.

Installing dependencies

The following dependencies are only required for compiling to WASM.

  • wasmer
  • Clang / LLVM version 13 or later (NB: On macOS the preinstalled clang does not support the wasm target so use brew install llvm instead for example)
  • wasi-sdk
  • wasm-ld - the LLVM linker for WASM (NB: On linux you may need to install the lld package, on macOS this is installed as part of llvm).

To install wasi-sdk you need to download libclang_rt and wasi-sysroot precompiled archives from the wasi-sdk release page and:

  1. Extract the libclang_rt.builtins-wasm32-wasi-*.tar.gz archive in the clang installation root (for example /usr/lib/clang/13 on Ubuntu or `brew --prefix llvm` on macos).

    For example on macos with homebrew clang:

    cd `brew --prefix llvm`
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/libclang_rt.builtins-wasm32-wasi-15.0.tar.gz -OL
tar xf libclang_rt.builtins-wasm32-wasi-15.0.tar.gz

  2. Extract the wasi-sysroot-*.tar.gz archive on your local system and set WASI_SYSROOT_PATH to its path.

    For example:

    cd ~
curl https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-15/wasi-sysroot-15.0.tar.gz -OL
tar xf wasi-sysroot-15.0.tar.gz
export WASI_SYSROOT_PATH=~/wasi-sysroot

Examples of programs written in Juvix

The following links are clickable versions of their corresponding Juvix programs. The HTML output can be generated by running juvix html --recursive FileName.juvix.

The Juvix standard library contains common functions that can be used in Juvix programs.

Example Juvix Web apps

The following links navigate to example Juvix programs running as Web apps:

NodeJS Interop

A Juvix module can be compiled to a Wasm module. When a Wasm module is instantiated by a host, functions from the host can be injected into a Wasm module and functions from the Wasm module can be called by the host.

In this tutorial you will see how to call host functions in Juvix and call Juvix functions from the host using the Wasm mechanism.

The Juvix module

The following Juvix module has two functions.

The function hostDisplayString is an axiom with no corresponding compile block that implements it. We will inject an implementation for this function when we instantiate the module from NodeJS.

The function juvixRender is a normal Juvix function. We will call this from NodeJS.

-- NodeJsInterop.juvix
module NodeJsInterop;

open import Stdlib.Prelude;

axiom hostDisplayString : String → IO;

juvixRender : IO;
juvixRender ≔ hostDisplayString "Hello World from Juvix!";

end;

Compiling the Juvix module

The Juvix module can be compiled using the following command:

juvix compile -r standalone NodeJsInterop.juvix

This will create a file containing a Wasm module called NodeJsInterop.wasm.

The NodeJS module

The following NodeJS module demonstrates both calling a Juvix function from NodeJS and injecting a NodeJS function into a Juvix module.

The NodeJS function hostDisplayString is passed to the Wasm module NodeJSInterop.wasm when it is instantiated. After instantiation the Juvix function juvixRender is called.

The functions ptrToCstr and cstrlen are necessary to convert the char pointer passed from Juvix to a JS String.

-- NodeJSInterop.js
const fs = require('fs');
let wasmModule = null;

function cstrlen(mem, ptr) {
    let len = 0;
    while (mem[ptr] != 0) {
        len++;
        ptr++;
    }
    return len;
}

function ptrToCstr(ptr) {
    const wasmMemory = wasmModule.instance.exports.memory.buffer;
    const mem = new Uint8Array(wasmMemory);
    const len = cstrlen(mem, ptr);
    const bytes = new Uint8Array(wasmMemory, ptr, len);
    return new TextDecoder().decode(bytes);
}

function hostDisplayString(strPtr) {
    const text = ptrToCstr(strPtr);
    console.log(text);
}

const wasmBuffer = fs.readFileSync("NodeJsInterop.wasm");
WebAssembly.instantiate(wasmBuffer, {
    env: {
        hostDisplayString,
    }
}).then((w) => {
    wasmModule = w;
    wasmModule.instance.exports.juvixRender();
});

Running the Wasm module

Now you should have the files NodeJsInterop.wasm and NodeJsInterop.js in the same directory. Run the following command to execute the module:

node NodeJsInterop.js

You should see the following output:

Hello World from Juvix!

Comments

A comment is introduced in the same fashion as in Haskell=/=Agda.

  • Inline Comment
-- This is a comment!
  • Region comment
{-
    This is a comment!

-}

Axiom

Axioms or postulates can be introduced by using the axiom keyword. For example, let us imagine one wants to write a program that assumes A is a type, and there exists a term x that inhabits A. Then the program would look like the following.

-- Example.juvix
module Example;
 axiom A : Type;
 axom x : A;
end;

Terms introduced by the axiom keyword lack any computational content. However, it is possible to attach computational content to an axiom by giving compilation rules, see the compile keyword.

Compile blocks

The compile keyword has two arguments:

  • A name of an expression to be compiled.
  • A set of compilation rules using the format (backend → string) where the string is the text we inline.

This is an example:

$ cat tests/positive/HelloWorld
...
axiom Action : Type;
compile Action {
 ghc ↦ "IO ()";
};
...

The following Juvix examples are NOT valid.

  • One can not repeat backend inside a compile block.
...
axiom Action : Type;
compile Action {
 ghc ↦ "IO ()";
 ghc ↦ "IO ()";  --
};
...
  • One name, one compile block, no more.
...
axiom Action : Type;
compile Action {
 ghc ↦ "IO ()";
};
compile Action {
 ghc ↦ "IO ()";
};
...
  • A compile block must be in the same module as their name definition.
$ cat A.mjuvix
...
axiom Action : Type;
...

$ cat B.mjuvix
...
compile Action {
 ghc ↦ "IO ()";
};
...

Module system

Defining a module

A module is of the following form. The module keyword stars the declaration of a module followed by its name and its body. The module declaration ends after seeing the end keyword.

-- ModuleName.juvix
module ModuleName;

end;

A Juvix project is a collection of Juvix modules inside one main project folder containing a metadata file named juvix.yaml. Each Juvix file has to define a module of the same name. The name of the module must coincide with the path of the its file respect to its project. For example, if the file is root/Data/List.juvix then the module must be called Data.List, assumming root is the project's folder.

To check that Juvix is correctly detecting your project's root, one can run the command juvix internal root File.juvix.

Importing modules

To bring into the current scope all module definitions from other external modules, one can use the import keyword along with the corresponding module name. This way, one gets all the imported names qualified.

-- A.juvix
module A;
   axiom Nat : Type;
   axiom zero : Nat;
end;

-- B.juvix
module B;
    import A;
    x : A.Nat;
    x := A.zero;

Additionally, one can open an imported module making available all its names by their unqualified name.

-- A.juvix
module A;
   axiom Nat : Type;
   axiom zero : Nat;
end;

-- B.juvix
module B;
    import A;
    open A;
    x : Nat;
    x := zero;

However, opening modules may create name collisions if you already have the imported names as definitions in the current module. In this case, Juvix will complain with an error, letting you know which symbols are ambiguous. For example, in module B below, the name a is ambiguous.

-- A.juvix
module A;
axiom A : Type;
axiom a : A;
end;

-- B.juvix
module B;
import A;
open A;
axiom a : A;

x := a;
end;

One alternative here is hiding the name a as follows.

-- B.juvix
module B;
import A;
open A hiding {a};

axiom a : A;
x := a;

end;

Now, we can use the open import syntax to simplify the import-open statements.

Instead of having:

import Prelude;
open Prelude;

We simplify it by the expression:

open import Prelude;

The hiding keyword can be used within an open-import statement.

-- B.juvix
module A;
open import A hiding {a};
axiom a : A;
x := a;
end;

Exporting symbols

The module C below does not typecheck. Both symbols, originally defined in module A, are not visible in module C after importing B. The symbols A and a are not exported by the module B. To export symbols from an imported module, one can use the public keyword at the end of the corresponing open statement. For example, in module B, after marking the import of A as public, the module C typechecks.

-- A.juvix
module A;
axiom A : Type;
axiom a : A;
end;

-- B.juvix
module B;
open import A;
end;

-- C.juvix
module C;
open import B;

x : A;
x := a;
end;

Fix:

-- B.juvix
module B;
open import A public;
end;

Inductive data types

The inductive keyword is reserved for declaring inductive data types. An inductive type declaration requires a unique name for its type and its constructors, functions for building its terms. Constructors can be used as normal identifiers and also in patterns. As shown later, one can also provide type parameters to widen the family of inductive types one can define in Juvix.

The simplest inductive type is the Empty type with no constructors.

inductive Empty {};

In the following example, we declare the inductive type Nat, the unary representation of natural numbers. This type comes with two data constructors, namely zero and suc. A term of the type Nat is the number one, represented by suc zero or the number two represented by suc (suc zero), etc.

inductive Nat {
    zero : Nat;
    suc : Nat → Nat;
};

The way to use inductive types is by declaring functions by pattern matching. Let us define, for example, the function for adding two natural numbers.

inifl 6 +;
+ : Nat → Nat → Nat;
+ zero b ≔ b;
+ (suc a) b ≔ suc (a + b);

As mentioned earlier, an inductive type may have type parameters. The canonical example is the polymorphic type List. The type List is the inductive type that considers the type of the elements in the list as a parameter. A constructor to build the empty list, that is the base case, and another constructor to enlarge the list, we usually called it cons. One possible definition for this type is the following type taken from the Juvix standard library:

infixr 5 ∷;
inductive List (A : Type) {
  nil : List A;
  ∷ : A → List A → List A;
};

elem : {A : Type} → (A → A → Bool) → A → List A → Bool;
elem _ _ nil ≔ false;
elem eq s (x ∷ xs) ≔ eq s x || elem eq s xs;

To see more examples of inductive types and how to use them, please check out the Juvix standard library

Function declaration

A function declaration is a type signature and a group of definitions called function clauses.

In the following example we define a function called multiplyByTwo. The first line multiplyByTwo : ℕ -> ℕ; is the type signature and the second line multiplyByTwo n := 2 * n; is a function clause.

open import Stdlib.Prelude;

multiplyByTwo : ℕ -> ℕ;
multiplyByTwo n := 2 * n;

A function may have more than one function clause. When a function is called, the first clause that matches the argument is used.

The following function has two clauses.

open import Stdlib.Prelude;

neg : Bool -> Bool;
neg true := false;
neg false := true;

When neg is called with true the first clause is used and the function returns false. Similarly, when neg is called with false the second clause is used and the function returns true.

Mutually recursive functions

Function declarations can depend on others recursively. In the following example we define a function that checks if a number is even by calling a function that checks if a number is odd.

open import Stdlib.Prelude;

odd : Nat → Bool;

even : Nat → Bool;

odd zero ≔ false;
odd (suc n) ≔ even n;

even zero ≔ true;
even (suc n) ≔ odd n;

Foreign blocks

The foreign blocks give the developer the ability to introduce any piece of code in the compiled file. In addition, every foreign block specifies the backend's name that will include the given code in the body of the foreign block.

The following is an example taken from the Juvix standard library.

module Integers;

axiom Int : Type;
compile Int {  c ↦ "int" };

foreign c {
   bool lessThan(int l, int r) {
     return l < r;
   \}
};

inductive Bool {
    true : Bool;
    false : Bool;
};

infix 4 <';
axiom <' : Int → Int → Bool;
compile <' {
  c ↦ "lessThan";
};

infix 4 <;
< : Int → Int → Bool;
< a b ≔ from-backend-bool (a <' b);

Termination

To not bring inconsistencies by function declarations, Juvix requires that every function passes its termination checker. However, since this is a strong requirement, often tricky to fulfill, we give the user the possibility to skip this check in two different ways:

  • Using the terminating keyword to annotate function type signatures as terminating. The syntax is the following.
terminating fun : A → B;

Note that annotating a function as terminating means that all its function clauses pass the termination checker's criterion. To skip the termination checker for mutual recursive functions, all the functions involved must be annotated as terminating.

  • Using the CLI global flag --no-termination.
juvix typecheck --no-termination MyProgram.juvix

In any case, be aware that our termination checker is limited as it only accepts a subset of recursion functions. The termination checker algorithm is a slightly modification of the algorithm for checking termination in the Foetus's language.

CLI

Usage

juvix [Global options]  ((-v|--version) | --show-root | COMMAND)

Informative options

  • -v,--version Print the version and exit
  • --show-root Print the detected root of the project
  • -h,--help Show this help text

Global Command flags

  • --no-colors Disable globally ANSI formatting
  • --show-name-ids Show the unique number of each identifier when pretty printing
  • --only-errors Only print errors in a uniform format (used by juvix-mode)

Main Commands

  • html Generate HTML output from a Juvix file

  • typecheck Typecheck a Juvix file

  • compile Compile a Juvix file

Internal Commands

juvix internal COMMAND
  • parse Parse a Juvix file
  • scope Parse and scope a Juvix file
  • termination Subcommands related to termination checking
  • monojuvix Translate a Juvix file to MonoJuvix
  • microjuvix Subcommands related to MicroJuvix
  • minihaskell Translate a Juvix file to MiniHaskell
  • minic Translate a Juvix file to MiniC

CLI Auto-completion Scripts

The Juvix CLI can generate auto-completion scripts. Follow the instructions below for your shell.

NB: You may need to restart your shell after installing the completion script.

Bash

Add the following line to your bash init script (for example ~/.bashrc).

eval "$(juvix --bash-completion-script juvix)"

Fish

Run the following command in your shell:

juvix --fish-completion-script juvix
  > ~/.config/fish/completions/juvix.fish

ZSH

Run the following command in your shell:

juvix --zsh-completion-script juvix > $DIR_IN_FPATH/_juvix

where $DIR_IN_FPATH is a directory that is present on the ZSH FPATH variable (which you can inspect by running echo $FPATH in the shell).

Juvix Doctor

The juvix doctor command can help you to troubleshoot problems with your development environment. For each problem the doctor finds they'll be a link to a section on this page to help you fix it.

Could not find the clang command

The Juvix compiler uses the Clang compiler version 13 or later to generate binaries. You need to have Clang available on your system $PATH.

Recommended installation method:

MacOS

Use Homebrew:

brew install llvm

NB: The distribution of Clang that comes with XCode does not support the Wasm target so you must install the standard Clang distribution.

Debian / Ubuntu Linux

sudo apt install clang lldb lld

Arch Linux

sudo pacman -S llvm lld

Could not find the wasm-ld command

The Juvix compiler required wasm-ld (the Wasm linker) to produce Wasm binaries.

Recommened installation method:

MacOS

wasm-ld is included in the Homebrew llvm distribution:

brew install llvm

Debian / Ubuntu Linux

sudo apt install lldb lld

Arch Linux

sudo pacman -S lld

Newer Clang version required

Juvix requires Clang version 13 or above. See the documentation on installing Clang.

Clang does not support the wasm32 target

Juvix requires Clang version 13 or above. See the documentation on installing Clang.

Clang does not support the wasm32-wasi target

Juvix uses WASI - The Wasm System Interface to produce binaries that can be executed using a Wasm runtime. The files necessary to setup Clang with wasm32-wasi support are available at wasi-sdk.

To install the wasm32-wasi target for Clang you need to do two things:

Install libclang_rt.builtins-wasm32.a into your Clang distribution

  1. Obtain libclang_rt.builtins-wasm32-wasi-16.0.tar.gz from the wasi-sdk releases page.

  2. Untar the file and place the file lib/wasi/libclang_rt.builtins-wasm32.a into your Clang distribution directory.

    On MacOS, if you installed llvm using homebrew you can find the Clang distribution directory using brew --prefix llvm. You should then place the builtins file at `brew --prefix llvm`/lib/wasi/libclang_rt.builtins-wasm32.a.

    On Linux the Clang distribution directory will be something like /usr/lib/clang/13.0.1 where 13.0.1 is the version of Clang that you have installed. You should then place the builtins file at /usr/lib/clang/13.0.1/lib/wasi/libclang_rt.builtins-wasm32.

Download the WASI sysroot and set WASI_SYSROOT_PATH

  1. Obtain wasi-sysroot-16.0.tar.gz from the wasi-sdk releases page.
  2. Untar the file and set the environment variable WASI_SYSROOT_PATH to that location.

Environment variable WASI_SYSROOT_PATH is not set

Set the WASI_SYSROOT_PATH to the directory where you installed the wasi-sdk sysroot files. See installing the WASI sysroot.

Could not find the wasmer command

The Juvix test suite uses Wasmer as a Wasm runtime to execute compiled Wasm binaries. See the Wasmer documentation to see how to install it.

Emacs Mode

There is an Emacs mode available for Juvix. Currently, it supports syntax highlighting for well-scoped modules.

To install it add the following lines to your Emacs configuration file:

(push "/path/to/juvix/juvix-mode/" load-path)
(require 'juvix-mode)

Make sure that Juvix is installed in your PATH.

The Juvix major mode will be activated automatically for .juvix files.

Keybindings

Key Function Name Description
C-c C-l juvix-load Runs the scoper and adds semantic syntax highlighting

Testing

Dependencies

See Installing dependencies for instructions on how to setup the testing environment for the WASM compiler tests.

Running

Run tests using:

stack test

To run tests, ignoring all the WASM tests:

stack test --ta '-p "! /slow tests/"'

Validity predicates

Monomorphization

Monomorphization refers to the process of converting polymorphic code to monomorphic code (no type variables) through static analysis.

Example:

id : (A : Type) → A → A;
id _ a ≔ a;

b : Bool;
b ≔ id Bool true;

n : Nat;
n ≔ id Nat zero;

Is translated into:

id_Bool : Bool → Bool;
id_Bool a ≔ a;

id_Nat : Nat → Nat;
id_Nat a ≔ a;

More examples

Mutual recursion

inductive List (A : Type) {
  nil : List A;
  cons : A → List A → List A;
};

even : (A : Type) → List A → Bool;
even A nil ≔ true ;
even A (cons _ xs) ≔ not (odd A xs) ;

odd : (A : Type) → List A → Bool;
odd A nil ≔ false ;
odd A (cons _ xs) ≔ not (even A xs) ;

-- main ≔ even Bool ..  odd Nat;

Collection algorithm

This section describes the algorithm to collect the list of all concrete functions and inductive definitions that need to be generated.

Assumptions:

  1. Type abstractions only appear at the leftmost part of a type signature.
  2. All functions and constructors are fully type-applied: i.e. currying for types is not supported.
  3. There is at least one function with a concrete type signature.
  4. All axioms are monomorphic.
  5. No module parameters.

Definitions

  1. Application. An application is an expression of the form t₁ t₂ … tₙ with n > 0.

  2. Sub application. If t₁ t₂ … tₙ is an application then for every 0<i<n t₁ t₂ … tᵢ is a sub application.

Fix a juvix program P. Let 𝒲 be the set of all applications that appear in P.

  1. Maximal application. A maximal application is an application A∈𝒲 such that for every A'∈𝒲 we have that A is not a sub application of A'.

  2. Type application. If

    1. t a₁ a₂ … aₙ is a maximal application; and
    2. t is either a function or an inductive type; and
    3. a₁, …, aₘ are types; and
    4. aₘ₊₁ is not a type or m = n.

    Then t a₁, …, aₘ is a type application.

  3. Concrete type. A type is concrete if it involves no type variables.

  4. Concrete type application. A type application t a₁ a₂ … aₙ if a₁, a₂, …, aₙ are concrete types.

Option 1

Let S₀ be the set of functions with a concrete type signature. Gather all type applications (both in the type and in the body) in each of the functions in S₀. Clearly the collected type applications are all concrete. We now have a stack c₁, c₂, …, cₙ of concrete type applications.

  1. If the stack is empty, we are done.
  2. Otherwise pop c₁ from the stack. It will be of the form t a₁ … aₘ, where t is either an inductive or a function and a₁, …, aₘ are concrete types.
  3. If the instantiation t a₁ … aₘ has already been registered go to step 1. Otherwise continue to the next step.
  4. Register the instantiation t a₁ … aₘ.
  5. If t is a function, then it has type variables v₁, …, vₘ. Consider the substitution σ = {v₁ ↦ a₁, …, vₘ ↦ aₘ}. Consider the list of type applications in the body of t: d₁, …, dᵣ. Add σ(d₁), …, σ(dᵣ) to the stack and continue to step 1. It is easy to see that for any i, σ(dᵢ) is a concrete type application.
  6. If t is an inductive type, let d₁, …, dᵣ be the type applications that appear in the type of its constructors, then proceed as before.

Correctness

It should be clear that the algorithm terminates and registers all instantiations of constructors and functions.

Generation algorithm

The input of this algorithm is the list of concrete type applications, name it ℒ, produced by the collection algorithm. Example:

List String
Pair Int Bool
Maybe String
Maybe Int
if (Maybe String)
if (Maybe Int)
if (Pair Int Bool)

Name generation

Let f â be an arbitrary element of ℒ, where â is a list of concrete types.

  • If f is a function, assign a fresh name to f â, call it ⋆(f â).
  • If f is an inductive type, assign a fresh name to f â, call it ⋆(f â). Then, for each constructor cᵢ of f, where i is the index of the constructor, assign a fresh name to it and call it ⋆ᵢ(f â).

Function generation

Consider an arbitrary function f in the original program. Then consider the list of concrete type applications involving f: f â₁, …, f âₙ.

  • If n = 0, then either:
    1. f has a concrete type signature, in that case we proceed as expected.
    2. f is never called from the functions with a concrete type. In this case we can safely ignore it.
  • If n > 1. For each âᵢ we proceed as follows in the next sections. Fix m to be the lenght of âᵢ with m > 0.

Function name

The name of the monomorphized function is ⋆(f âᵢ).

Type signature

Let 𝒮 be the type signature of f. Then 𝒮 has to be of the form (A₁ : Type) → … → (Aₘ : Type) → Π, where Π is a type with no type abstractions. Now consider the substitution σ = {A₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]}. Since âᵢ is a list of concrete types, it is clear that σ(Π) is a concrete type. Then proceed as described in Types.

Function clause

Let 𝒞 be a function clause of f. Let p₁ … pₖ with k ≥ m be the list of patterns in 𝒞. Clearly the first m patterns must be either variables or wildcards. Wlog assume that the first m patterns are all variables, namely v₁, …, vₘ. Let σ = {v₁ ↦ âᵢ[1], …, Aₘ ↦ âᵢ[m]} be a substitution. Let e be the body of 𝒞, then clearly σ(e) has no type variables in it. Now, since each name id must be bound at most once, we need to generate new ones for the local variables bound in the patterns pₘ₊₁, …, pₖ. Let w₁, …, wₛ be the variables bound in pₘ₊₁, …, pₖ. Let w'₁, …, w'ₛ be fresh variables. Then let δ = {w₁ ↦ w'₁, …, wₛ ↦ w'ₛ}.

Now let 𝒞' have patterns δ(pₘ₊₁), …, δ(pₖ) and let e' ≔ (σ ∪ δ)(e). It should be clear that e' has no type variables in it and that all local variable references in e' are among w'₁, …, w'ₛ. Note that e' is not yet monomorphized. Proceed to the next step to achieve that.

Expressions

The input is an expression e that has no type variables in it. The goal is to replace the concrete type applications by the corresponding monomorphized expression.

The only interesting case is when we find an application. Consider the unfolded view of the application: f a₁ … aₘ. Then, if f is either a constructor, or a function, let A₁, …, Aₖ with k ≤ m be the list of type parameters of f.

  • If f is a function and f a₁ … aₖ ∉ ℒ then recurse normally, otherwise, let â ≔ a₁ … aₖ and replace the original expression f a₁ … aₘ, by ⋆(f â) aₖ₊₁' … aₘ' where aₖ₊₁' … aₘ' are the monomorphization of aₖ₊₁ … aₘ respectively.
  • If f is a constructor, let d be its inductive type. Then check d a₁ … aₖ ∈ ℒ. Proceed analogously as before.

Types

The input is a type t that has no type variables in it. The goal is to replace the concrete type applications by the corresponding monomorphized type. Proceed analogously to the previous section.

Strictly positive data types

We follow a syntactic description of strictly positive inductive data types.

An inductive type is said to be strictly positive if it does not occur or occurs strictly positively in the types of the arguments of its constructors. A name qualified as strictly positive for an inductive type if it never occurs at a negative position in the types of the arguments of its constructors. We refer to a negative position as those occurrences on the left of an arrow in a type constructor argument.

In the example below, the type X occurs strictly positive in c0 and negatively at the constructor c1. Therefore, X is not strictly positive.

axiom B : Type;
inductive X {
  c0 : (B -> X) -> X;
  c1 : (X -> X) -> X;
};

We could also refer to positive parameters as such parameters occurring in no negative positions. For example, the type B in the c0 constructor above is on the left of the arrow B->X. Then, B is at a negative position. Negative parameters need to be considered when checking strictly positive data types as they may allow to define non-strictly positive data types.

In the example below, the type T0 is strictly positive. However, the type T1 is not. Only after unfolding the type application T0 (T1 A) in the data constructor c1, we can find out that T1 occurs at a negative position because of T0. More precisely, the type parameter A of T0 is negative.

inductive T0 (A : Type) {
  c0 : (A -> T0 A) -> T0 A;
};

inductive T1 {
  c1 : T0 T1 -> T1;
};

Bypass the strict positivity condition

To bypass the positivity check, a data type declaration can be annotated with the keyword positive. Another way is to use the CLI global flag --no-positivity when typechecking a Juvix File.

$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
module E5;
  positive
  inductive T0 (A : Type){
    c0 : (T0 A -> A) -> T0 A;
  };
end;

Examples of non-strictly data types

  • NSPos is at a negative position in c.

    inductive Empty {};
inductive NSPos {
  c : ((NSPos -> Empty) -> NSPos) -> NSPos;
};

  • Bad is not strictly positive beceause of the negative parameter A of Tree.

    inductive Tree (A : Type) {
  leaf : Tree A;
  node : (A -> Tree A) -> Tree A;
};

inductive Bad {
  bad : Tree Bad -> Bad;
};

  • A is a negative parameter.

    inductive B (A : Type) {
  b : (A -> B (B A -> A)) -> B A;
};

Juvix

CI status

pages-build-deployment

LICENSE Juvix Mascot

Description

Juvix is a research programming language created by Heliax as a first step toward creating more robust and reliable alternatives for formally verified smart contracts than existing languages. The Juvix language is constantly evolving, open-source, functional, and statically typed with special support for compiling validity predicates to the C language, which can be deployed to various distributed ledgers including Anoma.

The Juvix language and related tools are documented in the Juvix book. To write and test Juvix programs, you can use your favorite text editor and the juvix command line tool. However, we recommend using the juvix-mode in Emacs or the plugin in VSCode.

First examples of programs written in Juvix

The following links are clickable versions of their corresponding Juvix programs. The HTML output is generated by running juvix html --recursive FileName.juvix.

The Juvix standard library contains common functions that can be used in Juvix programs.

Quick Start

Installing Juvix on MacOS

The easiest way to install Juvix on MacOS is by using Homebrew.

To install the homebrew-juvix tap, run:

brew tap anoma/juvix

To install Juvix, run:

brew install juvix

After installing Juvix, you might want to try our doctor to check your system setup:

juvix doctor

Helpful information on the shell can also be obtained by running:

brew info juvix

Building Juvix from the sources

To install Juvix from the sources, you must download the Github repository. Then, the program can be installed with the following commands. We assume have Stack installed.

git clone --recursive https://github.com/anoma/juvix.git
cd juvix
stack install

If the installation succeeds, you must be able to run the Juvix command from any location. To get the complete list of commands, please run juvix --help.

On MacOS, you can alternatively run the following command for Homebrew. The flag --HEAD used below is optional, mostly to build the latest version of Juvix in the main branch on Github.

brew install --build-from-source --HEAD juvix --verbose

The Hello World Example

In the following example a Juvix file is compiled to Wasm. Please check out the documentation Installing dependencies for instructions on how to setup your environment for compiling Juvix. You can also run juvix doctor to check your system setup.

-- HelloWorld.juvix
module HelloWorld;

open import Stdlib.Prelude;

main : IO;
main ≔ putStrLn "hello world!";

end;

Then, run the following commands at the location folder of the file HelloWorld.juvix:

juvix compile HelloWorld.juvix
wasmer HelloWorld.wasm

You should see the output: hello world!

The Juvix programming language

Juvix allows us to write programs with a high degree of assurance. The Juvix compiler runs several static analyses during the compilation phase to guarantee no runtime errors. Analyses permormed during this phase include scope, termination, arity, and type checkiqng. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors.

Some of the language features in Juvix include:

  • unicode syntax
  • parametric polymorphism
  • inductive and parametric data types
  • higher-order functions
  • implicit arguments
  • holes in expressions
  • axioms for non-computable terms

Additionally, the foreign and compile blocks syntax enable developers to compile a program to different backends including the C language. The Juvix module system further permits splitting programs into several modules to build libraries which can be later documented by generating HTML files based on the codebase, see for example, the Juvix standard library's website. For futher details, please refer to the Juvix book which includes our latest updates.

Coming soon

For the language:

  • lambda expressions
  • let expressions
  • tail call optimization
  • inference for mutually recursive functions
  • compilation to circuits
  • coverage checking (i.e. exhaustiveness and useless clauses)

For the compiler:

  • Init command
  • Better documentation tool: juvix doc MyFile.juvix

Community

We would love to hear what you think of Juvix! Join us on the Anoma Discord.

Juvix community

We would love to hear what you think of Juvix! Join us on Discord

This project is part of a bigger effort called Anoma. Anoma is a suite of protocols and mechanisms for self-contained, self-sovereign coordination. Join the Anoma project.