minitt 0.1.5

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

minitt-rs

Crates.io Crates.io Crates.io docs.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.

Resources

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)