voile-rs

Voile is a dependently-typed programming language with a non-dependent version of row-polymorphism, meta variable resolution and implicit parameter syntax. For language description, please head to the docs.rs page.

Voile is the language after minitt, and the next language after Voile is Narc.

Resources

• Docs.rs documentation, including KaTeX-rendered typing rules
• Change Log, useful resource for tracking language evolution
• IntelliJ Plugin, which can export your code as clickable HTML
• Code Examples, which also acts as integration test suites
• Utilities Library, a rust crate extracted from Voile's implementation with some util codes
• Binary Download on GitHub Actions page for Windows, Ubuntu and macOS

The most good-looking example is this one.

Install

The most recommended way of installation is to download the prebuilt binaries from GitHub Actions page. Here's how to find them.

You can install the voile type-checker by this command (cargo installation and rust stable toolchain are assumed):

cargo install voile --bin voilec

After installation, you can type-check a voile file by:

voilec [filename]

You can also start a REPL:

voilec -i

Progress

• [X] Basic dependent type (minitt-rs things)
• [X] Universe level support
• [X] Row-types and kinds
• [X] Record constructor
• [X] Record projection
• [X] Variant constructor
• [X] Variant eliminator (case-split)
• [X] Implicit arguments