minitt-rs
Rust implementation of Mini-TT, a simple dependently-typed lambda calculus. This implementation includes a type-checker (extended the origin), an AST pretty-printer and a command line tool which can be used as a file checker and an interactive REPL with completion and type inference. Built with latest (when developing this) stable Rust, 2018 edition. It can be used as a core language for complicated dependently-typed programming languages, or used for testing the correctness of translation algorithms.
I'm trying my best to use complete and meaningful namings. I'm also doing a general clean-up of the Haskell implementation and comment the functions with their counterparts' names in the Haskell implementation so people don't get confused when they read the paper while reading this implementation.
A dependently-typed program in samples:
const bool = sum { True | False };
const unit = sum { TT };
-- A 2 type and a 1 type
let return_type: bool -> U = split
{ True => unit
| False => 1
};
-- By `function.minitt` of course I mean dependent functions :)
let function: \Pi b: bool. return_type b = split
{ True => TT
| False => 0
};
-- Return things that are of different types.
We can have functions returning values of different types, while it's still statically-typed. Very flexible.
Resources
- Mini-TT Paper
- Code Samples, tested on CI
- Doc.rs documentation
- Change Log
- REPL Example
- Windows binary download by AppVeyor
Features
- Everything that the Haskell implementation has
- Parser as a cargo feature (using pest)
- AST pretty-printer as a cargo feature
- Improvements to the original implementation
- Use
BTreeMap
for branch/case tree so we become flexible on case order - Use
Vec
for telescope/declaration instead of functional immutable list
- Use
- New feature apart from trivial improvements
- Infer type of a pair
- Infer type of a constructor call
- Infer type of a case-split
- Module system (or even a very simple one)
- (Typed-)Holes?
- For completion / context lookup
- For type-directed development
-
const
declarations, where the type is inferred - Prefixing declarations with parameters, like
let a (b: c): d = f b;
- An executable for CLI usages (
minittc
) (using clap)- File checker
- Completion script generation
- Get the script:
minittc completion zsh/bash/powershell/fish/elvish
- Get the script:
- REPL (a fancy one based on rustyline and a plain
one based on stdio)
- Load file
- Infer (and normalize) type
- Eval (and normalize) expressions (may panic if ill-typed)
- Add single declaration
- Show context/gamma
- Help
- Completion
- Commands
- Files
- In-scope variables
- Language server (?)
- Publish?
- By
cargo install --path . --bin minittc --all-features
- By AppVeyor (Just find the configuration fits you best and get the artifact)
- By