minitt 0.1.4

Mini-TT, a dependently-typed lambda calculus, implementated in Rust

minitt-rs Build status CircleCI

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.



  • 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
    • Support inferring type of a pair
    • Module system (or even a very simple one)
  • An executable for CLI usages
    • File checker
    • REPL
    • Language server