minitt-rs

Rust implementation of Mini-TT, a simple dependently-typed lambda calculus. 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.

Resources

• Mini-TT Paper
• Code samples, tested on CI
• Doc.rs documentation
• Windows binary download by AppVeyor

Features

• Everything that the Haskell implementation has
• Parser as a cargo feature
• 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 instead of functional immutable list
• New feature apart from trivial improvements
  • Infer type of a pair
  • Module system (or even a very simple one)
  • (Typed-)Holes?
    • For completion / context lookup
    • For type-directed development
• An executable for CLI usages (minittc)
  • File checker
  • Completion script generation
    • Get the script: minittc completion zsh/bash/powershell/fish/elvish
    • Thanks to clap!
  • REPL
  • Language server
  • Publish?
    • By cargo install --path . --bin minittc --all-features
    • By AppVeyor (Just find the configuration fits you best and get the artifact)