28 releases

0.2.6 Sep 21, 2020
0.2.5 Nov 26, 2019
0.2.4 Oct 23, 2019
0.0.14 Jul 11, 2019
0.0.1 Mar 30, 2019

#236 in Programming languages

46 downloads per month



Rust 4K SLoC // 0.2% comments Pest 449 SLoC // 0.1% comments Perl 64 SLoC Shell 6 SLoC // 0.2% comments Batch 3 SLoC


Crates.io Crates.io Crates.io docs.rs Actions Status dep-svg

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.


  • 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.


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


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


~71K SLoC