#language #page #programming #head

bin+lib voile

Voile, a dependently-typed row-polymorphic programming language

27 releases

✓ Uses Rust 2018 edition

0.2.5 Nov 26, 2019
0.2.2 Sep 21, 2019
0.0.14 Jul 11, 2019
0.0.1 Mar 30, 2019

#77 in Development tools

Download history 31/week @ 2019-11-30 496/week @ 2019-12-07 1/week @ 2019-12-14 30/week @ 2019-12-28 6/week @ 2020-01-04 252/week @ 2020-01-11 149/week @ 2020-01-18 2/week @ 2020-01-25 1/week @ 2020-02-01 31/week @ 2020-02-08 5/week @ 2020-02-15 121/week @ 2020-02-22 1/week @ 2020-02-29 60/week @ 2020-03-07 34/week @ 2020-03-14

371 downloads per month


4.5K 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


~53K SLoC