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.39.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.
The most recommended way of installation is to download the prebuilt binaries from GitHub Actions page. Here's how to find them.
You may also install from source:
$ 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.4.2", features = ["parser"] }
BTreeMap
for branch/case tree so we become flexible on case orderVec
for telescope/declaration instead of functional immutable listconst
declarations, where the type is inferredlet a (b: c): d = f b;
minittc
) (using clap)
minittc completion zsh/bash/powershell/fish/elvish
cargo install --path . --bin minittc --all-features