Tao

您现在可以在浏览器中测试Tao了！

Tao是一种静态类型的函数式编程语言，具有多态性、类型类、广义代数效应、和类型、模式匹配、一等函数、柯里化、良好的诊断功能等多种特性！

<a href = "https://www.github.com/zesterer/tao"> <img src="https://yellow-cdn.veclightyear.com/835a84d5/e739b21f-f3a7-43d4-be67-d038a845685a.png" alt="Tao特性演示"/> </a>

更多示例程序，请参见...

• hello.tao：Hello world
• input.tao：展示了更复杂的IO效应示例
• calc.tao：一个命令行计算器，展示了解析器组合子
• adventure.tao：一个文字冒险游戏
• brainfuck.tao：一个Brainfuck解释器
• mutate.tao：将突变表达为副作用
• polymorphic_effects.tao：一个对副作用多态的高阶函数示例
• quickcheck.tao：在Tao中实现的一个非常简陋的quickcheck版本

目标

目前，Tao是一个业余项目，我没有计划将其转变为生产级语言。随着项目的发展，这可能会改变，但现在我更愿意花时间实验新的语言特性。尽管如此，我对语言本身还是有一些目标的：

• 全面性

  • 所有程序必须明确处理所有输入。没有恐慌、异常等机制。目标是构建一个足够有表现力的类型系统，能够证明广泛程序的全面性。
  • 随着时间的推移，我希望看到该语言发展出对终止分析技术的支持，如Walther递归。

• 极致优化

  • 我一个相当固执且令人讨厌的观点是，静态类型、全面的函数式编程语言的"优化上限"显著高于具有相对较弱类型系统的传统命令式语言。我希望Tao能成为一个实际的例子，让我可以指向它，而不是使用关于不变量的模糊论点。
  • 我特意确保Tao的核心MIR具有非常小的表面积，使其适合各种优化和静态分析。
  • MIR优化器已经执行了相当多的优化，大大减少了生成的字节码指令数量。请参见下面的列表。

• 学习

  • 我只有高中水平的数学知识。我想用Tao作为测试台，帮助我学习更多关于数学、证明、类型系统、逻辑和计算的知识。
  • 此外，我希望Tao能成为那些想要涉足语言设计、编译器开发或简单的函数式编程的人的有用工具：考虑到一些语言特性的复杂性，代码库相对较小且实用。

特性

• Hindley-Milner类型推断
• 有用的错误信息
• 代数数据类型
  • 和类型
  • 记录类型
  • 泛型数据类型
  • 名义别名（如：data Metres = Real）
• 类型别名
• 通过泛型实现的类型多态
  • 类约束
  • 关联类型相等约束
  • 任意where子句（包括关联类型相等）
  • 惰性关联项推断（Foo.Bar.Baz.Biz在每一步都惰性推断类！）
  • 类型检查器是图灵完备的（这算是一个特性吗？可能不是...）
  • 变异性在类型和效果参数中都得到正确追踪
• 模式匹配
  • 解构和绑定
  • ADT模式
  • 列表模式（[a, b, c]，[a, b .. c]等）
  • 算术模式（如：n + k）
  • 居住性检查（如：None穷尽覆盖Maybe Never）
  • 递归穷尽性检查
  • let进行模式匹配
• 一等函数
  • 函数支持模式匹配
  • 柯里化
• 类型类
  • 类型参数
  • 关联类型
  • 运算符通过类型类实现
• 代数效应
  • 效应对象（独立于函数，不同于某些语言）
  • 流域和传播语法（相当于Haskell的do表示法，或Rust的async/try块）
  • 泛型效应
  • 多态效应（不再需要try_x或async_x函数！）
  • 效应集（即：可以表达具有多个副作用的值）
  • 效应别名
  • 效应处理器（包括有状态处理器，允许用单子IO表达效应驱动的IO）
  • 效应可以由类型和其他效应参数化
• 内置列表
  • 专用列表构造语法（[a, b, c]，[a, b .. c, d]等）
• 显式尾调用优化
  • 更好的语法/保证
• 优化
  • 泛型代码单态化
  • 内联
  • 常量折叠
  • 符号执行
  • 分支交换
  • 死代码删除
  • 居住性分析
  • 穷尽模式展平
  • 未使用函数剪枝
  • 未使用绑定移除
  • 算术重写/简化
  • 恒等分支移除
• 字节码编译器
• 字节码虚拟机

当前正在进行

• 模式穷尽性检查（健全但过于保守）
• 算术模式（当前仅实现了自然数加法）
• 类型类
  • 一致性检查器
  • 可见成员语义以放宽孤儿规则
• MIR优化器
  • 拆箱
  • 递归类型的自动表示更改
    • 将data Nat = Succ Nat | Zero转换为运行时整数
    • 将data List A = Cons (A, List A) | Nil转换为向量
• 代数效应
  • 高阶效应（需要适当的async支持）
  • 效应对象的任意恢复/挂起
  • 效应对象的完全单态化

计划功能

• 更好的语法（可能对模式匹配使用缩进敏感？）
• 模块系统（代替import复制/粘贴）
• LLVM/Cranelift后端

理念

• 偏好通用解决方案而非特例处理：应该优先考虑灵活和通用的特性，而不是可能在后期产生棘手问题的特定解决方案，这些问题可能需要更多特例解决方案来解决。提供一个较小的通用特性核心比将语言发展成一个不统一的混乱更好。

• 正确性优先于便利性：如果某些内容存在问题或边缘情况，不要掩盖裂缝。Tao试图强制程序员编写尽可能完善和无bug的程序。溢出很重要。未处理的模式很重要。重叠的类实现很重要。

• 做显而易见的事：当需要在行为上做出选择时，应该选择最常见的正确做法。其他所有情况都应该默认开启lint或报错。

• 相似概念应有相似语法：列表/记录/数据类型的构造和解构（即模式匹配）应共享相同的语法。函数参数模式和when模式应共享相同的语法。

• 局部推理：在可能的情况下，程序/函数/表达式的行为应该只通过局部信息就能明显看出。不应有需要查看导入才能理解的奇怪覆盖或行为变化。

• 表达你的意思：语法确实很重要！程序是为了阅读而设计的，Tao应该鼓励编写能讲述线性故事的程序。如果你需要来回跳转才能理解程序，那就是需要修复的问题。

• 抽象应保留'核心'语义：许多语言提供复杂的宏系统，允许大规模的元编程。Tao并不反对元编程和抽象，但积极尝试将这些内容保持在表面语法范围内，以提高可读性并最小化意外因素。作为一个很好的补充，拒绝宏使Tao对IDE和静态分析系统更加友好。

有趣的特性

以下是Tao独有或在其他语言中不常见的一些特性选择。

广义代数效应

Tao支持"广义代数效应"。"效应"意味着Tao可以在类型签名中表达函数的副作用（IO、变异、异常、异步等）。"广义"意味着你可以创建和使用自己的效应来表达任何你想要的东西。"代数"意味着Tao允许代码对一个效应（或一组效应）进行泛化。例如，考虑map函数，用于依次对列表的每个元素应用一个函数：

fn map A, B : (A -> B) -> [A] -> [B]
    | _, [] => []
    \ f, [x .. xs] => [f(x) .. map(f, xs)]

map可以这样使用，例如，将列表中的所有元素翻倍：

[1, 2, 3, 4]
    -> map(fn x => x * 2)

# 结果：[2, 4, 6, 8]

大多数语言，如Rust，都有类似的函数。不幸的是，当我们想在映射函数中做一些哪怕是稍微不同于"纯"映射的事情时，它很快就会失效。例如，考虑一个程序，其映射函数可能失败，或需要完成某些异步操作。必须做以下两件事之一：

• 让函数通过栈展开"静默"退出，就像在C#、C++等语言中那样。
• 创建一个可以处理失败的函数副本，如Rust中的try_map。

值得注意的是，Haskell主要通过单子解决了这个问题：但它们经常很笨重。效应系统和单子有很多相似之处，但前者更努力地使它们与常规控制流更好地集成。

在Tao中，这个问题可以通过让map对一个效应参数进行泛化来解决，如下所示：

fn map A, B, e : (A -> e ~ B) -> [A] -> e ~ [B]
    | _, [] => []
    \ f, [x .. xs] => [f(x)! .. map(f, xs)!]

这里有几处变化。

首先，我们引入了一个效应参数e。其次，类型签名发生了变化：映射函数A -> B现在在其返回类型上附加了e，变成A -> e ~ B。这也出现在函数的最终返回类型e ~ [B]中，表示函数整体的副作用对应于映射函数执行的副作用。

其次，在实现中调用映射函数后出现了!运算符。这是"效应传播"运算符，向编译器表明f的副作用应该被提升到整个函数的签名中。

注意，除此之外，实现保持不变：我们不需要使用任何复杂的机制来处理副作用（就像在Rust风格的try_map中那样），只需要一个额外的运算符。

由于这个变化，map现在可以接受执行任何副作用的映射函数：抛出错误、IO、生成值、变异等等。它还接受执行任意效应组合的函数，或者根本没有副作用的函数（空集仍然是一个有效的效应集！）：

# 生成列表中的每个元素，结果是一个生成器
[1, 2, 3, 4]
    -> map(fn x => yield(x)!)!

# 如果列表中任何元素为`0`，则生成一个错误
[1, 2, 3, 4]
    -> map(fn x => if x = 0 then err("不允许零")! else x)!

# 打印列表中的每个元素
[1, 2, 3, 4]
    -> map(fn x => print(x)!)!

这就是代数效应系统的表达能力：我们不再需要担心函数颜色、隐藏的崩溃/异常，或编写多个版本的函数来处理各种不规则的控制流。由于代数效应的泛化性很强，它也可以用于以可组合的方式将接口与实现分离，允许开发者根据需要交换甚至是非常核心的API（如文件系统访问）的实现，而无需复杂和笨拙的回调系统。

在Tao中，效应是种类，就像Rust中的类型、生命周期和常量一样。它们也独立于函数签名表示，作为"效应对象"（你可以把效应对象想象成类似于Future/Promise，但泛化到所有副作用）。因此，可以在广泛的上下文中使用它们。

算术模式

Tao的类型系统旨在完全可靠（即：不可能触发运行时错误，除了"实现"因素如OOM、栈溢出等）。因此，自然数的减法会产生一个有符号整数，而不是自然数。然而，许多算法仍然需要将数字倒数到零！

为了解决这个问题，Tao支持在模式中执行算术运算，并绑定结果。由于编译器直观地理解这些操作，可以静态确定这些操作的可靠性，并保证永远不会发生运行时错误或溢出。看看这个100%可靠的阶乘程序！

fn factorial =
    | 0 => 1
    \ y ~ x + 1 => y * factorial(x)

所有函数都是lambda，并允许模式匹配

除了语法糖（如类型别名）外，Tao只有两个高级构造：值和类型。每个"函数"实际上只是对应于行内lambda的值，而行内lambda语法自然地泛化以允许模式匹配。允许多个模式参数，每个参数对应函数的一个参数。

def five =
    let identity = fn x => x in
    identity(5)

穷尽的模式匹配

Tao要求模式匹配是穷尽的，如果模式没有被处理，将会产生错误。

非常少的分隔符，但空格不是语义的

在Tao中，每个值都是一个表达式。即使是let，在大多数语言中通常是一个语句，在Tao中也是一个表达式。正因如此，Tao不需要分号和代码块。

柯里化和前缀调用

在Tao中，arg->f是f(arg)（函数应用）的简写。此外，这种前缀语法可以链式使用，从而形成非常自然的一级管道语法。

my_list
    -> filter(fn x => x % 2 == 0) # 只包含偶数元素
    -> map(fn x => x * x)         # 对元素进行平方
    -> sum                        # 对元素求和

有用且用户友好的错误诊断

这一点通过图片展示会更好。

<a href = "https://www.github.com/zesterer/tao"> <img src="https://yellow-cdn.veclightyear.com/835a84d5/95cfe76f-363b-483a-9e53-0037ad99d7f3.png" alt="Tao错误示例"/> </a>

Tao保留了输入代码的有用信息，如每个元素的跨度，从而能够提供丰富的错误信息，引导用户解决程序问题。诊断信息的渲染是通过我的crate Ariadne完成的。

自动调用图生成

Tao编译器还可以自动生成程序的graphviz调用图，帮助你更好地理解程序。以下是examples/calc.tao中的表达式解析器和REPL。调用图会自动忽略工具函数（即带有$[util]属性的函数），这意味着即使是非常复杂的程序也能变得易于理解。

<a href = "https://yellow-cdn.veclightyear.com/835a84d5/da472ab8-9986-4f54-ac56-d4c609bcf9a0.svg"> <img src="https://yellow-cdn.veclightyear.com/835a84d5/da472ab8-9986-4f54-ac56-d4c609bcf9a0.svg" alt="Tao中表达式解析器的调用图"/> </a>

使用方法

命令

编译/运行一个.tao文件

cargo run -- <文件>

运行编译器测试

cargo test

编译/运行标准库

cargo run -- lib/std.tao

编译器参数

• --opt：指定优化模式（none、fast、size）

• --debug：为编译阶段启用调试输出（tokens、ast、hir、mir、bytecode）