Juvix
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
.
- HelloWorld.juvix
- Fibonacci.juvix
- Hanoi.juvix
- PascalsTriangle.juvix
- Collatz.juvix
- TicTacToe.juvix
- SimpleFungibleToken.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
v0.2.3 (2022-08-15)
Implemented enhancements:
- add
name
andversion
tojuvix.yaml
#1422 (janmasrovira)
Fixed bugs:
- Properly handle paragraphs in judoc #1447 (janmasrovira)
Merged pull requests:
- Give a proper type to literal natural numbers #1453 (janmasrovira)
- Add the option to output json in the
juvix internal highlight
command #1450 (janmasrovira) for supporting the new Juvix Mode for Visual Studio Code (jonaprieto) - Allow _ in Wasm exported names to support Anoma signature #1449 (paulcadman)
- Add Towers of Hanoi and Pascal triangle examples #1446 (paulcadman)
- Add
juvix init
command #1445 (janmasrovira) - Refactor pretty to reduce duplication #1443 (janmasrovira)
- Add initial support for examples in Html documentation #1442 (janmasrovira)
- Add revisions to README #1440 (jonaprieto)
- CI: Run build on push to main #1437 (paulcadman)
- Add doctor subcommand #1436 (paulcadman)
- CI checkout repo before cache and use recommended cache strategy #1435 (paulcadman)
- Various documentation adjustments #1434 (paulcadman)
- Setup Clang before building docs in CI #1433 (paulcadman)
- Major revisions to Makefile #1431 (jonaprieto)
- Do not add
-src
suffix to links in HTML when runningjuvix html
#1429 (paulcadman) - Add a Web version of TicTacToe #1427 (paulcadman)
- WASM import all non-compile axioms with alphanum names in entrypoint #1426 (paulcadman)
- Export all functions with alpha numeric names from entrypoint module #1425 (paulcadman)
- Refactor #1420 (jonaprieto)
- Permit axiom without a compile block #1418 (paulcadman)
- Implement an html documentation generator similar to haddock (#1413) #1416 (janmasrovira)
- Fix version shell test for 0.2.2 #1415 (paulcadman)
- Remove Int from stdlib and update SimpleFungibleToken example #1414 (paulcadman)
v0.2.2 (2022-07-25)
Implemented enhancements:
- Compute name dependency graph and filter unreachable definitions #1408 (lukaszcz)
- Support type aliases #1404 (janmasrovira)
- Add debugging custom function to Prelude #1401 (jonaprieto)
- Add positivity check for data types #1393 (jonaprieto)
- Keep qualified names #1392 (janmasrovira)
- Direct translation from MicroJuvix to MiniC #1386 (lukaszcz)
- Widens the accepted symbol list #1385 (mariari)
- Check all the type parameter names are different when declaring an inductive type #1377 (jonaprieto)
Fixed bugs:
- Curly braces are allowed nested in patterns #1380 (janmasrovira)
Merged pull requests:
- Add
Fail
effect (#1409) #1411 (janmasrovira) - Refactor of typechecking and other checking processes #1410 (jonaprieto)
- Use bold for code in scoper error messages #1403 (janmasrovira)
- Replace ppSimple by text #1402 (jonaprieto)
- Implement some error messages (#1396) #1400 (lukaszcz)
- Refactor childs of pattern parentheses and braces #1398 (janmasrovira)
- Update Juvix standard-library #1389 (jonaprieto)
- Fix documentation generation #1387 (jonaprieto)
- Adds Collatz sequence generator example #1384 (paulcadman)
- html-examples #1381 (jonaprieto)
- Refine hole in type signature to function type #1379 (janmasrovira)
- Type checking fails when the type of a pattern is not given by the signature #1378 (janmasrovira)
- Set cname for gh-pages action #1376 (paulcadman)
- Add fibonacci sequence example program #1375 (paulcadman)
- Fix Changelog links and minors #1371 (jonaprieto)
- Add Version number to the emacs mode #1320 (mariari)
v0.2.1 (2022-07-12)
Implemented enhancements:
- Specialize commands of/for internal use #270 (jonaprieto)
- Improve handling of location information for different objs #263 (jonaprieto)
- Add issues and PR templates #261 (jonaprieto)
- Throw error when reading a file that conflicts with embedded stdlib #243 (paulcadman)
- Embed standard library in the minijuvix binary #210 (paulcadman)
Fixed bugs:
- Fixed a bug with the path to walloc.c #237 (lukaszcz)
- Perform ScopedToAbstract exactly once for each module #223 (paulcadman)
Merged pull requests:
- Label renaming #275 (jonaprieto)
- Update link to discord #264 (Romainua)
- Include
open import
statements when generating HTML #260 (paulcadman) - Renaming MiniJuvix to Juvix #259 (jonaprieto)
- Updates tests to use the updated standard library #253 (paulcadman)
- Enforce C99 standard in the generated C files #252 (lukaszcz)
- Restore mascot images to the minijuvix book #250 (paulcadman)
- Allow jumping to another module in emacs #249 (janmasrovira)
- Restore Juvix mascot image to README #248 (paulcadman)
- Add emacs option
minijuvix-disable-embedded-stdlib
#247 (paulcadman) - Deprecate GHC backend #244 (lukaszcz)
- Removed 'eval' and 'print' keywords (#214) #242 (lukaszcz)
- Add option to disable minijuvix input method #239 (janmasrovira)
- Remove the 'match' keyword #238 (lukaszcz)
- Removed tests/positive/HelloWorld.mjuvix and specified clang version in the documentation #236 (lukaszcz)
- Filter symbol entries properly in the scoper #234 (janmasrovira)
- Use the ModulesCache for
open
statements in ScopedToAbstract pass #224 (paulcadman) - README: Include
--recursive
in git clone command to fetch stdlib #211 (paulcadman) - Update project description v0.2.0 #209 (jonaprieto)
- Unify AST representation of types and expressions in MicroJuvix #188 (janmasrovira)
v0.2.0
(2022-06-28)
Implemented enhancements:
- Support built in types #192 (janmasrovira)
- Support partial application and closure passing in C backend #190 (paulcadman)
- Allow
open import
statements #175 (janmasrovira) - Remove TypeAny and adapt typechecking for literals #173 (janmasrovira)
- Allow holes to be refined into function types #165 (janmasrovira)
- Support implicit arguments #144 (janmasrovira)
- Add support for holes in type signatures #141 (janmasrovira)
- Support function closures with no environment in minic #137 (paulcadman)
- Add holes for expressions in function clauses and inference support #136 (janmasrovira)
- Add "-Oz" optimization flag to clang args #133 (paulcadman)
- Add version and help option and root command to the CLI #131 (jonaprieto)
Fixed bugs:
- Fix: Ignore implicit patterns and arguments in termination checking #172 (janmasrovira)
- Fix: pretty printing for terminating keyword #145 (jonaprieto)
Merged pull requests:
- Fix: proper error handling for typechecker errors #189 (jonaprieto)
- Add juvix version info and date to HTML output #186 (jonaprieto)
- Fix: Add check for constructor return types #182 (jonaprieto)
- Use Abstract name in Abstract syntax and Micro/MonoJuvix #181 (janmasrovira)
- Add an option to specify the path where to put the HTML output #179 (jonaprieto)
- Upgrade to ghc-9.2.3 #178 (janmasrovira)
- Replace dead link in README with a link to the Juvix book #177 (paulcadman)
- Embed HTML assets in the juvix binary #176 (paulcadman)
- Fix: identifiers with a keyword prefix cannot be parsed #171 (janmasrovira)
- Improve filepath equality #170 (janmasrovira)
- Update validity predicate milestone example to 0.2 syntax #167 (paulcadman)
- Fix links in documentation and update to new syntax #163 (paulcadman)
- Update stdlib to work with version 0.2 #160 (janmasrovira)
- Update README usage example to use the compile command #158 (paulcadman)
- Remove dead code related to the pipeline #156 (janmasrovira)
- Add negative test for AppLeftImplicit #154 (janmasrovira)
- Add positive test designed for implicit arguments #153 (janmasrovira)
- Remove ExpressionTyped from MicroJuvix #143 (janmasrovira)
- Revision for package.yaml and minor deletions #135 (jonaprieto)
v0.1.4
(2022-05-30)
Merged pull requests:
- Generic Errors and refactoring #123 (jonaprieto)
- Only generates docs if the pull request merges #121 (jonaprieto)
- Add initial docs generation website #119 (jonaprieto)
- Fix internal link in README #116 (paulcadman)
- Add minic-runtime for linking without libc #113 (paulcadman)
- Add termination checking to the pipeline #111 (jonaprieto)
- Support uncurried higher order functions #110 (paulcadman)
- Improve error generation and handling #108 (janmasrovira)
- Add MiniC tests with clang+wasi-sdk #105 (paulcadman)
- Add usage example and move developer docs #96 (paulcadman)
- Refactor warning related stuff #91 (janmasrovira)
- Remove Agda backend #86 (paulcadman)
Implemented enhancements:
- Add
compile
subcommand to generate binaries #128 - Add intervals to flycheck errors #124
- Improve error handling in juvix-mode #107
- Support multiple modules in compilation #93
- Add compile command to CLI #130 (paulcadman)
- Use Interval in GenericErrors #125 (janmasrovira)
- Remove dev in the CI and other tweaks #118 (jonaprieto)
- Highlight comments correctly #106 (janmasrovira)
- Support multiple modules in compilation #100 (janmasrovira)
- New target syntax and modular VP examples #92 (jonaprieto)
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)
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
fromstack.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:
- Remove agda backend #86 (paulcadman)
- 84 monomorphisation naming inconsistency #85 (janmasrovira)
- Change terminating keyword behavior #82 (jonaprieto)
- Remove unused constructor ExpressionTyped in Monojuvix #80 (janmasrovira)
- Stricter stack builds and pedantic mode for CI #78 (jonaprieto)
- Bump stackage version and remove allow-newer #76 (janmasrovira)
- Add automatically updates/issues/merged PRs to the changelog #74 (jonaprieto)
- Add terminating keyword #71 (jonaprieto)
- Monomorphization #70 (janmasrovira)
- Remove StatementCompile in AST after scoping #69 (paulcadman)
- Add C code generation backend #68 (paulcadman)
- Check if stderr supports ANSI and print accordingly #67 (janmasrovira)
- Add support for compile (by Jonathan) #66 (paulcadman)
- Add NameIdGen effect to the pipeline #64 (janmasrovira)
- Make the
--show-name-ids
flag global #63 (janmasrovira) - Implement type checker with polymorphism #62 (janmasrovira)
v0.1.2
(2022-04-11)
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:
- The Juvix project now follows the same goals as the original Juvix project. #7 (jonaprieto)
- Dev→main #6 (jonaprieto)
- Big update including termination checking #5 (janmasrovira)
- Parser and scoper #3 (jonaprieto)
- Upgrade to ghc9 and use hpack #2 (janmasrovira)
- Merge #1 (jonaprieto)
v0.1.1
(2022-03-25)
- 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:
Quick Start
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 ofllvm
).
To install wasi-sdk
you need to download libclang_rt
and
wasi-sysroot
precompiled archives from the wasi-sdk release
page and:
-
Extract the
libclang_rt.builtins-wasm32-wasi-*.tar.gz
archive in theclang
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
-
Extract the
wasi-sysroot-*.tar.gz
archive on your local system and setWASI_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
.
- HelloWorld.juvix
- Fibonacci.juvix
- Hanoi.juvix
- PascalsTriangle.juvix
- Collatz.juvix
- TicTacToe.juvix
- SimpleFungibleToken.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
- Axiom
- Function
- Module System
- Inductive data type
- Termination checking
- Compile block
- Foreign block
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 filescope
Parse and scope a Juvix filetermination
Subcommands related to termination checkingmonojuvix
Translate a Juvix file to MonoJuvixmicrojuvix
Subcommands related to MicroJuvixminihaskell
Translate a Juvix file to MiniHaskellminic
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
-
Obtain
libclang_rt.builtins-wasm32-wasi-16.0.tar.gz
from the wasi-sdk releases page. -
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
where13.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
- Obtain
wasi-sysroot-16.0.tar.gz
from the wasi-sdk releases page. - 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:
- Type abstractions only appear at the leftmost part of a type signature.
- All functions and constructors are fully type-applied: i.e. currying for types is not supported.
- There is at least one function with a concrete type signature.
- All axioms are monomorphic.
- No module parameters.
Definitions
-
Application. An application is an expression of the form
t₁ t₂ … tₙ
with n > 0. -
Sub application. If
t₁ t₂ … tₙ
is an application then for every0<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
.
-
Maximal application. A maximal application is an application
A∈𝒲
such that for everyA'∈𝒲
we have thatA
is not a sub application ofA'
. -
Type application. If
t a₁ a₂ … aₙ
is a maximal application; andt
is either a function or an inductive type; anda₁, …, aₘ
are types; andaₘ₊₁
is not a type orm = n
.
Then
t a₁, …, aₘ
is a type application. -
Concrete type. A type is concrete if it involves no type variables.
-
Concrete type application. A type application
t a₁ a₂ … aₙ
ifa₁, 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.
- If the stack is empty, we are done.
- Otherwise pop
c₁
from the stack. It will be of the formt a₁ … aₘ
, wheret
is either an inductive or a function anda₁, …, aₘ
are concrete types. - If the instantiation
t a₁ … aₘ
has already been registered go to step 1. Otherwise continue to the next step. - Register the instantiation
t a₁ … aₘ
. - If
t
is a function, then it has type variablesv₁, …, vₘ
. Consider the substitutionσ = {v₁ ↦ a₁, …, vₘ ↦ aₘ}
. Consider the list of type applications in the body oft
:d₁, …, dᵣ
. Addσ(d₁), …, σ(dᵣ)
to the stack and continue to step 1. It is easy to see that for anyi
,σ(dᵢ)
is a concrete type application. - If
t
is an inductive type, letd₁, …, 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 tof â
, call it⋆(f â)
. - If
f
is an inductive type, assign a fresh name tof â
, call it⋆(f â)
. Then, for each constructorcᵢ
off
, wherei
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:f
has a concrete type signature, in that case we proceed as expected.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. Fixm
to be the lenght ofâᵢ
withm > 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 andf a₁ … aₖ ∉ ℒ
then recurse normally, otherwise, letâ ≔ a₁ … aₖ
and replace the original expressionf a₁ … aₘ
, by⋆(f â) aₖ₊₁' … aₘ'
whereaₖ₊₁' … aₘ'
are the monomorphization ofaₖ₊₁ … aₘ
respectively. - If
f
is a constructor, letd
be its inductive type. Then checkd 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 inc
.inductive Empty {}; inductive NSPos { c : ((NSPos -> Empty) -> NSPos) -> NSPos; };
-
Bad
is not strictly positive beceause of the negative parameterA
ofTree
.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
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
.
- HelloWorld.juvix
- Fibonacci.juvix
- Hanoi.juvix
- PascalsTriangle.juvix
- Collatz.juvix
- TicTacToe.juvix
- SimpleFungibleToken.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.