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:

```haskell -- A 2 type and a 1 type const bool = Sum { True | False }; const unit = Sum { TT };

-- By function.minitt of course I mean dependent functions :) let return_type: bool -> Type = split { True => unit | False => 1 };

-- Return things that are of different types. let function: \Pi b: bool. return_type b = split { True => TT | False => 0 }; ```

We can have functions returning values of different types, while it's still statically-typed. Very flexible.

Install

bash $ cargo install minitt --bin minittc --all-features --force

Resources

• Mini-TT Paper
• Code Samples, tested on CI
• Doc.rs documentation (a tutorial is included)
• Change Log
• REPL Example
• Windows binary download by AppVeyor
• IntelliJ Plugin

Features

• [X] Everything that the Haskell implementation has
• [X] Parser as a cargo feature (using pest)
• [X] AST pretty-printer as a cargo feature
• Improvements to the original implementation
  • [X] Use BTreeMap for branch/case tree so we become flexible on case order
  • [ ] Use Vec for telescope/declaration instead of functional immutable list
• New feature apart from trivial improvements
  • [X] 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
  • [X] const declarations, where the type is inferred
  • [X] Prefixing declarations with parameters, like let a (b: c): d = f b;
• An executable for CLI usages (minittc) (using clap)
  • [X] File checker
  • [X] Completion script generation
  • Get the script: minittc completion zsh/bash/powershell/fish/elvish
  • REPL (a fancy one based on rustyline and a plain one based on stdio)
  • [X] Load file
  • [X] Infer (and normalize) type
  • [X] Eval (and normalize) expressions (may panic if ill-typed)
  • [X] Add single declaration
  • [X] Show context/gamma
  • [X] Help
  • [X] Completion
    • [X] Commands
    • [X] 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)