mirror of
https://github.com/anoma/juvix.git
synced 2024-11-24 08:45:51 +03:00
Remove docs related files (#2023)
This commit is contained in:
Jonathan Cubides
GitHub
parent
d59fca6786
commit
cf3855ab7a
101
.github/workflows/ci.yml
vendored
101
.github/workflows/ci.yml
vendored
@ -1,4 +1,4 @@
|
|||||||
name: The Juvix compiler CI
|
name: Juvix Compiler CI
|
||||||
"on":
|
"on":
|
||||||
workflow_dispatch:
|
workflow_dispatch:
|
||||||
inputs:
|
inputs:
|
||||||
@ -148,105 +148,6 @@ jobs:
|
|||||||
cd main
|
cd main
|
||||||
make smoke
|
make smoke
|
||||||
|
|
||||||
docs-linux:
|
|
||||||
needs: build-and-test-linux
|
|
||||||
runs-on: ubuntu-20.04
|
|
||||||
environment:
|
|
||||||
name: github-pages
|
|
||||||
url: ${{ steps.deployment.outputs.page_url }}
|
|
||||||
# Grant GITHUB_TOKEN the permissions required to make a Pages deployment
|
|
||||||
permissions:
|
|
||||||
pages: write # to deploy to Pages
|
|
||||||
id-token: write # to verify the deployment originates from an appropriate source
|
|
||||||
|
|
||||||
steps:
|
|
||||||
- name: Checkout our repository
|
|
||||||
uses: actions/checkout@v3
|
|
||||||
with:
|
|
||||||
path: main
|
|
||||||
submodules: recursive
|
|
||||||
|
|
||||||
- name: Install mdbook-pagetoc
|
|
||||||
uses: baptiste0928/cargo-install@v1
|
|
||||||
with:
|
|
||||||
crate: mdbook-pagetoc
|
|
||||||
|
|
||||||
- name: Install mdbook-katex
|
|
||||||
uses: baptiste0928/cargo-install@v1
|
|
||||||
with:
|
|
||||||
crate: mdbook-katex
|
|
||||||
|
|
||||||
- name: Install mdbook-linkcheck
|
|
||||||
uses: baptiste0928/cargo-install@v1
|
|
||||||
with:
|
|
||||||
crate: mdbook-linkcheck
|
|
||||||
|
|
||||||
- name: MDBook setup
|
|
||||||
uses: peaceiris/actions-mdbook@v1
|
|
||||||
with:
|
|
||||||
mdbook-version: "latest"
|
|
||||||
|
|
||||||
- name: Cache LLVM and Clang
|
|
||||||
id: cache-llvm
|
|
||||||
uses: actions/cache@v3
|
|
||||||
with:
|
|
||||||
path: |
|
|
||||||
C:/Program Files/LLVM
|
|
||||||
./llvm
|
|
||||||
key: "${{ runner.os }}-llvm-13"
|
|
||||||
|
|
||||||
- name: Install LLVM and Clang
|
|
||||||
uses: KyleMayes/install-llvm-action@v1
|
|
||||||
with:
|
|
||||||
version: "13.0"
|
|
||||||
cached: "${{ steps.cache-llvm.outputs.cache-hit }}"
|
|
||||||
|
|
||||||
- name: Make runtime
|
|
||||||
run: |
|
|
||||||
cd main
|
|
||||||
make runtime
|
|
||||||
|
|
||||||
- name: Stack setup
|
|
||||||
id: stack
|
|
||||||
uses: freckle/stack-action@v4
|
|
||||||
with:
|
|
||||||
working-directory: main
|
|
||||||
test: false
|
|
||||||
|
|
||||||
- name: Generate HTML files from examples
|
|
||||||
run: |
|
|
||||||
cd main
|
|
||||||
echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
|
|
||||||
make install
|
|
||||||
make html-examples
|
|
||||||
make demo-example
|
|
||||||
|
|
||||||
- name: Build the mdbook
|
|
||||||
run: |
|
|
||||||
cd main
|
|
||||||
make docs
|
|
||||||
|
|
||||||
- name: Setup Pages
|
|
||||||
uses: actions/configure-pages@v3
|
|
||||||
if: >-
|
|
||||||
github.ref == 'refs/heads/main' || github.event_name ==
|
|
||||||
'workflow_dispatch'
|
|
||||||
|
|
||||||
- name: Upload artifact
|
|
||||||
uses: actions/upload-pages-artifact@v1
|
|
||||||
if: >-
|
|
||||||
github.ref == 'refs/heads/main' || github.event_name ==
|
|
||||||
'workflow_dispatch'
|
|
||||||
with:
|
|
||||||
path: main/book/html
|
|
||||||
|
|
||||||
- name: Deploy to GitHub Pages
|
|
||||||
uses: actions/deploy-pages@v1
|
|
||||||
id: deployment
|
|
||||||
if: >-
|
|
||||||
github.ref == 'refs/heads/main' || github.event_name ==
|
|
||||||
'workflow_dispatch'
|
|
||||||
|
|
||||||
build-and-test-macos:
|
build-and-test-macos:
|
||||||
runs-on: macos-12
|
runs-on: macos-12
|
||||||
steps:
|
steps:
|
||||||
|
|||||||
26
Makefile
26
Makefile
@ -56,11 +56,7 @@ clean-juvix-build:
|
|||||||
repl:
|
repl:
|
||||||
@${STACK} ghci Juvix:lib ${STACKFLAGS}
|
@${STACK} ghci Juvix:lib ${STACKFLAGS}
|
||||||
|
|
||||||
# ------------------------------------------------------------------------------
|
# -- EXAMPLES HTML OUTPUT
|
||||||
# -- The Juvix Book
|
|
||||||
# ------------------------------------------------------------------------------
|
|
||||||
|
|
||||||
# -- EXAMPLES
|
|
||||||
|
|
||||||
.PHONY: html-examples
|
.PHONY: html-examples
|
||||||
html-examples: $(EXAMPLES)
|
html-examples: $(EXAMPLES)
|
||||||
@ -76,26 +72,6 @@ demo-example:
|
|||||||
@mkdir -p ${OUTPUTDIR}
|
@mkdir -p ${OUTPUTDIR}
|
||||||
@${JUVIXBIN} html $(DEMO_EXAMPLE) --output-dir=$(CURDIR)/${OUTPUTDIR}
|
@${JUVIXBIN} html $(DEMO_EXAMPLE) --output-dir=$(CURDIR)/${OUTPUTDIR}
|
||||||
|
|
||||||
# -- MDBook
|
|
||||||
|
|
||||||
.PHONY: docs
|
|
||||||
docs: html-examples
|
|
||||||
@cp $(METAFILES) docs/
|
|
||||||
@cp -r assets/ docs/
|
|
||||||
@mdbook build
|
|
||||||
|
|
||||||
.PHONY: serve-docs
|
|
||||||
serve-docs: docs
|
|
||||||
@mdbook serve --open
|
|
||||||
|
|
||||||
cargo-dependencies:
|
|
||||||
@cargo install mdbook \
|
|
||||||
mdbook-katex \
|
|
||||||
mdbook-linkcheck \
|
|
||||||
mdbook-pagetoc
|
|
||||||
|
|
||||||
# -- Codebase Documentation
|
|
||||||
|
|
||||||
.PHONY : haddock
|
.PHONY : haddock
|
||||||
haddock :
|
haddock :
|
||||||
@cabal --docdir=docs/ --htmldir=docs/ haddock --enable-documentation
|
@cabal --docdir=docs/ --htmldir=docs/ haddock --enable-documentation
|
||||||
|
|||||||
@ -1,56 +0,0 @@
|
|||||||
# Summary
|
|
||||||
|
|
||||||
- [The Juvix project](./README.md)
|
|
||||||
- [Changelog](./CHANGELOG.md)
|
|
||||||
- [Quick start](./quick-start.md)
|
|
||||||
|
|
||||||
# Tutorials
|
|
||||||
|
|
||||||
- [Learn Juvix in minutes](./tutorials/learn.md)
|
|
||||||
- [Structuring Juvix projects](./tutorials/structure.md)
|
|
||||||
- [Juvix Emacs mode](./tutorials/emacs.md)
|
|
||||||
- [Juvix VSCode extension](./tutorials/vscode.md)
|
|
||||||
|
|
||||||
# How-to guides
|
|
||||||
|
|
||||||
- [Installing Juvix](./howto/installing.md)
|
|
||||||
- [Compiling Juvix programs](./howto/compilation.md)
|
|
||||||
- [Judoc: Juvix documentation tool](./howto/judoc.md)
|
|
||||||
|
|
||||||
# Explanations
|
|
||||||
|
|
||||||
- [Type theory](./explanations/typetheory.md)
|
|
||||||
- [Totality checking](./explanations/totality/README.md)
|
|
||||||
- [Termination](./explanations/totality/termination.md)
|
|
||||||
- [Strictly positive data
|
|
||||||
types](./explanations/totality/positive.md)
|
|
||||||
- [Coverage checking](./explanations/totality/coverage.md)
|
|
||||||
|
|
||||||
# Reference
|
|
||||||
|
|
||||||
- [Standard library](./reference/stdlib.md)
|
|
||||||
- [Language reference](./reference/language/README.md)
|
|
||||||
- [Project](./reference/language/project.md)
|
|
||||||
- [Functions](./reference/language/functions.md)
|
|
||||||
- [Infix operators](./reference/language/infix.md)
|
|
||||||
- [Data types](./reference/language/datatypes.md)
|
|
||||||
- [Modules](./reference/language/modules.md)
|
|
||||||
- [Statements](./reference/language/statement.md)
|
|
||||||
- [Local definitions](./reference/language/let.md)
|
|
||||||
- [Control structures](./reference/language/control.md)
|
|
||||||
- [Comments](./reference/language/comments.md)
|
|
||||||
- [Axioms](./reference/language/axioms.md)
|
|
||||||
- [Example programs](./reference/examples.md)
|
|
||||||
- [Benchmarks](./reference/benchmarks.md)
|
|
||||||
- [Tooling](./reference/tooling/README.md)
|
|
||||||
- [Command line interface](./reference/tooling/CLI.md)
|
|
||||||
- [Doctor](./reference/tooling/doctor.md)
|
|
||||||
- [Emacs mode](./reference/tooling/emacs.md)
|
|
||||||
- [Haskell test suite](./reference/tooling/testing.md)
|
|
||||||
- [Judoc reference](./reference/judoc.md)
|
|
||||||
|
|
||||||
# About
|
|
||||||
|
|
||||||
- [Community](./about/community.md)
|
|
||||||
- [Contributing](./CONTRIBUTING.md)
|
|
||||||
- [License](./LICENSE.md)
|
|
||||||
@ -1,8 +0,0 @@
|
|||||||
# Juvix community
|
|
||||||
|
|
||||||
Join us on our [Discord server](https://discord.gg/waYhQ2Qr)
|
|
||||||
|
|
||||||
This project is part of a bigger effort called
|
|
||||||
[Anoma](https://anoma.net/). Anoma is a suite of protocols and
|
|
||||||
mechanisms for self-contained, self-sovereign coordination. Join the
|
|
||||||
[Anoma project](https://anoma.net/community).
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# The Juvix Dev Team
|
|
||||||
1547
docs/changelog.md
1547
docs/changelog.md
File diff suppressed because it is too large
Load Diff
@ -1,15 +0,0 @@
|
|||||||
## [Examples of programs written in Juvix](https://github.com/anoma/juvix/tree/main/examples/milestone)
|
|
||||||
|
|
||||||
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](./html/examples/html/HelloWorld/HelloWorld.html)
|
|
||||||
- [Fibonacci.juvix](./html/examples/html/Fibonacci/Fibonacci.html)
|
|
||||||
- [Hanoi.juvix](./html/examples/html/Hanoi/Hanoi.html)
|
|
||||||
- [PascalsTriangle.juvix](./html/examples/html/PascalsTriangle/PascalsTriangle.html)
|
|
||||||
- [Collatz.juvix](./html/examples/html/Collatz/Collatz.html)
|
|
||||||
- [TicTacToe.juvix](./html/TicTacToe/CLI/CLI.TicTacToe.html)
|
|
||||||
|
|
||||||
The [Juvix standard library](https://anoma.github.io/juvix-stdlib/)
|
|
||||||
contains common functions that can be used in Juvix programs.
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Totality checking
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Coverage checking
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Strictly positive data types
|
|
||||||
@ -1,29 +0,0 @@
|
|||||||
# 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 fulfil, 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.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
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
|
|
||||||
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 slight modification of the algorithm for checking
|
|
||||||
termination in the Foetus's language.
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Type theory
|
|
||||||
@ -1,61 +0,0 @@
|
|||||||
# Compiling simple programs
|
|
||||||
|
|
||||||
A Juvix file must declare a module whose name corresponds exactly to the
|
|
||||||
name of the file. For example, a file `Hello.juvix` must declare a
|
|
||||||
module `Hello`:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- Hello world example. This is a comment.
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
-- Import the standard library prelude, including the 'String' type
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : String;
|
|
||||||
main := "Hello world!";
|
|
||||||
```
|
|
||||||
|
|
||||||
A file compiled to an executable must define the zero-argument function
|
|
||||||
`main` of type `IO` which is evaluated when running the program.
|
|
||||||
|
|
||||||
To compile the file `Hello.juvix` type `juvix compile Hello.juvix`.
|
|
||||||
Typing `juvix compile --help` will list all options to the `compile`
|
|
||||||
command.
|
|
||||||
|
|
||||||
# Compilation targets
|
|
||||||
|
|
||||||
Since version 0.3 Juvix supports three compilation targets. The targets
|
|
||||||
are specified with the `-t` option:
|
|
||||||
`juvix compile -t target file.juvix`.
|
|
||||||
|
|
||||||
1. `native`. This is the default. Produces a native 64bit executable
|
|
||||||
for your machine.
|
|
||||||
2. `wasm32-wasi`. Produces a WebAssembly binary which uses the WASI
|
|
||||||
runtime.
|
|
||||||
3. `geb`. Produces a [GEB](https://anoma.github.io/geb/) input file.
|
|
||||||
|
|
||||||
# Compilation options
|
|
||||||
|
|
||||||
To see all compilation options type `juvix compile --help`. The most
|
|
||||||
commonly used options are:
|
|
||||||
|
|
||||||
- `-t target`: specify the target,
|
|
||||||
- `-g`: generate debug information and runtime assertions,
|
|
||||||
- `-o file`: specify the output file.
|
|
||||||
|
|
||||||
# Juvix projects
|
|
||||||
|
|
||||||
A <u>Juvix project</u> is a collection of Juvix modules inside one main
|
|
||||||
project directory containing a `juvix.yaml` metadata file. The name of
|
|
||||||
each module must coincide with the path of the file it is defined in,
|
|
||||||
relative to the project's root directory. For example, if the file is
|
|
||||||
`root/Data/List.juvix` then the module must be called `Data.List`,
|
|
||||||
assuming `root` is the project's directory.
|
|
||||||
|
|
||||||
To interactively initialize a Juvix project in the current directory,
|
|
||||||
use `juvix init`.
|
|
||||||
|
|
||||||
To check that Juvix is correctly detecting your project's root, you can
|
|
||||||
run the command `juvix dev root File.juvix`.
|
|
||||||
|
|
||||||
See also: [Modules Reference](../reference/language/modules.md).
|
|
||||||
@ -1,135 +0,0 @@
|
|||||||
# Dependencies
|
|
||||||
|
|
||||||
You need [Clang / LLVM](https://releases.llvm.org/download.html) version
|
|
||||||
13 or later. Note that on macOS the preinstalled clang does not support
|
|
||||||
the wasm target, so use e.g. `brew install llvm` instead.
|
|
||||||
|
|
||||||
If you want to compile to WebAssembly, you also need:
|
|
||||||
|
|
||||||
- [wasmer](https://wasmer.io)
|
|
||||||
- [wasi-sdk](https://github.com/WebAssembly/wasi-sdk/releases)
|
|
||||||
- [wasm-ld](https://lld.llvm.org) - 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`).
|
|
||||||
|
|
||||||
See [below](./installing.md#installing-dependencies) for instructions on
|
|
||||||
how to install the dependencies.
|
|
||||||
|
|
||||||
# Installing Juvix
|
|
||||||
|
|
||||||
### MacOS
|
|
||||||
|
|
||||||
The easiest way to install Juvix on MacOS is by using
|
|
||||||
[Homebrew](https://brew.sh).
|
|
||||||
|
|
||||||
To install the [homebrew-juvix
|
|
||||||
tap](https://github.com/anoma/homebrew-juvix), run:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
brew tap anoma/juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
To install Juvix, run:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
brew install juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
Helpful information can also be obtained by running:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
brew info juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
### Linux x86<sub>64</sub>
|
|
||||||
|
|
||||||
A Juvix compiler binary executable for Linux x86<sub>64</sub> is
|
|
||||||
available on the [Juvix release
|
|
||||||
page](https://github.com/anoma/juvix/releases/latest).
|
|
||||||
|
|
||||||
To install this executable, download and unzip the linked file and move
|
|
||||||
it to a directory on your shell's `PATH`.
|
|
||||||
|
|
||||||
For example if `~/.local/bin` is on your shell's `PATH`, you can install
|
|
||||||
Juvix as follows:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
cd /tmp
|
|
||||||
curl -OL https://github.com/anoma/juvix/releases/download/v0.3.2/juvix-linux_x86_64-v0.3.2.zip
|
|
||||||
unzip juvix-linux_x86_64-v0.3.2.zip
|
|
||||||
mv juvix-linux_x86_64-v0.3.2 ~/.local/bin/juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
### Building Juvix from source
|
|
||||||
|
|
||||||
To install Juvix from source you must clone the [Github
|
|
||||||
repository](https://github.com/anoma/juvix.git). Then Juvix can be
|
|
||||||
installed with the following commands. We assume you have
|
|
||||||
[Stack](https://haskellstack.org) and [GNU
|
|
||||||
Make](https://www.gnu.org/software/make/) installed.
|
|
||||||
|
|
||||||
```shell
|
|
||||||
git clone --recursive https://github.com/anoma/juvix.git
|
|
||||||
cd juvix
|
|
||||||
make install
|
|
||||||
```
|
|
||||||
|
|
||||||
The C compiler and linker paths can be specified as options to the
|
|
||||||
`make install` command, e.g.
|
|
||||||
|
|
||||||
```shell
|
|
||||||
make install CC=path/to/clang LIBTOOL=path/to/llvm-ar
|
|
||||||
```
|
|
||||||
|
|
||||||
On MacOS, you can alternatively run the following command for Homebrew.
|
|
||||||
The flag `--HEAD` used below is optional – use it to build the latest
|
|
||||||
version of Juvix in the `main` branch on Github.
|
|
||||||
|
|
||||||
```shell
|
|
||||||
brew install --build-from-source --HEAD juvix --verbose
|
|
||||||
```
|
|
||||||
|
|
||||||
### Building the project with `cabal`
|
|
||||||
|
|
||||||
We recommend to use the `stack` build tool with this project.
|
|
||||||
|
|
||||||
If you prefer the `cabal` build tool instead, then you need to generate
|
|
||||||
the `juvix.cabal` file using [hpack](https://github.com/sol/hpack)
|
|
||||||
before running `cabal build`.
|
|
||||||
|
|
||||||
You also need to compile the runtime first:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
make runtime
|
|
||||||
cabal build
|
|
||||||
```
|
|
||||||
|
|
||||||
# Installing dependencies
|
|
||||||
|
|
||||||
To install `wasi-sdk` you need to download `libclang_rt` and
|
|
||||||
`wasi-sysroot` precompiled archives from the [wasi-sdk release
|
|
||||||
page](https://github.com/WebAssembly/wasi-sdk/releases/) 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:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
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:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
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
|
|
||||||
```
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Documenting Juvix programs with Judoc
|
|
||||||
@ -1,82 +0,0 @@
|
|||||||
---
|
|
||||||
author: Jan Mas Rovira
|
|
||||||
title: Builtins
|
|
||||||
---
|
|
||||||
|
|
||||||
# Overview
|
|
||||||
|
|
||||||
The goal is to support builtin types and functions that get compiled to
|
|
||||||
efficient primitives. We plan on supporting primitives for the following
|
|
||||||
types of definitions:
|
|
||||||
|
|
||||||
1. Builtin inductive definitions. For example:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
builtin nat
|
|
||||||
type Nat :=
|
|
||||||
zero : Nat |
|
|
||||||
suc : Nat → Nat;
|
|
||||||
```
|
|
||||||
|
|
||||||
We will call this the canonical definition of natural numbers.
|
|
||||||
|
|
||||||
2. Builtin function definitions. For example:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
inifl 6 +;
|
|
||||||
builtin nat-plus
|
|
||||||
+ : Nat → Nat → Nat;
|
|
||||||
+ zero b := b;
|
|
||||||
+ (suc a) b := suc (a + b);
|
|
||||||
```
|
|
||||||
|
|
||||||
3. Builtin axiom definitions. For example:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
builtin nat-print
|
|
||||||
axiom printNat : Nat → Action;
|
|
||||||
```
|
|
||||||
|
|
||||||
## Collecting builtin information
|
|
||||||
|
|
||||||
The idea is that builtin definitions are treated normally throughout the
|
|
||||||
pipeline except in the backend part. There is one exception to that. We
|
|
||||||
need to collect information about the builtins that have been included
|
|
||||||
in the code and what are the terms that refer to them. For instance,
|
|
||||||
imagine that we find this definitions in a juvix module:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
builtin nat
|
|
||||||
type MyNat :=
|
|
||||||
z : MyNat |
|
|
||||||
s : MyNat → MyNat;
|
|
||||||
```
|
|
||||||
|
|
||||||
We need to take care of the following:
|
|
||||||
|
|
||||||
1. Check that the definition `MyInt` is up to renaming equal to the
|
|
||||||
canonical definition that we provide in the compiler.
|
|
||||||
2. Rember a map from concrete to canonical names: {MyNat ↦ Nat; z ↦
|
|
||||||
zero; s ↦ suc};
|
|
||||||
3. Rembember that we have a definition for builtin natural numbers.
|
|
||||||
This is necessary if later we attempt to define a builtin function
|
|
||||||
or axiom that depends on natural numbers.
|
|
||||||
|
|
||||||
In the compiler we need to know the following:
|
|
||||||
|
|
||||||
1. For inductives:
|
|
||||||
1. What is the primitive type that we will target in the backend:
|
|
||||||
E.g. {Nat ↦ int}.
|
|
||||||
2. For constructors:
|
|
||||||
1. What is the primitive constructor function: E.g. {zero ↦ 0;
|
|
||||||
suc ↦ plus<sub>one</sub>};
|
|
||||||
2. How to test if a term matches a pattern with that
|
|
||||||
constructor. E.g. {zero ↦ is<sub>zero</sub>; suc ↦
|
|
||||||
is<sub>notzero</sub>};
|
|
||||||
3. How to deconstruct/project each of the constructor
|
|
||||||
arguments. E.g. {zero ↦ ∅; suc ↦ minus<sub>one</sub>}}. Note
|
|
||||||
that if a constructor takes multiple arguments we will need
|
|
||||||
to have a projection function for each argument.
|
|
||||||
2. For functions and axioms:
|
|
||||||
1. What is the primitive function that we will target in the
|
|
||||||
backend: E.g. {+ ↦ add}.
|
|
||||||
@ -1,16 +0,0 @@
|
|||||||
# LSP support
|
|
||||||
|
|
||||||
We provide a sample `hie.yaml` configuration file for both `cabal` and
|
|
||||||
`stack`.
|
|
||||||
|
|
||||||
If you prefer `stack`, run:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
cp stack.hie.yaml hie.yaml
|
|
||||||
```
|
|
||||||
|
|
||||||
If you prefer `cabal`, run:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
cp cabal.hie.yaml hie.yaml
|
|
||||||
```
|
|
||||||
@ -1,228 +0,0 @@
|
|||||||
---
|
|
||||||
author: Jan Mas Rovira
|
|
||||||
---
|
|
||||||
|
|
||||||
# Monomorphization
|
|
||||||
|
|
||||||
(Removed in v0.2.5)
|
|
||||||
|
|
||||||
Monomorphization refers to the process of converting polymorphic code to
|
|
||||||
monomorphic code (no type variables) through static analysis.
|
|
||||||
|
|
||||||
Example:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
id : (A : Type) → A → A;
|
|
||||||
id _ a := a;
|
|
||||||
|
|
||||||
b : Bool;
|
|
||||||
b := id Bool true;
|
|
||||||
|
|
||||||
n : Nat;
|
|
||||||
n := id Nat zero;
|
|
||||||
```
|
|
||||||
|
|
||||||
Is translated into:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
id_Bool : Bool → Bool;
|
|
||||||
id_Bool a := a;
|
|
||||||
|
|
||||||
id_Nat : Nat → Nat;
|
|
||||||
id_Nat a := a;
|
|
||||||
```
|
|
||||||
|
|
||||||
# More examples
|
|
||||||
|
|
||||||
## Mutual recursion
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type 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:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
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 <span class="spurious-link" target="Types">_Types_</span>.
|
|
||||||
|
|
||||||
### 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.
|
|
||||||
@ -1,343 +0,0 @@
|
|||||||
# Benchmarks of the new Juvix runtime
|
|
||||||
|
|
||||||
Benchmarked version: commit 148ececb4d4259eacbb980f5992073a3ac611d82
|
|
||||||
from 31.10.2022
|
|
||||||
|
|
||||||
## Summary
|
|
||||||
|
|
||||||
We benchmark several programs manually compiled into the primitives of
|
|
||||||
the new Juvix runtime. The code corresponds closely to the code that
|
|
||||||
will be generated by the new compilation process, with basic low-level
|
|
||||||
optimisations (unboxing, untagging, etc.) but without any high-level
|
|
||||||
optimisations on JuvixCore (inlining, specialisation, constant folding,
|
|
||||||
fusion, etc.). This corresponds to the compilation process planned for
|
|
||||||
the 0.4 milestone.
|
|
||||||
|
|
||||||
We compare the running time and memory usage with analogous programs
|
|
||||||
written in Haskell, OCaml, JuvixCore (using the evaluator), current
|
|
||||||
Juvix (with the "direct" transpilation to C) and C.
|
|
||||||
|
|
||||||
The results suggest that for most first-order programs the new
|
|
||||||
compilation process will produce code with running time comparable to
|
|
||||||
the code produced by the native OCaml compiler. For higher-order
|
|
||||||
programs heavy on closure manipulation, the results are acceptable but
|
|
||||||
noticeably worse, especially with third-order functions (i.e. functions
|
|
||||||
which take functions taking functions). This could, however, be
|
|
||||||
alleviated by implementing the specialisation optimisation (see the
|
|
||||||
"specialised" column in the \`ackermann\` and \`mapfun\` benchmarks).
|
|
||||||
Besides, functional programs of order higher than two are rare.
|
|
||||||
|
|
||||||
The comparisons with OCaml and Haskell were not entirely fair because
|
|
||||||
the new Juvix runtime does not perform garbage collection. The overhead
|
|
||||||
of garbage collection is particularly visible on the \`mergesort\`
|
|
||||||
benchmark which creates many intermediate data structures that are
|
|
||||||
quickly discarded. With proper memory management, the running time
|
|
||||||
results on first-order programs for the new Juvix runtime are expected
|
|
||||||
to become slightly worse than for the native OCaml compiler.
|
|
||||||
|
|
||||||
For simple programs operating on integers which don't require any heap
|
|
||||||
memory allocation (\`fibonacci\` and \`combinations\` benchmarks), the
|
|
||||||
direct transpilation to C in the current Juvix seems to perform best
|
|
||||||
(behind only C). The reason is that for very simple programs \`clang\`
|
|
||||||
can better optimise the output of such a direct transpiler. The main
|
|
||||||
problem with the transpilation to C approach is that it cannot scale to
|
|
||||||
reliably work for more complex programs, as evidenced by the segfaults,
|
|
||||||
longer running time and higher memory use on other benchmarks.
|
|
||||||
|
|
||||||
In addition to the \`fibonacci\` and \`combinations\` benchmarks, the
|
|
||||||
advantage of direct transpilation for very simple programs is also
|
|
||||||
visible on the \`fold\` benchmark where a simple loop over a list
|
|
||||||
dominates the running time. However, this is partly because the
|
|
||||||
compilation of closures in current Juvix is incorrect allowing it to be
|
|
||||||
more efficient.
|
|
||||||
|
|
||||||
## Benchmark programs
|
|
||||||
|
|
||||||
# fibonacci: compute the Nth Fibonacci number modulo 2<sup>28</sup> (N = 100’000’000)
|
|
||||||
|
|
||||||
The Nth Fibonacci number is computed in O(N). Needs only constant stack
|
|
||||||
space and no heap memory. This benchmark tests the efficiency of tail
|
|
||||||
recursion and arithmetic operations.
|
|
||||||
|
|
||||||
# combinations: count combinations of numbers 1 to N having sum N (N = 100)
|
|
||||||
|
|
||||||
This benchmark tests the efficiency of general recursion. No heap memory
|
|
||||||
needs to be allocated. Uses stack space proportional to N. The running
|
|
||||||
time is exponential in N.
|
|
||||||
|
|
||||||
# prime: compute the Nth prime (N = 16384)
|
|
||||||
|
|
||||||
The Nth prime number is computed via the Eratosthenes sieve. A list of N
|
|
||||||
primes is created. No intermediate lists are discarded (garbage
|
|
||||||
collection not needed). This benchmark tests the efficiency of tail
|
|
||||||
recursion, arithmetic operations, list cell allocation and access.
|
|
||||||
|
|
||||||
# mergesort: merge sort a list of N integers (N = 2’000’000)
|
|
||||||
|
|
||||||
At each level of merge sort intermediate lists are created and
|
|
||||||
discarded. The running time for this benchmark largely depends on the
|
|
||||||
efficiency of memory management. Here one may observe the overhead of
|
|
||||||
garbage collection or the memory blow-up if no garbage collection is
|
|
||||||
used.
|
|
||||||
|
|
||||||
# maybe: optionally sum N integers from a binary tree K times (N = 2<sup>20</sup>, K = 100)
|
|
||||||
|
|
||||||
If a fixed number k is encountered in the tree then the result is
|
|
||||||
\`Nothing\`, otherwise it is \`Just sum\`. The computation is repeated
|
|
||||||
for values of k from 0 to K. This tests the efficiency of handling
|
|
||||||
optional values and data structure access.
|
|
||||||
|
|
||||||
# fold: fold a list of N integers K times (N = 100’000, K = 1000)
|
|
||||||
|
|
||||||
The sum of N natural numbers is computed via fold<sub>left</sub>
|
|
||||||
(tail-recursive). The computation is repeated K times. The list is
|
|
||||||
created only once, so that allocation time does not dominate. This
|
|
||||||
benchmark tests the efficiency of closure call and list cell access.
|
|
||||||
|
|
||||||
# cps: compute the Nth Fibonacci number modulo 2<sup>28</sup> with CPS (N = 100’000’000)
|
|
||||||
|
|
||||||
The function computing the Nth Fibonacci number is written in
|
|
||||||
continuation-passing style, tail-recursively calling a continuation
|
|
||||||
supplied as an argument. This benchmark tests the efficiency of closure
|
|
||||||
call and allocation.
|
|
||||||
|
|
||||||
# mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
|
|
||||||
|
|
||||||
This benchmark tests the efficiency of standard higher-order functions
|
|
||||||
on lists, closure call and memory management. The program allocates O(K)
|
|
||||||
intermediate lists of length N which are quickly discarded.
|
|
||||||
|
|
||||||
# ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
|
|
||||||
|
|
||||||
The higher-order Ackermann function definition iterates an iteration of
|
|
||||||
function compositions. Hence, it uses a third-order invocation of an
|
|
||||||
iteration function. This benchmark tests the efficiency of creating and
|
|
||||||
calling second-order closures, and of partial application.
|
|
||||||
|
|
||||||
# mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
|
|
||||||
|
|
||||||
The benchmark stores K second-order closures in a list, maps them
|
|
||||||
successively to a list of K closures, and then successively maps the K
|
|
||||||
closures from the result to a list of N integers. This benchmark tests
|
|
||||||
the efficiency of manipulating closures and storing them in data
|
|
||||||
structures.
|
|
||||||
|
|
||||||
The benchmark programs can be found in \`tests/benchmark\` in the Juvix
|
|
||||||
source directory.
|
|
||||||
|
|
||||||
## Methodology
|
|
||||||
|
|
||||||
For each program the total running time (elapsed real time) and memory
|
|
||||||
use (maximum resident set size) were measured on an M1 iMac with no
|
|
||||||
significant background activity. Averages of several runs were taken.
|
|
||||||
The variance was negligible, unless indicated otherwise by providing a
|
|
||||||
range.
|
|
||||||
|
|
||||||
## Results
|
|
||||||
|
|
||||||
# fibonacci: compute the Nth Fibonacci number modulo 2<sup>28</sup> (N = 100’000’000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.26 | 0.35 | 0.35 | 0.23 | 13.15 | 10.03 | 0.39 | 0.35 | 0.94 | 0.16 | 0.22 |
|
|
||||||
| Memory use (MB, max RSS) | 1.5 | 3.8 | 1.3 | 8.8 | 21.3 | 8067.7 | 9.7 | 1.7 | 1.8 | 1.3 | 4.0 |
|
|
||||||
|
|
||||||
# combinations: count all combinations of numbers 1 to N having sum N (N = 1000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 6.67 | 11.25 | 3.22 | 5.1 | 441.71 | 5.48 | 5.48 | 6.53 | 41.08 | 2.69 | 4.80 |
|
|
||||||
| Memory use (MB, max RSS) | 1.5 | 3.9 | 1.3 | 8.9 | 22.3 | 9.6 | 9.6 | 1.7 | 1.9 | 1.3 | 4.0 |
|
|
||||||
|
|
||||||
# prime: compute the Nth prime (N = 16384)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 1.52 | 1.91 | segfault | 3.09 | 167.04 | 3.85 | 3.85 | 1.68 | 14.82 | 0.12 | 0.13 |
|
|
||||||
| Memory use (MB, max RSS) | 1.7 | 4.0 | segfault | 9.3 | 24.4 | 9.8 | 9.6 | 2.2 | 2.2 | 1.4 | 4.0 |
|
|
||||||
|
|
||||||
# mergesort: merge sort a list of N integers (N = 2’000’000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.40 | 0.31 | 3.55 | 1.32 | 22.45 | 2.86 | 2.90 | 1.95 | 3.52 | 0.15 | 0.15 |
|
|
||||||
| Memory use (MB, max RSS) | 1973.7 | 720.4 | 5046.7 | 2729.8 | 1728.9 | 253.6 | 253.6 | 172.6 | 343.1 | 24.4 | 26.8 |
|
|
||||||
|
|
||||||
# maybe: optionally sum N non-zero integers from a binary tree K times (N = 2<sup>20</sup>, K = 100)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.45 | 0.64 | 3.29 | 1.57 | 22.75 | 5.58 | 0.59 | 0.30 | 3.57 | 0.27 | 0.50 |
|
|
||||||
| Memory use (MB, max RSS) | 1.6 | 3.8 | 2646.1 | 1320.9 | 22.4 | 5560.7 | 9.7 | 3.9 | 4.0 | 1.3 | 4.1 |
|
|
||||||
|
|
||||||
# fold: fold a list of N integers K times (N = 100’000, K = 1000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.45 | 0.54 | 0.35 | 0.23 | 15.27 | 0.58 | 0.58 | 0.36 | 1.80 | NA | NA |
|
|
||||||
| Memory use (MB, max RSS) | 3.1 | 4.6 | 4.4 | 10.6 | 43.4 | 12.7 | 12.7 | 5.9 | 5.9 | NA | NA |
|
|
||||||
|
|
||||||
# cps: compute the Nth Fibonacci number modulo 2<sup>28</sup> with CPS (N = 100’000’000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.43 | 0.52 | 1.56 | stack overflow | 20.22 | 10.04 | 0.39 | 0.35 | 1.60 | 0.16 | 0.25 |
|
|
||||||
| Memory use (MB, max RSS) | 1.5 | 3.9 | 1539.3 | stack overflow | 21.3 | 8067.7 | 9.7 | 1.7 | 1.8 | 1.3 | 4.0 |
|
|
||||||
|
|
||||||
# mapfold: map and fold a list of N integers K times (N = 10000, K = 10000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 1.01 | 1.59 | 2.74 | 1.81 | 38.24 | 1.29 | 2.42 | 1.43 | 4.22 | NA | NA |
|
|
||||||
| Memory use (MB, max RSS) | 2154.5 | 893.0 | 3059.1 | 1542.0 | 26.4 | 10.6 | 10.7 | 7.5 | 10-20 | NA | NA |
|
|
||||||
|
|
||||||
# ackermann: compute Ack(3, N) with the higher-order Ackermann function definition (N = 11)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | New Juvix runtime (specialised, native) | New Juvix runtime (specialised, wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | --------------------------------------- | ----------------------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 0.92 | 1.21 | 0.30 | 0.65 | segfault | runtime error | 11.71 | 0.87 | 0.47 | 0.54 | 1.35 | 0.00 | 0.14 |
|
|
||||||
| Memory use (MB, max RSS) | 2.6 | 4.1 | 2.3 | 3.9 | segfault | runtime error | 23.3 | 13.6 | 9.6 | 2.0 | 3.6 | 1.3 | 4.0 |
|
|
||||||
|
|
||||||
# mapfun: successively map K functions to a list of N integers (K = 100, N = 10000)
|
|
||||||
|
|
||||||
| | New Juvix runtime (native) | New Juvix runtime (wasm32, wasmer) | New Juvix runtime (specialised, native) | New Juvix runtime (specialised, wasm32, wasmer) | Current Juvix (native) | Current Juvix (wasm32, wasmer) | JuvixCore evaluator | Haskell (native, ghc -O2) | Haskell (native, ghc -XStrict -O2) | OCaml (native, ocamlopt -O2) | OCaml (bytecode) | C (native, clang -O3) | C (wasm32, clang -Os, wasmer) |
|
|
||||||
| ------------------------ | -------------------------- | ---------------------------------- | --------------------------------------- | ----------------------------------------------- | ---------------------- | ------------------------------ | ------------------- | ------------------------- | ---------------------------------- | ---------------------------- | ---------------- | --------------------- | ----------------------------- |
|
|
||||||
| Time (seconds, real) | 1.27 | 1.04 | 0.39 | 0.46 | segfault | runtime error | 4.18 | 1.85 | 0.95 | 0.19 | 0.68 | NA | NA |
|
|
||||||
| Memory use (MB, max RSS) | 3209.8 | 1229.7 | 21.8 | 13.2 | segfault | runtime error | 33.0 | 13.6 | 11.6 | 5.3 | 7.9 | NA | NA |
|
|
||||||
|
|
||||||
Comments
|
|
||||||
|
|
||||||
---
|
|
||||||
|
|
||||||
# "New Juvix runtime" denotes C programs written using the primitives
|
|
||||||
|
|
||||||
of the new Juvix runtime. These programs were "manually" compiled from
|
|
||||||
the corresponding Juvix/JuvixCore programs, according to the new Juvix
|
|
||||||
compilation concept. They correspond closely to the code that will be
|
|
||||||
generated by the basic version of the new compilation process, without
|
|
||||||
any high-level optimisations (inlining, specialisation, fusion, constant
|
|
||||||
folding) but with basic low-level memory representation optimisations
|
|
||||||
(unboxing, untagging, etc). This version of the new compilation process
|
|
||||||
should be finished with the 0.4 milestone.
|
|
||||||
|
|
||||||
# The "specialised" column for "New Juvix runtime" denotes a version
|
|
||||||
|
|
||||||
of the corresponding "New Juvix runtime" benchmark program for which
|
|
||||||
specialisation of higher-order functions was manually performed (to
|
|
||||||
simulate the effects of the high-level specialisation optimisation).
|
|
||||||
|
|
||||||
# "Current Juvix" denotes Juvix programs compiled with the current
|
|
||||||
|
|
||||||
compilation process via a "direct" translation to C. For a fair
|
|
||||||
comparison, all number operations were implemented using native binary C
|
|
||||||
integers (exposed via \`foreign\` and \`compile\` blocks) without
|
|
||||||
overflow check, instead of using the unary Nat from the standard
|
|
||||||
library. For Haskell, we use the fixed-precision Int instead of the
|
|
||||||
arbitrary-precision Integer.
|
|
||||||
|
|
||||||
# For the simplest benchmark programs without heap memory allocation
|
|
||||||
|
|
||||||
(e.g. \`fibonacci\`, \`combinations\`), the performance of "Current
|
|
||||||
Juvix" is comparable to or better than that of "New Juvix runtime". This
|
|
||||||
is because \`clang\` managed to eliminate (tail) recursion and optimise
|
|
||||||
the code to essentially the same or better thing. The main problem with
|
|
||||||
the current "direct" transpilation to C approach is that it cannot scale
|
|
||||||
to reliably work for more complex programs. By "more complex" I mean
|
|
||||||
larger program size, more functions, more complex patterns of recursion
|
|
||||||
and/or the use of more functional programming features (including
|
|
||||||
functional data structures). I don't mean higher computational
|
|
||||||
complexity or more resource use.
|
|
||||||
|
|
||||||
# The segfaults and runtime errors for "Current Juvix" are
|
|
||||||
|
|
||||||
consequences of incorrectly generated code (current compilation of
|
|
||||||
partial application is not entirely correct) or stack overflows (when
|
|
||||||
\`clang\` didn't figure out how to eliminate tail recursion).
|
|
||||||
|
|
||||||
# The comparison with "Current Juvix" is not entirely fair for
|
|
||||||
|
|
||||||
benchmarks that test the manipulation and calling of closures (e.g.
|
|
||||||
\`fold\`). Current Juvix achieves good performance (when it doesn't
|
|
||||||
segfault) at the expense of correctness: partial application is not
|
|
||||||
compiled correctly and fixing this would require a fundamental change in
|
|
||||||
closure representation.
|
|
||||||
|
|
||||||
# The comparison with Haskell and OCaml compilers is not entirely
|
|
||||||
|
|
||||||
fair, because the new Juvix runtime does not perform garbage collection.
|
|
||||||
With the GC overhead, I would expect the Juvix runtime results for
|
|
||||||
native compilation of first-order programs to become a bit worse than
|
|
||||||
the native OCaml versions. The GC overhead is particularly noticeable
|
|
||||||
for the \`mergesort\` benchmark which creates many large intermediate
|
|
||||||
lists. The memory usage of the Juvix runtime is much higher on this
|
|
||||||
benchmark than the memory usage of OCaml or Haskell versions. The
|
|
||||||
relatively small time difference between the OCaml native and bytecode
|
|
||||||
versions of \`mergesort\` also indicates that GC accounts for a
|
|
||||||
significant part of the running time.
|
|
||||||
|
|
||||||
# Another small overhead will be introduced by bounds checking for
|
|
||||||
|
|
||||||
integer operations. Currently, the new Juvix runtime operates on unboxed
|
|
||||||
31-bit (or 63-bit) integers without checking for integer overflow.
|
|
||||||
|
|
||||||
# If we decide to default to transparent arbitrary-precision integers,
|
|
||||||
|
|
||||||
then another small overhead will be introduced by the need to check the
|
|
||||||
integer representation with each arithmetic operation.
|
|
||||||
|
|
||||||
# Admittedly, the programs were deliberately written in a way to make
|
|
||||||
|
|
||||||
high-level optimisations unnecessary, except specialisation for
|
|
||||||
higher-order functions (mostly in \`ackermann\` and \`mapfun\`). This
|
|
||||||
also explains the good performance of the OCaml native compiler which
|
|
||||||
doesn't do much high-level optimisation.
|
|
||||||
|
|
||||||
# In the "Current Juvix" and OCaml version of \`mergesort\`, to avoid
|
|
||||||
|
|
||||||
stack overflow the \`merge\` function was written tail-recursively with
|
|
||||||
accumulator reversal at the end. This is not necessary for the new Juvix
|
|
||||||
runtime, because the stack is dynamically extended when needed.
|
|
||||||
|
|
||||||
# As evidenced by the \`combinations\` benchmark, for non-tail-recursive
|
|
||||||
|
|
||||||
direct calls our code performs worse than the code which uses the C /
|
|
||||||
WebAssembly stack and function call mechanisms. However, in general it
|
|
||||||
is impossible to directly use the C / WebAssembly stack and call
|
|
||||||
mechanisms for a purely functional language. Since we dynamically
|
|
||||||
allocate the stack segments when needed, stack overflow is impossible.
|
|
||||||
This is convenient in an eager functional language. Otherwise, one needs
|
|
||||||
to rewrite all functions operating on large data to use tail recursion.
|
|
||||||
We pay for this convenience with a small overhead, which is the main
|
|
||||||
reason for poorer performance on \`combinations\` where stack
|
|
||||||
manipulation cost dominates.
|
|
||||||
|
|
||||||
# Haskell's laziness seems to introduce more overhead than I
|
|
||||||
|
|
||||||
expected. This would explain the comparatively better performance of the
|
|
||||||
native OCaml compiler. The problem is particularly stark when Haskell's
|
|
||||||
strictness analysis fails for some reason, as in the \`fibonacci\`
|
|
||||||
benchmark. The second "Haskell" column with the "-XStrict" flag for GHC
|
|
||||||
indicates the version of the benchmark compiled with strictness as the
|
|
||||||
default.
|
|
||||||
|
|
||||||
# The C versions of the programs were written to take advantage of C's
|
|
||||||
|
|
||||||
imperative features, e.g., using arrays instead of lists, loops instead
|
|
||||||
of recursion. No C versions are provided for some benchmarks designed to
|
|
||||||
test specifically functional language features.
|
|
||||||
|
|
||||||
# With the new Juvix runtime, the 32-bit WebAssembly version of
|
|
||||||
|
|
||||||
\`mergesort\` is faster than the 64-bit native version because it needs
|
|
||||||
roughly half as much memory (the word size is 4 bytes instead of 8). The
|
|
||||||
difference is even starker between the WebAssembly and native versions
|
|
||||||
of \`mergesort\` for "Current Juvix".
|
|
||||||
|
|
||||||
# There seems to be a memory leak in the JuvixCore evaluator. This is
|
|
||||||
|
|
||||||
what happens too often when one uses a lazy language.
|
|
||||||
|
|
||||||
# Haskell also leaks memory in the Fibonacci benchmark, despite it
|
|
||||||
|
|
||||||
being a simple tail-recursive program. It seems strictness analysis
|
|
||||||
didn't work.
|
|
||||||
@ -1,77 +0,0 @@
|
|||||||
# Strictly positive data types
|
|
||||||
|
|
||||||
We follow a syntactic description of strictly positive inductive data
|
|
||||||
types.
|
|
||||||
|
|
||||||
An inductive type is said to be <u>strictly positive</u> 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.
|
|
||||||
|
|
||||||
```minijuvix
|
|
||||||
axiom B : Type;
|
|
||||||
type 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 defining
|
|
||||||
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.
|
|
||||||
|
|
||||||
```minijuvix
|
|
||||||
type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
|
|
||||||
|
|
||||||
type 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 type checking a `Juvix` File.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix
|
|
||||||
module E5;
|
|
||||||
positive
|
|
||||||
type T0 (A : Type) :=
|
|
||||||
c0 : (T0 A -> A) -> T0 A;
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
## Examples of non-strictly data types
|
|
||||||
|
|
||||||
- `Bad` is not strictly positive because of the negative parameter
|
|
||||||
`A` of `Tree`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Tree (A : Type) :=
|
|
||||||
leaf : Tree A
|
|
||||||
| node : (A -> Tree A) -> Tree A;
|
|
||||||
|
|
||||||
type Bad :=
|
|
||||||
bad : Tree Bad -> Bad;
|
|
||||||
```
|
|
||||||
|
|
||||||
- `A` is a negative parameter.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type B (A : Type) :=
|
|
||||||
b : (A -> B (B A -> A)) -> B A;
|
|
||||||
```
|
|
||||||
@ -1,91 +0,0 @@
|
|||||||
# Quick Start
|
|
||||||
|
|
||||||
<a href="https://github.com/anoma/juvix">
|
|
||||||
<img align="left" width="200" height="200" alt="Juvix Mascot" src="assets/images/tara-teaching.svg" />
|
|
||||||
</a>
|
|
||||||
|
|
||||||
To install Juvix, follow the instructions in the [Installation
|
|
||||||
How-to](./howto/installing.md).
|
|
||||||
|
|
||||||
After installation, run `juvix --help` to see the list of commands.
|
|
||||||
|
|
||||||
Run Juvix doctor to check your system setup:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix doctor
|
|
||||||
```
|
|
||||||
|
|
||||||
## CLI Usage Examples
|
|
||||||
|
|
||||||
Create a new package:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix init
|
|
||||||
```
|
|
||||||
|
|
||||||
Compile a source file into an executable:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix compile path/to/source.juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
Compile a source file into a WebAssembly binary:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix compile -t wasm path/to/source.juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
Launch the REPL:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix repl
|
|
||||||
```
|
|
||||||
|
|
||||||
Typecheck a source file:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix typecheck path/to/source.juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
Generate HTML representations of a source file and its imports:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix html --recursive path/to/source.juvix
|
|
||||||
```
|
|
||||||
|
|
||||||
## The Hello World example
|
|
||||||
|
|
||||||
This is the Juvix source code of the traditional Hello World program.
|
|
||||||
|
|
||||||
```shell
|
|
||||||
-- HelloWorld.juvix
|
|
||||||
module HelloWorld;
|
|
||||||
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := printStringLn "hello world!";
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
To compile and run a binary generated by Juvix, save the source code to
|
|
||||||
a file called `HelloWorld.juvix` and run the following command from the
|
|
||||||
directory containing it:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix compile HelloWorld.juvix
|
|
||||||
./HelloWorld
|
|
||||||
```
|
|
||||||
|
|
||||||
You should see the output: `hello world!`
|
|
||||||
|
|
||||||
The source code can also be compiled to a WebAssembly binary. This
|
|
||||||
requires some additional setup. See the [Installation
|
|
||||||
How-to](https://anoma.github.io/juvix/howto/installing.html) for more
|
|
||||||
information. You can also run `juvix doctor` to check your setup.
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix compile --target wasm HelloWorld.juvix
|
|
||||||
wasmer HelloWorld.wasm
|
|
||||||
```
|
|
||||||
@ -1 +0,0 @@
|
|||||||
# Benchmarks
|
|
||||||
@ -1,10 +0,0 @@
|
|||||||
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](./../examples/html/HelloWorld/HelloWorld.html)
|
|
||||||
- [Fibonacci.juvix](./../examples/html/Fibonacci/Fibonacci.html)
|
|
||||||
- [Hanoi.juvix](./../examples/html/Hanoi/Hanoi.html)
|
|
||||||
- [PascalsTriangle.juvix](./../examples/html/PascalsTriangle/PascalsTriangle.html)
|
|
||||||
- [Collatz.juvix](./../examples/html/Collatz/Collatz.html)
|
|
||||||
- [TicTacToe.juvix](./../examples/html/TicTacToe/CLI/CLI.TicTacToe.html)
|
|
||||||
@ -1,120 +0,0 @@
|
|||||||
# Judoc syntax reference
|
|
||||||
|
|
||||||
Judoc is used to document parts of your code. You can attach _Judoc
|
|
||||||
blocks_ to the following entities:
|
|
||||||
|
|
||||||
1. A module.
|
|
||||||
2. A type definition.
|
|
||||||
3. A constructor definition.
|
|
||||||
4. A type signature of a function.
|
|
||||||
5. An axiom definition.
|
|
||||||
|
|
||||||
In order to attach documentation to any of these entities, write _blocks_ of
|
|
||||||
documentation before them:
|
|
||||||
|
|
||||||
1. For modules:
|
|
||||||
```
|
|
||||||
--- This module is cool
|
|
||||||
module Cool;
|
|
||||||
..
|
|
||||||
```
|
|
||||||
2. For type definitions:
|
|
||||||
```
|
|
||||||
--- Unary representation of natural numbers
|
|
||||||
type Nat : Type :=
|
|
||||||
| --- Nullary constructor representing number 0
|
|
||||||
zero : Nat
|
|
||||||
| --- Unary constructor representing the successor of a natural number
|
|
||||||
suc : Nat -> Nat;
|
|
||||||
```
|
|
||||||
3. For type signatures (and likewise for axioms):
|
|
||||||
|
|
||||||
```
|
|
||||||
--- The polymorphic identity function
|
|
||||||
id : {A : Type} -> A -> A;
|
|
||||||
```
|
|
||||||
|
|
||||||
Next we define the syntax of Judoc _blocks_.
|
|
||||||
|
|
||||||
## Block
|
|
||||||
|
|
||||||
A _block_ can be one of these:
|
|
||||||
|
|
||||||
1. A _paragraph_.
|
|
||||||
2. An _example_.
|
|
||||||
|
|
||||||
_Blocks_ are separated by a line with only `---`.
|
|
||||||
For instance, this is a sequence of two _blocks_:
|
|
||||||
|
|
||||||
```
|
|
||||||
--- First block
|
|
||||||
---
|
|
||||||
--- Second block
|
|
||||||
```
|
|
||||||
|
|
||||||
Note that the following is a single block since it lacks the `---` separator:
|
|
||||||
|
|
||||||
```
|
|
||||||
--- First block
|
|
||||||
|
|
||||||
--- Still first block
|
|
||||||
```
|
|
||||||
|
|
||||||
### Paragraph
|
|
||||||
|
|
||||||
A _paragraph_ is a non-empty sequence of _lines_.
|
|
||||||
|
|
||||||
For instance, the following is a paragraph with two _lines_:
|
|
||||||
|
|
||||||
```
|
|
||||||
--- First line
|
|
||||||
--- Second line
|
|
||||||
```
|
|
||||||
|
|
||||||
Note that a rendered paragraph will have have no line breaks. If you want to
|
|
||||||
have line breaks, you will need to split the paragraph. Hence, the paragraph
|
|
||||||
above will be rendered as
|
|
||||||
|
|
||||||
```
|
|
||||||
First line Second line
|
|
||||||
```
|
|
||||||
|
|
||||||
##### line
|
|
||||||
|
|
||||||
A _line_ starts with `---` and is followed by a non-empty sequence of
|
|
||||||
_atoms_.
|
|
||||||
|
|
||||||
For instance, the following is a valid _line_:
|
|
||||||
|
|
||||||
```
|
|
||||||
--- A ;Pair Int Bool; contains an ;Int; and a ;Bool;
|
|
||||||
```
|
|
||||||
|
|
||||||
##### Atom
|
|
||||||
|
|
||||||
An _atom_ is either:
|
|
||||||
|
|
||||||
1. A string of text (including spaces but not line breaks).
|
|
||||||
2. An inline Juvix expression surrounded by `;`.
|
|
||||||
|
|
||||||
For instance, the following are valid _atoms_:
|
|
||||||
|
|
||||||
1. `I am some text.`
|
|
||||||
2. `;Pair Int Bool;`
|
|
||||||
|
|
||||||
### Example
|
|
||||||
|
|
||||||
An example is of the following form
|
|
||||||
|
|
||||||
```
|
|
||||||
--- >>> someExpression ;
|
|
||||||
```
|
|
||||||
|
|
||||||
The `someExpression` can span multiple lines and it must be ended with a `;`.
|
|
||||||
For instance:
|
|
||||||
|
|
||||||
```
|
|
||||||
--- >>> 1
|
|
||||||
+ 2
|
|
||||||
+ 3;
|
|
||||||
```
|
|
||||||
@ -1,7 +0,0 @@
|
|||||||
- [Functions](./functions.md)
|
|
||||||
- [Data types](./datatypes.md)
|
|
||||||
- [Modules](./modules.md)
|
|
||||||
- [Local definitions](./let.md)
|
|
||||||
- [Control structures](./control.md)
|
|
||||||
- [Comments](./comments.md)
|
|
||||||
- [Axioms](./axioms.md)
|
|
||||||
@ -1,20 +0,0 @@
|
|||||||
# 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.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Example;
|
|
||||||
axiom
|
|
||||||
A : Type;
|
|
||||||
|
|
||||||
axiom
|
|
||||||
x : A;
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
Terms introduced by the `axiom` keyword lack any computational content.
|
|
||||||
Programs containing axioms not marked as builtins cannot be compiled to
|
|
||||||
most targets.
|
|
||||||
@ -1,30 +0,0 @@
|
|||||||
# Built-ins
|
|
||||||
|
|
||||||
Juvix has support for the built-in natural type and a few functions that
|
|
||||||
are compiled to efficient primitives.
|
|
||||||
|
|
||||||
1. Built-in inductive definitions.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
builtin nat
|
|
||||||
type Nat :=
|
|
||||||
zero : Nat |
|
|
||||||
suc : Nat → Nat;
|
|
||||||
```
|
|
||||||
|
|
||||||
2. Builtin function definitions.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
infixl 6 +;
|
|
||||||
builtin nat-plus
|
|
||||||
+ : Nat → Nat → Nat;
|
|
||||||
+ zero b := b;
|
|
||||||
+ (suc a) b := suc (a + b);
|
|
||||||
```
|
|
||||||
|
|
||||||
3. Builtin axiom definitions.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
builtin nat-print
|
|
||||||
axiom printNat : Nat → Action;
|
|
||||||
```
|
|
||||||
@ -1,18 +0,0 @@
|
|||||||
# Comments
|
|
||||||
|
|
||||||
Comments follow the same syntax as in `Haskell` and `Agda`. Be aware,
|
|
||||||
Juvix has no support for nested comments.
|
|
||||||
|
|
||||||
- Inline Comment
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- This is a comment!
|
|
||||||
```
|
|
||||||
|
|
||||||
- Region comment
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
{-
|
|
||||||
This is a comment!
|
|
||||||
-}
|
|
||||||
```
|
|
||||||
@ -1,34 +0,0 @@
|
|||||||
# Control structures
|
|
||||||
|
|
||||||
## Case
|
|
||||||
|
|
||||||
A case expression has the following syntax:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
case value
|
|
||||||
| pat1 := branch1
|
|
||||||
..
|
|
||||||
| patN := branchN
|
|
||||||
```
|
|
||||||
|
|
||||||
For example, one can evaluate the following expression in the REPL:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
Stdlib.Prelude> case 2 | zero := 0 | suc x := x | _ := 19
|
|
||||||
1
|
|
||||||
```
|
|
||||||
|
|
||||||
## Lazy builtins
|
|
||||||
|
|
||||||
The standard library provides several builtin functions which are
|
|
||||||
treated specially and evaluated lazily. These builtins must always be
|
|
||||||
fully applied.
|
|
||||||
|
|
||||||
- `if condition branch1 branch2`. First evaluates `condition`, if true
|
|
||||||
evaluates and returns `branch1`, otherwise evaluates and returns
|
|
||||||
`branch2`.
|
|
||||||
- `a || b`. Lazy disjunction. First evaluates `a`, if true returns
|
|
||||||
true, otherwise evaluates and returns `b`.
|
|
||||||
- `a && b`. Lazy conjunction. First evaluates `a`, if false returns
|
|
||||||
false, otherwise evaluates and returns `b`.
|
|
||||||
- `a >> b`. Sequences two IO actions. Lazy in the second argument.
|
|
||||||
@ -1,57 +0,0 @@
|
|||||||
# Data types
|
|
||||||
|
|
||||||
A data type declaration consists of:
|
|
||||||
|
|
||||||
- The `type` keyword,
|
|
||||||
- a unique name for the type,
|
|
||||||
- the `:=` symbol, and
|
|
||||||
- a non-empty list of constructor declarations (functions for
|
|
||||||
building the elements of the data type).
|
|
||||||
|
|
||||||
The simplest data type is the `Unit` type with one constructor called
|
|
||||||
`unit`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Unit := unit : Unit;
|
|
||||||
```
|
|
||||||
|
|
||||||
In the following example, we declare the type `Nat` – the unary
|
|
||||||
representation of natural numbers. This type comes with two
|
|
||||||
constructors: `zero` and `suc`. Example elements of type `Nat` are the
|
|
||||||
number one represented by `suc zero`, the number two represented by
|
|
||||||
`suc (suc zero)`, etc.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Nat :=
|
|
||||||
zero : Nat
|
|
||||||
| suc : Nat -> Nat;
|
|
||||||
```
|
|
||||||
|
|
||||||
Constructors can be used like normal functions or in patterns when
|
|
||||||
defining functions by pattern matching. For example, here is a function
|
|
||||||
adding two natural numbers:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
infixl 6 +;
|
|
||||||
+ : Nat -> Nat -> Nat;
|
|
||||||
+ zero b := b;
|
|
||||||
+ (suc a) b := suc (a + b);
|
|
||||||
```
|
|
||||||
|
|
||||||
A data type may have type parameters. A data type with a type parameter
|
|
||||||
`A` is called _polymorphic in_ `A`. A canonical example is the type
|
|
||||||
`List` polymorphic in the type of list elements.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
infixr 5 ::;
|
|
||||||
type 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;
|
|
||||||
```
|
|
||||||
|
|
||||||
For more examples of inductive types and how to use them, see [the Juvix
|
|
||||||
standard library](https://anoma.github.io/juvix-stdlib/).
|
|
||||||
@ -1,93 +0,0 @@
|
|||||||
# Function declarations
|
|
||||||
|
|
||||||
A function declaration consists of a type signature and a group of
|
|
||||||
_function clauses_.
|
|
||||||
|
|
||||||
In the following example, we define a function `multiplyByTwo`. The
|
|
||||||
first line `multiplyByTwo : Nat -> Nat;` is the type signature and the
|
|
||||||
second line `multiplyByTwo n := 2 * n;` is a function clause.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
multiplyByTwo : Nat -> Nat;
|
|
||||||
multiplyByTwo n := 2 * n;
|
|
||||||
```
|
|
||||||
|
|
||||||
A function may have more than one function clause. When a function is
|
|
||||||
called, the first clause that matches the arguments is used.
|
|
||||||
|
|
||||||
The following function has two clauses.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
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 each other 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`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
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;
|
|
||||||
```
|
|
||||||
|
|
||||||
## Anonymous functions
|
|
||||||
|
|
||||||
Anonymous functions, or _lambdas_, are introduced with the syntax:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
\{| pat1 .. patN_1 := clause1
|
|
||||||
| ..
|
|
||||||
| pat1 .. patN_M := clauseM}
|
|
||||||
```
|
|
||||||
|
|
||||||
The first pipe `|` is optional. Instead of `\` one can also use `λ`.
|
|
||||||
|
|
||||||
An anonymous function just lists all clauses of a function without
|
|
||||||
naming it. Any function declaration can be converted to use anonymous
|
|
||||||
functions:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
odd : Nat -> Bool;
|
|
||||||
even : Nat -> Bool;
|
|
||||||
|
|
||||||
odd := \{
|
|
||||||
| zero := false
|
|
||||||
| (suc n) := even n
|
|
||||||
};
|
|
||||||
|
|
||||||
even := \{
|
|
||||||
| zero := true
|
|
||||||
| (suc n) := odd n
|
|
||||||
};
|
|
||||||
```
|
|
||||||
|
|
||||||
## Short definitions
|
|
||||||
|
|
||||||
A function definition can be written in one line, with the body
|
|
||||||
immediately following the signature:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
multiplyByTwo : Nat -> Nat := \{n := 2 * n};
|
|
||||||
```
|
|
||||||
@ -1,3 +0,0 @@
|
|||||||
# Infix operators
|
|
||||||
|
|
||||||
TODO
|
|
||||||
@ -1,18 +0,0 @@
|
|||||||
# Local definitions
|
|
||||||
|
|
||||||
Local definitions are introduced with the `let` construct.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
sum : NList -> Nat;
|
|
||||||
sum lst :=
|
|
||||||
let
|
|
||||||
go : Nat -> NList -> Nat;
|
|
||||||
go acc nnil := acc;
|
|
||||||
go acc (ncons x xs) := go (acc + x) xs;
|
|
||||||
in
|
|
||||||
go 0 lst;
|
|
||||||
```
|
|
||||||
|
|
||||||
The declaractions in a `let` have the same syntax as declarations inside
|
|
||||||
a module, but they are visible only in the expression following the `in`
|
|
||||||
keyword.
|
|
||||||
@ -1,140 +0,0 @@
|
|||||||
# Module system
|
|
||||||
|
|
||||||
Modules are the way in which we split our programs in separate files. Juvix also
|
|
||||||
supports local modules, which provide a way to better organize different scopes
|
|
||||||
within a file.
|
|
||||||
|
|
||||||
We call top modules those who are defined at the top of a file.
|
|
||||||
We call local modules those who are defined inside another module.
|
|
||||||
|
|
||||||
## Top modules
|
|
||||||
|
|
||||||
A module has a name and a body, which comprises a sequence of
|
|
||||||
[statements](statement.md).
|
|
||||||
|
|
||||||
In order to define a module named `Data.List` we will use the following syntax:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Data.List;
|
|
||||||
|
|
||||||
<body>
|
|
||||||
```
|
|
||||||
|
|
||||||
### Top module naming convention
|
|
||||||
|
|
||||||
Top modules that belong to a [project](project.md) must follow a naming
|
|
||||||
convention. That is, if `dir` is the root of a project, then the module in
|
|
||||||
`dir/Data/List.juvix` must be named `Data.List`.
|
|
||||||
|
|
||||||
## _Import_ and _open_ statements
|
|
||||||
|
|
||||||
In order to access the definitions from another modules we use an
|
|
||||||
_import_ statement. To import some module named `Data.List` we will write
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
import Data.List;
|
|
||||||
```
|
|
||||||
|
|
||||||
Now, we can access the definitions in the imported module using _qualified
|
|
||||||
names_. E.g., `Data.List.sort`.
|
|
||||||
|
|
||||||
It is possible to import modules and give them a more convinent way thus:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
import Data.List as List;
|
|
||||||
```
|
|
||||||
|
|
||||||
If we want to access the contents of a module without the need to qualify the
|
|
||||||
names, we use an _open statement_. The syntax is as follows:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open Data.List;
|
|
||||||
```
|
|
||||||
|
|
||||||
Now we can simply write `sort`. It is important to remember that when we open a
|
|
||||||
module, that module must be in scope, i.e., it must either be imported
|
|
||||||
or defined as a local module
|
|
||||||
|
|
||||||
Since importing and opening a module is done often, there is special syntax for
|
|
||||||
that. The following statement:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Data.List;
|
|
||||||
```
|
|
||||||
|
|
||||||
Is equivalent to this:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
import Data.List;
|
|
||||||
open Data.List;
|
|
||||||
```
|
|
||||||
|
|
||||||
When opening a module, if we want to open an explicit subset of its definitions,
|
|
||||||
we must use the `using` keyword thus:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open Data.List using {List; sort; reverse}
|
|
||||||
```
|
|
||||||
|
|
||||||
If we want to open all definitions of a module minus a subset, we
|
|
||||||
must use the `hiding` keyword thus:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open Data.List hiding {head; tail}
|
|
||||||
```
|
|
||||||
|
|
||||||
All opened definitions are available under the current module, but
|
|
||||||
they are not exported by default. Meaning that if another module imports the current
|
|
||||||
module, it will only be able to access the definitions defined there but not
|
|
||||||
those which have been opened. If we want opened definitions to be exported, we
|
|
||||||
must use the `public` keyword thus:
|
|
||||||
|
|
||||||
```
|
|
||||||
module Prelude;
|
|
||||||
|
|
||||||
open import Data.List public;
|
|
||||||
```
|
|
||||||
|
|
||||||
Now, from another module we can access definitions in `Data.List` through the
|
|
||||||
`Prelude` module.
|
|
||||||
|
|
||||||
```
|
|
||||||
module MyModule;
|
|
||||||
|
|
||||||
open import Prelude;
|
|
||||||
|
|
||||||
-- List, sort, reverse, etc. are now in scope
|
|
||||||
```
|
|
||||||
|
|
||||||
## Local modules
|
|
||||||
|
|
||||||
Juvix modules have a hierarchical structure. So far we have discussed top level
|
|
||||||
modules, which have a one-to-one correspondence with files in the filesystem. On
|
|
||||||
the other hand, local modules are defined within another module. They can be
|
|
||||||
useful to group definitions within a file.
|
|
||||||
|
|
||||||
The syntax for local modules is as follows:
|
|
||||||
|
|
||||||
```
|
|
||||||
module Path.To.TopModule;
|
|
||||||
|
|
||||||
module Loc;
|
|
||||||
<body>
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
After the definition of a local module, we can access its definitions by using
|
|
||||||
qualified names. Local modules can be opened by open statements in the same way
|
|
||||||
as top modules.
|
|
||||||
|
|
||||||
Local modules inherit the scope of the parent module. Some shadowing rules
|
|
||||||
apply, and they probably follow your intuition:
|
|
||||||
|
|
||||||
1. Opening or defining a symbol shadows inherited instances of that symbol.
|
|
||||||
2. Opening a symbol does _not_ shadow a defined instanance of that symbol in the
|
|
||||||
current module.
|
|
||||||
3. Conversely, defining a symbol in the current module does _not_ shadow an
|
|
||||||
opened instance of that symbol.
|
|
||||||
|
|
||||||
As a consequence of 2 and 3, using a symbol that is both defined and opened
|
|
||||||
locally will result in an ambiguity error.
|
|
||||||
@ -1,166 +0,0 @@
|
|||||||
# Module system
|
|
||||||
|
|
||||||
## Defining a module
|
|
||||||
|
|
||||||
The `module` keyword starts the declaration of a module followed by its
|
|
||||||
name and body. The module declaration ends with the `end` keyword.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- ModuleName.juvix
|
|
||||||
module ModuleName;
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
A <u>Juvix project</u> 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 <u>module</u> of the same name. The name of the
|
|
||||||
module must coincide with the path of the its file relative to its
|
|
||||||
project's root directory. For example, if the file is
|
|
||||||
`root/Data/List.juvix` then the module must be called `Data.List`,
|
|
||||||
assuming `root` is the project's folder.
|
|
||||||
|
|
||||||
To check that Juvix is correctly detecting your project's root, one can
|
|
||||||
run the command `juvix dev 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.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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 <u>open</u> an imported module making available
|
|
||||||
all its names by their unqualified name.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
import Prelude;
|
|
||||||
open Prelude;
|
|
||||||
```
|
|
||||||
|
|
||||||
We simplify it by the expression:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Prelude;
|
|
||||||
```
|
|
||||||
|
|
||||||
The `hiding` keyword can be used within an `open-import` statement.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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 corresponding `open` statement. For example, the
|
|
||||||
module `C` typechecks after marking the import of `A` as `public` in
|
|
||||||
module `B`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- 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:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- B.juvix
|
|
||||||
module B;
|
|
||||||
open import A public;
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
@ -1,37 +0,0 @@
|
|||||||
# Juvix project
|
|
||||||
|
|
||||||
A _juvix project_ is a collection of juvix modules plus some extra metadata
|
|
||||||
gathered in a `juvix.yaml` file. The most convenient way to create a juvix
|
|
||||||
project is to run the command `juvix init`.
|
|
||||||
|
|
||||||
A project is rooted in a directory. The root is set by creating a `juvix.yaml`,
|
|
||||||
which contains the following fields:
|
|
||||||
|
|
||||||
1. **name**: The name of the project. The name must not be empty and cannot
|
|
||||||
exceed 100 characters. Lower case letters, digits and hyphen `-` are
|
|
||||||
acceptable characters. The first letter must not be a hyphen. Summarizing, it
|
|
||||||
must match the following regexp: `[a-z0-9][a-z0-9-]{0,99}`.
|
|
||||||
2. **version** (_optional_): The version of the project. It must follow the
|
|
||||||
[SemVer](https://semver.org/) specification. If ommited the version will be
|
|
||||||
assumed to be _0.0.0_.
|
|
||||||
3. **dependencies** (_optional_): The dependencies of the project given as a
|
|
||||||
list. Each dependency is given as relative (or absolute) path to the root of
|
|
||||||
another juvix project. If the field is ommited, it will be assumed to contain
|
|
||||||
the juvix standard library as a dependency.
|
|
||||||
|
|
||||||
As intuition would tell, a juvix module belongs to a juvix project if it is
|
|
||||||
placed in the subtree hanging from the root directory. This rule has two
|
|
||||||
exceptions:
|
|
||||||
|
|
||||||
1. Modules in a hidden (or hanging from a hidden) directory are not part of the
|
|
||||||
project. E.g., if the root of a project is `dir`, then the module
|
|
||||||
`dir/.d/Lib.juvix` does not belong to the project rooted in `dir`.
|
|
||||||
1. A `juvix.yaml` file shadows other `juvix.yaml` files in parent
|
|
||||||
directories. E.g. if the root of a project is `dir` and the files
|
|
||||||
`dir/juvix.yaml` and `dir/nested/juvix.yaml` exist, then the module
|
|
||||||
`dir/nested/Lib.juvix` would belong to the project in `dir/nested`.
|
|
||||||
|
|
||||||
## Module naming convention
|
|
||||||
|
|
||||||
Modules that belong to a project must follow a naming convention.
|
|
||||||
See the documentation for [modules](modules.md).
|
|
||||||
@ -1,13 +0,0 @@
|
|||||||
# Statement
|
|
||||||
|
|
||||||
A juvix statement is each of the components of a module.
|
|
||||||
All statements are listed below:
|
|
||||||
|
|
||||||
1. [type definition](datatypes.md).
|
|
||||||
2. [function definition](functions.md).
|
|
||||||
3. [axiom definition](axioms.md).
|
|
||||||
4. [fixity declaration](infix.md).
|
|
||||||
5. [function definition](functions.md).
|
|
||||||
6. [open](modules.md).
|
|
||||||
7. [import](modules.md).
|
|
||||||
8. [local module](modules.md).
|
|
||||||
@ -1,2 +0,0 @@
|
|||||||
The [Juvix standard library](https://anoma.github.io/juvix-stdlib/)
|
|
||||||
contains common functions that can be used in Juvix programs.
|
|
||||||
@ -1,89 +0,0 @@
|
|||||||
# CLI
|
|
||||||
|
|
||||||
## Usage
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix [Global options] ((-v|--version) | (-h|--help) | COMPILER_CMD | UTILITY_CMD)
|
|
||||||
```
|
|
||||||
|
|
||||||
## Informative options
|
|
||||||
|
|
||||||
- `-v,--version` Print the version and exit
|
|
||||||
- `-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)
|
|
||||||
- `--no-termination` Disable termination checking
|
|
||||||
- `--no-positivity` Disable positivity checking for inductive types
|
|
||||||
- `--no-stdlib` Do not use the standard library
|
|
||||||
|
|
||||||
## Main Commands
|
|
||||||
|
|
||||||
- `html` Generate HTML output from a Juvix file
|
|
||||||
- `typecheck` Typecheck a Juvix file
|
|
||||||
- `compile` Compile a Juvix file
|
|
||||||
|
|
||||||
## Utility Commands
|
|
||||||
|
|
||||||
- `doctor` Perform checks on your Juvix development environment
|
|
||||||
- `init` Interactively initialize a Juvix project in the current
|
|
||||||
directory
|
|
||||||
|
|
||||||
## Dev Commands
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix dev COMMAND
|
|
||||||
```
|
|
||||||
|
|
||||||
- `parse` Parse a Juvix file
|
|
||||||
- `scope` Parse and scope a Juvix file
|
|
||||||
- `highlight` Highlight a Juvix file
|
|
||||||
- `core` Subcommands related to JuvixCore
|
|
||||||
- `asm` Subcommands related to JuvixAsm
|
|
||||||
- `root` Show the root path for a Juvix project
|
|
||||||
- `termination` Subcommands related to termination checking
|
|
||||||
- `internal` Subcommands related to Internal
|
|
||||||
- `minic` Translate a Juvix file to a subset of C
|
|
||||||
|
|
||||||
## 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`).
|
|
||||||
|
|
||||||
```shell
|
|
||||||
eval "$(juvix --bash-completion-script juvix)"
|
|
||||||
```
|
|
||||||
|
|
||||||
### Fish
|
|
||||||
|
|
||||||
Run the following command in your shell:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix --fish-completion-script juvix
|
|
||||||
> ~/.config/fish/completions/juvix.fish
|
|
||||||
```
|
|
||||||
|
|
||||||
### ZSH
|
|
||||||
|
|
||||||
Run the following command in your shell:
|
|
||||||
|
|
||||||
```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](https://zsh.sourceforge.io/Doc/Release/Functions.html) (which
|
|
||||||
you can inspect by running `echo $FPATH` in the shell).
|
|
||||||
@ -1,4 +0,0 @@
|
|||||||
- [Command line Interface](./CLI.md)
|
|
||||||
- [Emacs Mode](./emacs.md)
|
|
||||||
- [Test Suite](./testing.md)
|
|
||||||
- [Doctor](./doctor.md)
|
|
||||||
@ -1,123 +0,0 @@
|
|||||||
# 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](https://clang.llvm.org)
|
|
||||||
version 13 or later to generate binaries. You need to have Clang
|
|
||||||
available on your system `$PATH`.
|
|
||||||
|
|
||||||
Recommended installation method:
|
|
||||||
|
|
||||||
### MacOS
|
|
||||||
|
|
||||||
Use [Homebrew](https://brew.sh):
|
|
||||||
|
|
||||||
```shell
|
|
||||||
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
|
|
||||||
|
|
||||||
```shell
|
|
||||||
sudo apt install clang lldb lld
|
|
||||||
```
|
|
||||||
|
|
||||||
### Arch Linux
|
|
||||||
|
|
||||||
```shell
|
|
||||||
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.
|
|
||||||
|
|
||||||
Recommended installation method:
|
|
||||||
|
|
||||||
### MacOS
|
|
||||||
|
|
||||||
`wasm-ld` is included in the [Homebrew](https://brew.sh) llvm
|
|
||||||
distribution:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
brew install llvm
|
|
||||||
```
|
|
||||||
|
|
||||||
### Debian / Ubuntu Linux
|
|
||||||
|
|
||||||
```shell
|
|
||||||
sudo apt install lldb lld
|
|
||||||
```
|
|
||||||
|
|
||||||
### Arch Linux
|
|
||||||
|
|
||||||
```shell
|
|
||||||
sudo pacman -S lld
|
|
||||||
```
|
|
||||||
|
|
||||||
## Newer Clang version required
|
|
||||||
|
|
||||||
Juvix requires Clang version 13 or above. See the documentation on
|
|
||||||
[installing Clang](./doctor.md#could-not-find-the-clang-command).
|
|
||||||
|
|
||||||
## Clang does not support the wasm32 target
|
|
||||||
|
|
||||||
Juvix requires Clang version 13 or above. See the documentation on
|
|
||||||
[installing Clang](./doctor.md#could-not-find-the-clang-command).
|
|
||||||
|
|
||||||
## Clang does not support the wasm32-wasi target
|
|
||||||
|
|
||||||
Juvix uses [WASI - The Wasm System Interface](https://wasi.dev) 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](https://github.com/WebAssembly/wasi-sdk/releases).
|
|
||||||
|
|
||||||
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](https://github.com/WebAssembly/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](https://github.com/WebAssembly/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](./doctor.md#download-the-wasi-sysroot-and-set-wasi_sysroot_path).
|
|
||||||
|
|
||||||
## Could not find the wasmer command
|
|
||||||
|
|
||||||
The Juvix test suite uses [Wasmer](https://wasmer.io) as a Wasm runtime
|
|
||||||
to execute compiled Wasm binaries. See [the Wasmer
|
|
||||||
documentation](https://docs.wasmer.io/ecosystem/wasmer/getting-started)
|
|
||||||
to see how to install it.
|
|
||||||
@ -1,52 +0,0 @@
|
|||||||
## Emacs Mode
|
|
||||||
|
|
||||||
There is an Emacs mode available for Juvix. Currently, it supports
|
|
||||||
syntax highlighting for well-scoped modules.
|
|
||||||
|
|
||||||
To get started, clone the Juvix Emacs mode repository:
|
|
||||||
|
|
||||||
```bash
|
|
||||||
git clone https://github.com/anoma/juvix-mode.git
|
|
||||||
```
|
|
||||||
|
|
||||||
To install it add the following lines to your Emacs configuration file:
|
|
||||||
|
|
||||||
```elisp
|
|
||||||
(push "/path/to/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 |
|
|
||||||
| `M-.` | `juvix-goto-definition` | Go to the definition of symbol at point |
|
|
||||||
| `C-c C-f` | `juvix-format-buffer` | Format the current buffer |
|
|
||||||
|
|
||||||
### Emacs installation
|
|
||||||
|
|
||||||
Most Linux distributions contain an Emacs package which can be installed
|
|
||||||
with your package manager (`sudo apt install emacs` on Ubuntu). On
|
|
||||||
macOS, it is recommended to install Emacs Plus via Homebrew:
|
|
||||||
`brew install emacs-plus`. Using the Emacs Homebrew casks is not
|
|
||||||
recommended.
|
|
||||||
|
|
||||||
### Common problems
|
|
||||||
|
|
||||||
- Error "Symbol's value as variable is void: sh:1:"
|
|
||||||
|
|
||||||
Make sure the juvix executable is on the Emacs' `exec-path`. Note
|
|
||||||
that `exec-path` may be different from your shell's `PATH`. This is
|
|
||||||
particularly common on macOS with Emacs launched from GUI instead of
|
|
||||||
the terminal.
|
|
||||||
|
|
||||||
The easiest way to resolve this issue is to install the
|
|
||||||
[exec-path-from-shell](https://github.com/purcell/exec-path-from-shell)
|
|
||||||
package (available on MELPA). Alternatively, one may set `exec-path`
|
|
||||||
to match shell `PATH` by following the instructions from
|
|
||||||
[EmacsWiki](https://www.emacswiki.org/emacs/ExecPath).
|
|
||||||
@ -1,20 +0,0 @@
|
|||||||
# Testing
|
|
||||||
|
|
||||||
### Dependencies
|
|
||||||
|
|
||||||
See [Installing dependencies](./doctor.html) for instructions on how to
|
|
||||||
setup the testing environment for the WASM compiler tests.
|
|
||||||
|
|
||||||
### Running
|
|
||||||
|
|
||||||
Run tests using:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
stack test
|
|
||||||
```
|
|
||||||
|
|
||||||
To run tests, ignoring all the WASM tests:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
stack test --ta '-p "! /slow tests/"'
|
|
||||||
```
|
|
||||||
@ -1 +0,0 @@
|
|||||||
- [NodeJS Interop](./nodejs-interop.md)
|
|
||||||
@ -1,79 +0,0 @@
|
|||||||
# Juvix Emacs mode tutorial
|
|
||||||
|
|
||||||
First, follow the instructions in the [Emacs Mode
|
|
||||||
Reference](../reference/tooling/emacs.md) to install the Juvix Emacs
|
|
||||||
mode. Once you've successfully set it up, create a file `Hello.juvix`
|
|
||||||
with the following content.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := printStringLn "Hello world!";
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
Type `C-c C-l` to run the scoper and highlight the syntax.
|
|
||||||
|
|
||||||
If you make a mistake in your program, it is automatically underlined in
|
|
||||||
red with the error message popping up when you hover the mouse pointer
|
|
||||||
over the underlined part.
|
|
||||||
|
|
||||||
For example, in the following program the identifier `printStringLna`
|
|
||||||
should be underlined with the error message "Symbol not in scope".
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := printStringLna "Hello world!";
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
If error underlining doesn't work, make sure you have the `flycheck`
|
|
||||||
mode turned on. It should be turned on automatically when loading
|
|
||||||
`juvix-mode`, but in case this doesn't work you can enable it with
|
|
||||||
`M-x flycheck-mode`.
|
|
||||||
|
|
||||||
Let's extend our program with another definition.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
print : IO;
|
|
||||||
print := printStringLn "Hello world!";
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := print;
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
Place the cursor on the `print` call in the function clause of `main`
|
|
||||||
and press `M-.`. The cursor will jump to the definition of `print`
|
|
||||||
above. This also works across files and for definitions from the
|
|
||||||
standard library. You can try using `M-.` to jump to the definition of
|
|
||||||
`printStringLn`.
|
|
||||||
|
|
||||||
One more feature of the Juvix Emacs mode is code formatting. To format
|
|
||||||
the content of the current buffer, type `C-c C-f`. Here is the result.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Hello;
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
print : IO;
|
|
||||||
print := printStringLn "Hello world!";
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := print;
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
@ -1,805 +0,0 @@
|
|||||||
# Juvix tutorial
|
|
||||||
|
|
||||||
- [Juvix REPL](./learn.md#juvix-repl)
|
|
||||||
- [Basic expressions](./learn.md#basic-expressions)
|
|
||||||
- [Files, modules and
|
|
||||||
compilation](./learn.md#files-modules-and-compilation)
|
|
||||||
- [Data types and functions](./learn.md#data-types-and-functions)
|
|
||||||
- [Pattern matching](./learn.md#pattern-matching)
|
|
||||||
- [Comparisons and
|
|
||||||
conditionals](./learn.md#comparisons-and-conditionals)
|
|
||||||
- [Local definitions](./learn.md#local-definitions)
|
|
||||||
- [Recursion](./learn.md#recursion)
|
|
||||||
- [Partial application and higher-order
|
|
||||||
functions](./learn.md#partial-application-and-higher-order-functions)
|
|
||||||
- [Polymorphism](./learn.md#polymorphism)
|
|
||||||
- [Tail recursion](./learn.md#tail-recursion)
|
|
||||||
- [Totality checking](./learn.md#totality-checking)
|
|
||||||
- [Exercises](./learn.md#exercises)
|
|
||||||
|
|
||||||
## Juvix REPL
|
|
||||||
|
|
||||||
After [installing Juvix](../howto/installing.md), launch the Juvix REPL:
|
|
||||||
|
|
||||||
```shell
|
|
||||||
juvix repl
|
|
||||||
```
|
|
||||||
|
|
||||||
The response should be similar to:
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Juvix REPL version 0.3: https://juvix.org. Run :help for help
|
|
||||||
OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
|
|
||||||
Stdlib.Prelude>
|
|
||||||
```
|
|
||||||
|
|
||||||
Currently, the REPL supports evaluating expressions but it does not yet
|
|
||||||
support adding new definitions. To see the list of available REPL
|
|
||||||
commands type `:help`.
|
|
||||||
|
|
||||||
## Basic expressions
|
|
||||||
|
|
||||||
You can try evaluating simple arithmetic expressions in the REPL:
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> 3 + 4
|
|
||||||
7
|
|
||||||
Stdlib.Prelude> 1 + 3 * 7
|
|
||||||
22
|
|
||||||
Stdlib.Prelude> div 35 4
|
|
||||||
8
|
|
||||||
Stdlib.Prelude> mod 35 4
|
|
||||||
3
|
|
||||||
Stdlib.Prelude> sub 35 4
|
|
||||||
31
|
|
||||||
Stdlib.Prelude> sub 4 35
|
|
||||||
0
|
|
||||||
```
|
|
||||||
|
|
||||||
By default, Juvix operates on non-negative natural numbers. Natural number
|
|
||||||
subtraction is implemented by the function `sub`. Subtracting a bigger
|
|
||||||
natural number from a smaller one yields `0`.
|
|
||||||
|
|
||||||
You can also try boolean expressions
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> true
|
|
||||||
true
|
|
||||||
Stdlib.Prelude> not true
|
|
||||||
false
|
|
||||||
Stdlib.Prelude> true && false
|
|
||||||
false
|
|
||||||
Stdlib.Prelude> true || false
|
|
||||||
true
|
|
||||||
Stdlib.Prelude> if true 1 0
|
|
||||||
1
|
|
||||||
```
|
|
||||||
|
|
||||||
and strings, pairs and lists:
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> "Hello world!"
|
|
||||||
"Hello world!"
|
|
||||||
Stdlib.Prelude> (1, 2)
|
|
||||||
(1, 2)
|
|
||||||
Stdlib.Prelude> 1 :: 2 :: nil
|
|
||||||
1 :: 2 :: nil
|
|
||||||
```
|
|
||||||
|
|
||||||
In fact, you can use all functions and types from the
|
|
||||||
[Stdlib.Prelude](https://anoma.github.io/juvix-stdlib/Stdlib.Prelude.html)
|
|
||||||
module of the [standard library](https://anoma.github.io/juvix-stdlib),
|
|
||||||
which is preloaded by default.
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> length (1 :: 2 :: nil)
|
|
||||||
3
|
|
||||||
Stdlib.Prelude> null (1 :: 2 :: nil)
|
|
||||||
false
|
|
||||||
Stdlib.Prelude> swap (1, 2)
|
|
||||||
(2, 1)
|
|
||||||
```
|
|
||||||
|
|
||||||
## Files, modules and compilation
|
|
||||||
|
|
||||||
Currently, the REPL does not support adding new definitions. To define
|
|
||||||
new functions or data types, you need to put them in a separate file and
|
|
||||||
either load the file in the REPL with `:load file.juvix` or compile the
|
|
||||||
file to a binary executable with the shell command
|
|
||||||
`juvix compile file.juvix`.
|
|
||||||
|
|
||||||
To conveniently edit Juvix files, an [Emacs mode](./emacs.md) and a
|
|
||||||
[VSCode extension](./vscode.md) are available.
|
|
||||||
|
|
||||||
A Juvix file must declare a module whose name corresponds exactly to the
|
|
||||||
name of the file. For example, a file `Hello.juvix` must declare a
|
|
||||||
module `Hello`:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
-- Hello world example. This is a comment.
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
-- Import the standard library prelude, including the 'String' type
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : String;
|
|
||||||
main := "Hello world!";
|
|
||||||
```
|
|
||||||
|
|
||||||
A file compiled to an executable must define the zero-argument
|
|
||||||
function `main` which is evaluated when running the program. The
|
|
||||||
definition of `main` can have any non-function type, e.g., `String`,
|
|
||||||
`Bool` or `Nat`. The generated executable prints the result of
|
|
||||||
evaluating `main`.
|
|
||||||
|
|
||||||
## Data types and functions
|
|
||||||
|
|
||||||
To see the type of an expression, use the `:type` REPL command:
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> :type 1
|
|
||||||
Nat
|
|
||||||
Stdlib.Prelude> :type true
|
|
||||||
Bool
|
|
||||||
```
|
|
||||||
|
|
||||||
The types `Nat` and `Bool` are defined in the standard library.
|
|
||||||
|
|
||||||
The type `Bool` has two constructors `true` and `false`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Bool :=
|
|
||||||
| true : Bool
|
|
||||||
| false : Bool;
|
|
||||||
```
|
|
||||||
|
|
||||||
The constructors of a data type can be used to build elements of the
|
|
||||||
type. They can also appear as patterns in function definitions. For
|
|
||||||
example, the `not` function is defined in the standard library by:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
not : Bool -> Bool;
|
|
||||||
not true := false;
|
|
||||||
not false := true;
|
|
||||||
```
|
|
||||||
|
|
||||||
The first line is the _signature_ which specifies the type of the
|
|
||||||
definition. In this case, `not` is a function from `Bool` to `Bool`. The
|
|
||||||
signature is followed by two _function clauses_ which specify the
|
|
||||||
function result depending on the shape of the arguments. When a function
|
|
||||||
call is evaluated, the first clause that matches the arguments is used.
|
|
||||||
|
|
||||||
In contrast to languages like Python, Java or C/C++, Juvix doesn't
|
|
||||||
require parentheses for function calls. All the arguments are just
|
|
||||||
listed after the function. The general pattern for function application
|
|
||||||
is: `func arg1 arg2 arg3 ...`
|
|
||||||
|
|
||||||
A more complex example of a data type is the `Nat` type from the
|
|
||||||
standard library:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Nat :=
|
|
||||||
| zero : Nat
|
|
||||||
| suc : Nat -> Nat;
|
|
||||||
```
|
|
||||||
|
|
||||||
The constructor `zero` represents `0` and `suc` represents the successor
|
|
||||||
function – `suc n` is the successor of `n`, i.e., `n+1`. For example,
|
|
||||||
`suc zero` represents `1`. The number literals `0`, `1`, `2`, etc., are
|
|
||||||
just shorthands for appropriate expressions built using `suc` and
|
|
||||||
`zero`.
|
|
||||||
|
|
||||||
The constructors of a data type specify how the elements of the type can
|
|
||||||
be constructed. For instance, the above definition specifies that an
|
|
||||||
element of `Nat` is either:
|
|
||||||
|
|
||||||
- `zero`, or
|
|
||||||
- `suc n` where `n` is an element of `Nat`, i.e., it is constructed by
|
|
||||||
applying `suc` to appropriate arguments (in this case the argument
|
|
||||||
of `suc` has type `Nat`).
|
|
||||||
|
|
||||||
Any element of `Nat` can be built with the constructors in this way –
|
|
||||||
there are no other elements. Mathematically, this is an inductive
|
|
||||||
definition, which is why the data type is called _inductive_.
|
|
||||||
|
|
||||||
If implemented directly, the above unary representation of natural
|
|
||||||
numbers would be extremely inefficient. The Juvix compiler uses a binary
|
|
||||||
number representation under the hood and implements arithmetic
|
|
||||||
operations using corresponding machine instructions, so the performance
|
|
||||||
of natural number arithmetic is similar to other programming languages.
|
|
||||||
The `Nat` type is a high-level presentation of natural numbers as seen
|
|
||||||
by the user who does not need to worry about low-level arithmetic
|
|
||||||
implementation details.
|
|
||||||
|
|
||||||
One can use `zero` and `suc` in pattern matching, like any other
|
|
||||||
constructors:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
infixl 6 +;
|
|
||||||
+ : Nat -> Nat -> Nat;
|
|
||||||
+ zero b := b;
|
|
||||||
+ (suc a) b := suc (a + b);
|
|
||||||
```
|
|
||||||
|
|
||||||
The `infixl 6 +` declares `+` to be an infix left-associative operator
|
|
||||||
with priority 6. The `+` is an ordinary function, except that function
|
|
||||||
application for `+` is written in infix notation. The definitions of the
|
|
||||||
clauses of `+` still need the prefix notation on the left-hand sides.
|
|
||||||
|
|
||||||
The `a` and `b` in the patterns on the left-hand sides of the clauses
|
|
||||||
are _variables_ which match arbitrary values of the corresponding type.
|
|
||||||
They can be used on the right-hand side to refer to the values matched.
|
|
||||||
For example, when evaluating
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
(suc (suc zero)) + zero
|
|
||||||
```
|
|
||||||
|
|
||||||
the second clause of `+` matches, assigning `suc zero` to `a` and `zero`
|
|
||||||
to `b`. Then the right-hand side of the clause is evaluated with `a` and
|
|
||||||
`b` substituted by these values:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
suc (suc zero + zero)
|
|
||||||
```
|
|
||||||
|
|
||||||
Again, the second clause matches, now with both `a` and `b` being
|
|
||||||
`zero`. After replacing with the right-hand side, we obtain:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
suc (suc (zero + zero))
|
|
||||||
```
|
|
||||||
|
|
||||||
Now the first clause matches and finally we obtain the result
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
suc (suc zero)
|
|
||||||
```
|
|
||||||
|
|
||||||
which is just `2`.
|
|
||||||
|
|
||||||
The function `+` is defined like above in the standard library, but the
|
|
||||||
Juvix compiler treats it specially and generates efficient code using
|
|
||||||
appropriate CPU instructions.
|
|
||||||
|
|
||||||
## Pattern matching
|
|
||||||
|
|
||||||
The patterns in function clauses do not have to match on a single
|
|
||||||
constructor – they may be arbitrarily deep. For example, here is an
|
|
||||||
(inefficient) implementation of a function which checks whether a
|
|
||||||
natural number is even:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
even : Nat -> Bool;
|
|
||||||
even zero := true;
|
|
||||||
even (suc zero) := false;
|
|
||||||
even (suc (suc n)) := even n;
|
|
||||||
```
|
|
||||||
|
|
||||||
This definition states that a natural number `n` is even if either `n`
|
|
||||||
is `zero` or, recursively, `n-2` is even.
|
|
||||||
|
|
||||||
If a subpattern is to be ignored, then one can use a wildcard `_`
|
|
||||||
instead of naming the subpattern.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
isPositive : Nat -> Bool;
|
|
||||||
isPositive zero := false;
|
|
||||||
isPositive (suc _) := true;
|
|
||||||
```
|
|
||||||
|
|
||||||
The above function could also be written as:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
isPositive : Nat -> Bool;
|
|
||||||
isPositive zero := false;
|
|
||||||
isPositive _ := true;
|
|
||||||
```
|
|
||||||
|
|
||||||
It is not necessary to define a separate function to perform pattern
|
|
||||||
matching. One can use the `case` syntax to pattern match an expression
|
|
||||||
directly.
|
|
||||||
|
|
||||||
```jrepl
|
|
||||||
Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
|
|
||||||
1
|
|
||||||
```
|
|
||||||
|
|
||||||
## Comparisons and conditionals
|
|
||||||
|
|
||||||
To use the comparison operators on natural numbers, one needs to import
|
|
||||||
the `Stdlib.Data.Nat.Ord` module. The comparison operators are not in
|
|
||||||
`Stdlib.Prelude` to avoid clashes with user-defined operators for other
|
|
||||||
data types. The functions available in `Stdlib.Data.Nat.Org` include:
|
|
||||||
`<`, `<=`, `>`, `>=`, `==`, `/=`, `min`, `max`.
|
|
||||||
|
|
||||||
For example, one may define the function `max3` by:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Stdlib.Data.Nat.Ord;
|
|
||||||
|
|
||||||
max3 : Nat -> Nat -> Nat -> Nat;
|
|
||||||
max3 x y z := if (x > y) (max x z) (max y z);
|
|
||||||
```
|
|
||||||
|
|
||||||
The conditional `if` is a special function which is evaluated lazily,
|
|
||||||
i.e., first the condition (the first argument) is evaluated, and then
|
|
||||||
depending on its truth-value one of the branches (the second or the
|
|
||||||
third argument) is evaluated and returned.
|
|
||||||
|
|
||||||
By default, evaluation in Juvix is _eager_ (or _strict_), meaning that
|
|
||||||
the arguments to a function are fully evaluated before applying the
|
|
||||||
function. Only `if`, `||` and `&&` are treated specially and evaluated
|
|
||||||
lazily. These special functions cannot be partially applied (see
|
|
||||||
[Partial application and higher-order
|
|
||||||
functions](./learn.md#partial-application-and-higher-order-functions)
|
|
||||||
below).
|
|
||||||
|
|
||||||
## Local definitions
|
|
||||||
|
|
||||||
Juvix supports local definitions with let-expressions.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
f : Nat -> Nat;
|
|
||||||
f a := let x : Nat := a + 5;
|
|
||||||
y : Nat := a * 7 + x
|
|
||||||
in
|
|
||||||
x * y;
|
|
||||||
```
|
|
||||||
|
|
||||||
The variables `x` and `y` are not visible outside `f`.
|
|
||||||
|
|
||||||
One can also use multi-clause definitions in `let`-expressions, with the
|
|
||||||
same syntax as definitions inside a module. For example:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
even : Nat -> Bool;
|
|
||||||
even :=
|
|
||||||
let
|
|
||||||
even' : Nat -> Bool;
|
|
||||||
odd' : Nat -> Bool;
|
|
||||||
|
|
||||||
even' zero := true;
|
|
||||||
even' (suc n) := odd' n;
|
|
||||||
|
|
||||||
odd' zero := false;
|
|
||||||
odd' (suc n) := even' n;
|
|
||||||
in
|
|
||||||
even';
|
|
||||||
```
|
|
||||||
|
|
||||||
The functions `even'` and `odd'` are not visible outside `even`.
|
|
||||||
|
|
||||||
## Recursion
|
|
||||||
|
|
||||||
Juvix is a purely functional language, which means that functions have
|
|
||||||
no side effects and all variables are immutable. An advantage of
|
|
||||||
functional programming is that all expressions are _referentially
|
|
||||||
transparent_ – any expression can be replaced by its value without
|
|
||||||
changing the meaning of the program. This makes it easier to reason
|
|
||||||
about programs, in particular to prove their correctness. No errors
|
|
||||||
involving implicit state are possible, because the state is always
|
|
||||||
explicit.
|
|
||||||
|
|
||||||
In a functional language, there are no imperative loops. Repetition is
|
|
||||||
expressed using recursion. In many cases, the recursive definition of a
|
|
||||||
function follows the inductive definition of a data structure the
|
|
||||||
function analyses. For example, consider the following inductive type of
|
|
||||||
lists of natural numbers:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type NList :=
|
|
||||||
| nnil : NList
|
|
||||||
| ncons : Nat -> NList -> NList;
|
|
||||||
```
|
|
||||||
|
|
||||||
An element of `NList` is either `nnil` (empty) or `ncons x xs` where
|
|
||||||
`x : Nat` and `xs : NList` (a list with head `x` and tail `xs`).
|
|
||||||
|
|
||||||
A function computing the length of a list may be defined by:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
nlength : NList -> Nat;
|
|
||||||
nlength nnil := 0;
|
|
||||||
nlength (ncons _ xs) := nlength xs + 1;
|
|
||||||
```
|
|
||||||
|
|
||||||
The definition follows the inductive definition of `NList`. There are
|
|
||||||
two function clauses for the two constructors. The case for `nnil` is
|
|
||||||
easy – the constructor has no arguments and the length of the empty list
|
|
||||||
is `0`. For a constructor with some arguments, one typically needs to
|
|
||||||
express the result of the function in terms of the constructor
|
|
||||||
arguments, usually calling the function recursively on the constructor's
|
|
||||||
inductive arguments (for `ncons` this is the second argument). In the
|
|
||||||
case of `ncons _ xs`, we recursively call `nlength` on `xs` and add `1`
|
|
||||||
to the result.
|
|
||||||
|
|
||||||
Let's consider another example – a function which returns the maximum of
|
|
||||||
the numbers in a list or 0 for the empty list.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
open import Stdlib.Data.Nat.Ord; -- for `max`
|
|
||||||
|
|
||||||
nmaximum : NList -> Nat;
|
|
||||||
nmaximum nnil := 0;
|
|
||||||
nmaximum (ncons x xs) := max x (nmaximum xs);
|
|
||||||
```
|
|
||||||
|
|
||||||
Again, there is a clause for each constructor. In the case for `ncons`,
|
|
||||||
we recursively call the function on the list tail and take the maximum
|
|
||||||
of the result and the list head.
|
|
||||||
|
|
||||||
For an example of a constructor with more than one inductive argument,
|
|
||||||
consider binary trees with natural numbers in nodes.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Tree :=
|
|
||||||
| leaf : Nat -> Tree
|
|
||||||
| node : Nat -> Tree -> Tree -> Tree;
|
|
||||||
```
|
|
||||||
|
|
||||||
The constructor `node` has two inductive arguments (the second and the
|
|
||||||
third) which represent the left and the right subtree.
|
|
||||||
|
|
||||||
A function which produces the mirror image of a tree may be defined by:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
mirror : Tree -> Tree;
|
|
||||||
mirror (leaf x) := leaf x;
|
|
||||||
mirror (node x l r) := node x (mirror r) (mirror l);
|
|
||||||
```
|
|
||||||
|
|
||||||
The definition of `mirror` follows the definition of `Tree`. There are
|
|
||||||
two recursive calls for the two inductive constructors of `node` (the
|
|
||||||
subtrees).
|
|
||||||
|
|
||||||
## Partial application and higher-order functions
|
|
||||||
|
|
||||||
Strictly speaking, all Juvix functions have only one argument.
|
|
||||||
Multi-argument functions are really functions which return a function
|
|
||||||
which takes the next argument and returns a function taking another
|
|
||||||
argument, and so on for all arguments. The function type former `->`
|
|
||||||
(the arrow) is right-associative. Hence, the type, e.g.,
|
|
||||||
`Nat -> Nat -> Nat` when fully parenthesised becomes
|
|
||||||
`Nat -> (Nat -> Nat)`. It is the type of functions which given an
|
|
||||||
argument of type `Nat` return a function of type `Nat -> Nat` which
|
|
||||||
itself takes an argument of type `Nat` and produces a result of type
|
|
||||||
`Nat`. Function application is left-associative. For example, `f a b`
|
|
||||||
when fully parenthesised becomes `(f a) b`. So it is an application to
|
|
||||||
`b` of the function obtained by applying `f` to `a`.
|
|
||||||
|
|
||||||
Since a multi-argument function is just a one-argument function
|
|
||||||
returning a function, it can be _partially applied_ to a smaller number
|
|
||||||
of arguments than specified in its definition. The result is an
|
|
||||||
appropriate function. For example, `sub 10` is a function which
|
|
||||||
subtracts its argument from `10`, and `(+) 1` is a function which adds
|
|
||||||
`1` to its argument. If the function has been declared as an infix
|
|
||||||
operator (like `+`), then for partial application one needs to enclose
|
|
||||||
it in parentheses.
|
|
||||||
|
|
||||||
A function which takes a function as an argument is a _higher-order
|
|
||||||
function_. An example is the `nmap` function which applies a given
|
|
||||||
function to each element in a list of natural numbers.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
nmap : (Nat -> Nat) -> NList -> NList;
|
|
||||||
nmap _ nnil := nnil;
|
|
||||||
nmap f (ncons x xs) := ncons (f x) (nmap f xs);
|
|
||||||
```
|
|
||||||
|
|
||||||
The application
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
nmap \{ x := div x 2 } lst
|
|
||||||
```
|
|
||||||
|
|
||||||
divides every element of `lst` by `2`, rounding down the result. The
|
|
||||||
expression
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
\{ x := div x 2 }
|
|
||||||
```
|
|
||||||
|
|
||||||
is an unnamed function, or a _lambda_, which divides its argument by
|
|
||||||
`2`.
|
|
||||||
|
|
||||||
## Polymorphism
|
|
||||||
|
|
||||||
The type `NList` we have been working with above requires the list
|
|
||||||
elements to be natural numbers. It is possible to define lists
|
|
||||||
_polymorphically_, parameterising them by the element type. This is
|
|
||||||
similar to generics in languages like Java, C++ or Rust. Here is the
|
|
||||||
polymorphic definition of lists from the standard library:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
infixr 5 ::;
|
|
||||||
type List (A : Type) :=
|
|
||||||
| nil : List A
|
|
||||||
| :: : A -> List A -> List A;
|
|
||||||
```
|
|
||||||
|
|
||||||
The constructor `::` is declared as a right-associative infix operator
|
|
||||||
with priority 5. The definition has a parameter `A` which is the element
|
|
||||||
type.
|
|
||||||
|
|
||||||
Now one can define the `map` function polymorphically:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
map : {A B : Type} -> (A -> B) -> List A -> List B;
|
|
||||||
map f nil := nil;
|
|
||||||
map f (h :: hs) := f h :: map f hs;
|
|
||||||
```
|
|
||||||
|
|
||||||
This function has two _implicit type arguments_ `A` and `B`. These
|
|
||||||
arguments are normally omitted in function application – they are
|
|
||||||
inferred automatically during type checking. The curly braces indicate
|
|
||||||
that the argument is implicit and should be inferred.
|
|
||||||
|
|
||||||
In fact, the constructors `nil` and `::` also have an implicit argument:
|
|
||||||
the type of list elements. All type parameters of a data type definition
|
|
||||||
become implicit arguments of the constructors.
|
|
||||||
|
|
||||||
Usually, the implicit arguments in a function application can be
|
|
||||||
inferred. However, sometimes this is not possible and then the implicit
|
|
||||||
arguments need to be provided explicitly by enclosing them in braces:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
f {implArg1} .. {implArgK} arg1 .. argN
|
|
||||||
```
|
|
||||||
|
|
||||||
For example, `nil {Nat}` has type `List Nat` while `nil` by itself has
|
|
||||||
type `{A : Type} -> List A`.
|
|
||||||
|
|
||||||
## Tail recursion
|
|
||||||
|
|
||||||
Any recursive call whose result is further processed by the calling
|
|
||||||
function needs to create a new stack frame to save the calling function
|
|
||||||
environment. This means that each such call will use a constant amount
|
|
||||||
of memory. For example, a function `sum` implemented as follows will use
|
|
||||||
an additional amount of memory proportional to the length of the
|
|
||||||
processed list:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
sum : NList -> Nat;
|
|
||||||
sum nnil := 0;
|
|
||||||
sum (ncons x xs) := x + sum xs;
|
|
||||||
```
|
|
||||||
|
|
||||||
This is not acceptable if you care about performance. In an imperative
|
|
||||||
language, one would use a simple loop going over the list without any
|
|
||||||
memory allocation. In pseudocode:
|
|
||||||
|
|
||||||
```pascal
|
|
||||||
sum : Nat := 0;
|
|
||||||
|
|
||||||
while (lst /= nil) do
|
|
||||||
begin
|
|
||||||
sum := sum + head lst;
|
|
||||||
lst := tail lst;
|
|
||||||
end;
|
|
||||||
|
|
||||||
result := sum;
|
|
||||||
```
|
|
||||||
|
|
||||||
Fortunately, it is possible to rewrite this function to use _tail
|
|
||||||
recursion_. A recursive call is _tail recursive_ if its result is also
|
|
||||||
the result of the calling function, i.e., the calling function returns
|
|
||||||
immediately after it without further processing. The Juvix compiler
|
|
||||||
_guarantees_ that all tail calls will be eliminated, i.e., that they
|
|
||||||
will be compiled to simple jumps without extra memory allocation. In a
|
|
||||||
tail recursive call, instead of creating a new stack frame, the old one
|
|
||||||
is reused.
|
|
||||||
|
|
||||||
The following implementation of `sum` uses tail recursion.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
sum : NList -> Nat;
|
|
||||||
sum lst :=
|
|
||||||
let
|
|
||||||
go : Nat -> NList -> Nat;
|
|
||||||
go acc nnil := acc;
|
|
||||||
go acc (ncons x xs) := go (acc + x) xs;
|
|
||||||
in
|
|
||||||
go 0 lst;
|
|
||||||
```
|
|
||||||
|
|
||||||
The first argument of `go` is an _accumulator_ which holds the sum
|
|
||||||
computed so far. It is analogous to the `sum` variable in the imperative
|
|
||||||
loop above. The initial value of the accumulator is 0. The function `go`
|
|
||||||
uses only constant additional memory overall. The code generated for it
|
|
||||||
by the Juvix compiler is equivalent to an imperative loop.
|
|
||||||
|
|
||||||
Most imperative loops may be translated into tail recursive functional
|
|
||||||
programs by converting the locally modified variables into accumulators
|
|
||||||
and the loop condition into pattern matching. For example, here is an
|
|
||||||
imperative pseudocode for computing the nth Fibonacci number in linear
|
|
||||||
time. The variables `cur` and `next` hold the last two computed
|
|
||||||
Fibonacci numbers.
|
|
||||||
|
|
||||||
```pascal
|
|
||||||
cur : Nat := 0;
|
|
||||||
next : Nat := 1;
|
|
||||||
|
|
||||||
while (n /= 0) do
|
|
||||||
begin
|
|
||||||
tmp := next;
|
|
||||||
next := cur + next;
|
|
||||||
cur := tmp;
|
|
||||||
n := n - 1;
|
|
||||||
end;
|
|
||||||
|
|
||||||
result := cur;
|
|
||||||
```
|
|
||||||
|
|
||||||
An equivalent functional program is:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
fib : Nat -> Nat;
|
|
||||||
fib :=
|
|
||||||
let go : Nat -> Nat -> Nat -> Nat;
|
|
||||||
go cur _ zero := cur;
|
|
||||||
go cur next (suc n) := go next (cur + next) n;
|
|
||||||
in
|
|
||||||
go 0 1;
|
|
||||||
```
|
|
||||||
|
|
||||||
A naive definition of the Fibonacci function runs in exponential time:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
fib : Nat -> Nat;
|
|
||||||
fib zero := 0;
|
|
||||||
fib (suc zero) := 1;
|
|
||||||
fib (suc (suc n)) := fib n + fib (suc n);
|
|
||||||
```
|
|
||||||
|
|
||||||
Tail recursion is less useful when the function needs to allocate memory
|
|
||||||
anyway. For example, one could make the `map` function from the previous
|
|
||||||
section tail recursive, but the time and memory use would still be
|
|
||||||
proportional to the length of the input because of the need to allocate
|
|
||||||
the result list.
|
|
||||||
|
|
||||||
## Totality checking
|
|
||||||
|
|
||||||
By default, the Juvix compiler requires all functions to be total.
|
|
||||||
Totality consists of:
|
|
||||||
|
|
||||||
- [termination](../explanations/totality/termination.md),
|
|
||||||
- [coverage](../explanations/totality/coverage.md),
|
|
||||||
- [strict positivity](../explanations/totality/positive.md).
|
|
||||||
|
|
||||||
The termination check ensures that all functions are structurally
|
|
||||||
recursive, i.e., all recursive call are on structurally smaller values –
|
|
||||||
subpatterns of the matched pattern. For example, the termination checker
|
|
||||||
rejects the definition
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
fact : Nat -> Nat;
|
|
||||||
fact x := if (x == 0) 1 (x * fact (sub x 1));
|
|
||||||
```
|
|
||||||
|
|
||||||
because the recursive call is not on a subpattern of a pattern matched
|
|
||||||
on in the clause. One can reformulate this definition so that it is
|
|
||||||
accepted by the termination checker:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
fact : Nat -> Nat;
|
|
||||||
fact zero := 1;
|
|
||||||
fact x@(suc n) := x * fact n;
|
|
||||||
```
|
|
||||||
|
|
||||||
Sometimes, such a reformulation is not possible. Then one can use the
|
|
||||||
`terminating` keyword to forgoe the termination check.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
terminating
|
|
||||||
log2 : Nat -> Nat;
|
|
||||||
log2 n := if (n <= 1) 0 (suc (log2 (div n 2)));
|
|
||||||
```
|
|
||||||
|
|
||||||
Coverage checking ensures that there are no unhandled patterns in
|
|
||||||
function clauses or `case` expressions. For example, the following
|
|
||||||
definition is rejected because the case `suc zero` is not handled:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
even : Nat -> Bool;
|
|
||||||
even zero := true;
|
|
||||||
even (suc (suc n)) := even n;
|
|
||||||
```
|
|
||||||
|
|
||||||
Since coverage checking forces the user to specify the function for all input values, it may be unclear how to implement functions which are typically partial. For example, the `tail` function on lists is often left undefined for the empty list. One solution is to return a default value. In the Juvix standard library, `tail` is implemented as follows, returning the empty list when the argument is empty.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
tail : {A : Type} -> List A -> List A;
|
|
||||||
tail (_ :: xs) := xs;
|
|
||||||
tail nil := nil;
|
|
||||||
```
|
|
||||||
|
|
||||||
Another solution is to wrap the result in the `Maybe` type from the standard library, which allows to represent optional values. An element of `Maybe A` is either `nothing` or `just x` with `x : A`.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Maybe (A : Type) :=
|
|
||||||
| nothing : Maybe A
|
|
||||||
| just : A -> Maybe A;
|
|
||||||
```
|
|
||||||
|
|
||||||
For example, one could define the tail function as:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
tail' : {A : Type} -> List A -> Maybe (List A)
|
|
||||||
tail' (_ :: xs) := just xs;
|
|
||||||
tail' nil := nothing;
|
|
||||||
```
|
|
||||||
|
|
||||||
Then the user needs to explicitly check if the result of the function contains a value or not:
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
case tail' lst
|
|
||||||
| just x := ...
|
|
||||||
| nothing := ...
|
|
||||||
```
|
|
||||||
|
|
||||||
## Exercises
|
|
||||||
|
|
||||||
You have now learnt the very basics of Juvix. To consolidate your
|
|
||||||
understanding of Juvix and functional programming, try doing some of
|
|
||||||
the following exercises. To learn how to write more complex Juvix
|
|
||||||
programs, see the
|
|
||||||
[advanced tutorial](./../examples/html/Tutorial/Tutorial.html)
|
|
||||||
and the [Juvix program examples](../reference/examples.md).
|
|
||||||
|
|
||||||
1. Define a function `prime : Nat -> Nat` which checks if a given
|
|
||||||
natural number is prime.
|
|
||||||
|
|
||||||
2. What is wrong with the following definition?
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
half : Nat -> Nat;
|
|
||||||
half n := if (n < 2) 0 (half (n - 2) + 1);
|
|
||||||
```
|
|
||||||
|
|
||||||
How can you reformulate this definition so that it is accepted by
|
|
||||||
Juvix?
|
|
||||||
|
|
||||||
3. Define a polymorphic function which computes the last element of a
|
|
||||||
list. What is the result of your function on the empty list?
|
|
||||||
|
|
||||||
4. A _suffix_ of a list `l` is any list which can be obtained from `l`
|
|
||||||
by removing some initial elements. For example, the suffixes of
|
|
||||||
`1 :: 2 :: 3 :: nil` are: `1 :: 2 :: 3 :: nil`, `2 :: 3 :: nil`,
|
|
||||||
`3 :: nil` and `nil`.
|
|
||||||
|
|
||||||
Define a function which computes the list of all suffixes of a given
|
|
||||||
list in the order of decreasing length.
|
|
||||||
|
|
||||||
5. Recall the `Tree` type from above.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
type Tree :=
|
|
||||||
| leaf : Nat -> Tree
|
|
||||||
| node : Nat -> Tree -> Tree -> Tree;
|
|
||||||
```
|
|
||||||
|
|
||||||
Analogously to the `map` function for lists, define a function
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
tmap : (Nat -> Nat) -> Tree -> Tree;
|
|
||||||
```
|
|
||||||
|
|
||||||
which applies a function to all natural numbers stored in a tree.
|
|
||||||
|
|
||||||
6. Make the `Tree` type polymorphic in the element type and repeat the
|
|
||||||
previous exercise.
|
|
||||||
|
|
||||||
7. Write a tail recursive function which reverses a list.
|
|
||||||
|
|
||||||
8. Write a tail recursive function which computes the factorial of a
|
|
||||||
natural number.
|
|
||||||
|
|
||||||
9. Define a function `comp : {A : Type} -> List (A -> A) -> A -> A`
|
|
||||||
which composes all functions in a list. For example,
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
comp (suc :: (*) 2 :: \{x := sub x 1} :: nil)
|
|
||||||
```
|
|
||||||
|
|
||||||
should be a function which given `x` computes `2(x - 1) + 1`.
|
|
||||||
@ -1,101 +0,0 @@
|
|||||||
# 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 -t wasm -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!
|
|
||||||
@ -1,40 +0,0 @@
|
|||||||
# Juvix VSCode extension tutorial
|
|
||||||
|
|
||||||
To install the [Juvix VSCode extension][vscode-marketplace], click on the "Extensions" button
|
|
||||||
in the left panel and search for the "Juvix" extension by Heliax.
|
|
||||||
|
|
||||||
Once you've installed the Juvix extension, you can open a Juvix file.
|
|
||||||
For example, create a `Hello.juvix` file with the following content.
|
|
||||||
|
|
||||||
```juvix
|
|
||||||
module Hello;
|
|
||||||
|
|
||||||
open import Stdlib.Prelude;
|
|
||||||
|
|
||||||
main : IO;
|
|
||||||
main := printStringLn "Hello world!";
|
|
||||||
|
|
||||||
end;
|
|
||||||
```
|
|
||||||
|
|
||||||
Syntax should be automatically highlighted for any file with `.juvix`
|
|
||||||
extension. You can jump to the definition of an identifier by pressing
|
|
||||||
F12 or control-clicking it. To apply the Juvix code formatter to the
|
|
||||||
current file, use Shift+Ctrl+I.
|
|
||||||
|
|
||||||
In the top right-hand corner of the editor window you should see several
|
|
||||||
buttons. Hover the mouse pointer over a button to see its description.
|
|
||||||
The functions of the buttons are as follows.
|
|
||||||
|
|
||||||
- Load file in REPL (Shift+Alt+R). Launches the Juvix REPL in a
|
|
||||||
separate window and loads the current file into it. You can then
|
|
||||||
evaluate any definition from the loaded file.
|
|
||||||
- Typecheck (Shift+Alt+T). Type-checks the current file.
|
|
||||||
- Compile (Shift+Alt+C). Compiles the current file. The resulting
|
|
||||||
native executable will be left in the directory of the file.
|
|
||||||
- Run (Shift+Alt+X). Compiles and runs the current file. The output of
|
|
||||||
the executable run is displayed in a separate window.
|
|
||||||
- Html preview. Generates HTML documentation for the current file and
|
|
||||||
displays it in a separate window.
|
|
||||||
|
|
||||||
[vscode-marketplace]: https://marketplace.visualstudio.com/items?itemName=heliax.juvix-mode
|
|
||||||
Loading…
Reference in New Issue
Block a user