minitt 0.2.4

Mini-TT, a dependently-typed lambda calculus, extended and implementated in Rust
# minitt-rs

[![Build status][av-svg]][av-url]
[![dependency status][dep-svg]][dep-rs]


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 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 dependently-typed program in [samples](./samples/dependent/function.minitt):

const bool = sum { True | False };
const unit = sum { TT };
-- 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
 | 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.

## Install

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

## Resources


+ [Mini-TT Paper](
+ [Code Samples](./samples), tested on CI
+ [][doc-rs] documentation (a tutorial is included)
+ [Change Log](
+ [REPL Example](./samples/
+ Windows binary download by [AppVeyor][av-url]
+ [IntelliJ Plugin][plugin]

## Features

+ [X] Everything that the Haskell implementation has
+ [X] Parser as a cargo feature (using [pest][pest])
+ [X] AST pretty-printer as a cargo feature
+ Improvements to the original implementation
  + [X] 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
  + [X] 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
  + [X] `const` declarations, where the type is inferred
  + [X] Prefixing declarations with parameters, like `let a (b: c): d = f b;`
+ An executable for CLI usages (`minittc`) (using [clap][clap])
  + [X] File checker
  + [X] Completion script generation
    + Get the script: `minittc completion zsh/bash/powershell/fish/elvish`
  + REPL (a fancy one based on [rustyline][rustyline] and a plain
    one based on stdio)
    + [X] Load file
    + [X] Infer (and normalize) type
    + [X] Eval (and normalize) expressions (may panic if ill-typed)
    + [X] Add single declaration
    + [X] Show context/gamma
    + [X] Help
    + [X] Completion
      + [X] Commands
      + [X] Files
      + [ ] In-scope variables
  + [ ] Language server (?)
  + Publish?
    + By `cargo install --path . --bin minittc --all-features`
    + By [AppVeyor][av-url]
      (Just find the configuration fits you best and get the artifact)