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