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
• Windows binary download by AppVeyor

Install

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

• 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