minitt 0.1.6

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.

A program dependent types in samples:

let bool: U = sum { True 1 | False 1 };
let unit: U = sum { TT 1 };
-- A 2 type and a 1 type

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

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

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

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
    • Fix recursive data type definition scoping problem
    • 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
    • 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
  • 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)