minitt-rs

Rust实现的Mini-TT，一种简单的依赖类型lambda演算。此实现包括一个类型检查器（扩展了原始版本）、一个AST美化打印器和命令行工具，可以作为文件检查器和具有自动完成和类型推断的交互式REPL。使用稳定版Rust（版本1.39.0），2018版。它可以作为复杂依赖类型编程语言的核心语言，或用于测试翻译算法的正确性。

我正在尽力使用完整且有意义的名字来避免混淆。我还在对Haskell实现进行整体清理，并在函数上注释了与Haskell实现中对应函数的名称，以便人们在阅读论文的同时不会对此实现感到困惑。

注意：这个POC语言的开发已转移到另一个重新设计的编程语言，Voile。我们有一个新的类型理论，更好的表面语法，更好的错误消息，更丰富的类型检查器。在Voile中，一切（或将成为）更好。

在 示例 中的依赖类型程序

-- 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
 };

我们可以有返回不同类型值的函数，同时它仍然是静态类型的。非常灵活。

安装

最推荐的安装方法是下载来自 GitHub Actions页面 的预构建二进制文件。以下是 如何找到它们 的方法。

您也可以从源代码安装

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

想将minitt用作库？将以下内容添加到您的 Cargo.toml 中（如果您甚至不需要解析器，您可以完全删除功能）

minitt = { version = "0.4.2", features = ["parser"] }

资源

• Mini-TT论文
• 代码示例，在CI上测试
• Doc.rs 文档（包括教程）
• 变更日志
• REPL 示例
• 二进制下载 在 GitHub Actions 页面，支持 Windows、Ubuntu 和 macOS
• IntelliJ 插件，作为 Dependently-Typed Lambda Calculus 项目的一部分
• Mini-TT 工具库，用于构建 CLI REPL

功能

• 拥有 Haskell 实现的所有功能
• 解析器作为 cargo 功能（使用 pest）
• AST 美化打印器作为 cargo 功能
• 对原始实现的改进
  • 使用 BTreeMap 来处理分支/案例树，以便我们在案例顺序上更加灵活
  • 使用 Vec 来处理望远镜/声明，而不是功能不可变列表
• 除了微小的改进之外的新功能
  • 推断对类型
  • 推断构造函数调用类型
  • 推断案例拆分类型
  • 模块系统（或者一个非常简单的系统）
  • （类型化-）孔？
    • 用于完成/上下文查找
    • 用于类型指导开发
  • const 声明，其中类型是推断的
  • 将参数添加到声明之前，例如 let a (b: c): d = f b;
• 用于 CLI 使用的可执行文件（minittc）（使用 clap）
  • 文件检查器
  • 生成完成脚本
    • 获取脚本： minittc completion zsh/bash/powershell/fish/elvish
  • REPL（基于 rustyline 的花哨版本和基于 stdio 的简单版本）
    • 加载文件
    • 推断（并规范化）类型
    • 评估（并规范化）表达式（如果类型不正确可能会引发恐慌）
    • 添加单个声明
    • 显示上下文/伽玛
    • 帮助
    • 完成
      • 命令
      • 文件
      • 作用域中的变量
  • 语言服务器（？）
    • 我们有一个 IntelliJ 插件
  • 发布？
    • 通过 cargo install --path . --bin minittc --all-features
    • 通过 [AppVeyor][av-url]（只需找到最适合您的配置并获取工件）