#testing #completion #command-line-tool #language #stable #implementation

bin+lib minitt

Mini-TT, a dependently-typed lambda calculus, extended and (re)implemented in Rust

40 releases (4 breaking)

✓ Uses Rust 2018 edition

0.4.1 Sep 13, 2019
0.3.12 Sep 5, 2019
0.3.9 Apr 26, 2019
0.3.1 Mar 29, 2019

#24 in Development tools

Download history 71/week @ 2019-05-31 105/week @ 2019-06-07 6/week @ 2019-06-14 450/week @ 2019-06-21 70/week @ 2019-06-28 140/week @ 2019-07-05 44/week @ 2019-07-12 44/week @ 2019-07-19 26/week @ 2019-07-26 83/week @ 2019-08-02 70/week @ 2019-08-09 436/week @ 2019-08-23 70/week @ 2019-08-30 222/week @ 2019-09-06

567 downloads per month


2.5K SLoC


Crates.io Crates.io Crates.io docs.rs Build status CircleCI dependency status

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 stable Rust (version 1.37.0), 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 naming to avoid confusion. 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.

Notice: the development of this POC language has been moved to another redesigned programming language, Voile. We have a new type theory, better surface syntax, better error messages, richer type-checker. Everything is (or will become) better in Voile.

A dependently-typed program in samples:

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


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

Want to use minitt as a library? Add this to your Cargo.toml (if you don't even need a parser, you can remove the features completely):

minitt = { version = "0.3.12", features = ["parser"] }



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


~19K SLoC