voile-rs

![cc-svg] ![av-svg] ![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.

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):

bash cargo install voile --bin voilec

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

bash voilec [filename]

You can also start a REPL:

bash 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