Yatima：一个用于去中心化网络的编程语言

从某种意义上说，真理矿场只是另一个索引景观。图书馆内容的数十万个专业选择以类似的方式可访问——Yatima 已经攀登了进化树，跳跃了元素周期表，沿着历史长廊行走了 fleshers、gleisners 和公民的历史。半个 megatau 之前，ve'd 在真核细胞中游泳；每个蛋白质，每个核苷酸，甚至通过细胞质飘浮的碳水化合物都广播了包含对图书馆有关所讨论分子所有说明的全局标记。

然而，在真理矿场中，标签不仅仅是引用；它们包括了对象所代表的特定定义、公理或定理的完整陈述。矿场是自包含的：肉身及其后代所证明的每一个数学结果都完整地展示出来。图书馆的解释很有帮助——但真理本身都在这里。

分散，Greg Egan

Yatima 是一个由 Rust 实现的纯函数式编程语言，具有以下特性：

• 内容寻址 为可重复构建和点对点包管理提供支持。Yatima 的内容寻址代表一个不可变的程序及其所有依赖项。这意味着如果有人与你分享一个地址，你就可以完美地复制他们的计算（原则上甚至复制他们的计算环境！）由于程序是不可变的，它第一次运行的方式就是它每次运行的方式。
• 一等类型。这使得程序员可以向编译器说明他们在程序中打算做什么。然后，就像一个乐于助人的机器人助手一样，编译器会检查确保你实际所做的事情与你所表达的目的相符。类型驱动编程让编译器充当你的“正确性外皮”，即一种认知增强，帮助你捕捉到错误。
• 线性、仿射和擦除类型让你在执行过程中对资源使用具有精细的控制。子结构类型允许你获得使用高级语言带来的内存安全优势，同时在你想要的时候也能让你“接近金属”。
• 类型安全的依赖元编程让 Yatima 具有动态类型语言的灵活性和可扩展性，同时不牺牲静态类型的安全性。

示例

代数数据类型（ADT）

type Maybe (A: Type) {
  None,
  Some A,
}

type List (A: Type) {
  Nil,
  Cons A (List A),
}

def List.head (0 A: Type) (a: List A): Maybe A
  = (case a) (λ _ => Maybe A) (Maybe.None A) (λ x _ => Maybe.Some A x)

泛化代数数据类型

type Expr: ∀ Type -> Type {
  N Nat: Expr Nat,
  B Bool: Expr Bool,
  Add (Expr Nat) (Expr Nat): Expr Nat,
  Mut (Expr Nat) (Expr Nat): Expr Nat,
  Eql (Expr Nat) (Expr Nat): Expr Bool,
}

def Expr.checks : Expr Bool = Expr.Eql (Expr.N 1) (Expr.N 2)

依赖类型和证明

type Vector (A: Type): ∀ (ω k: Natural) -> Type {
   Nil: Vector A Natural.Z,
   Cons (0 k: Natural) (x: A) (xs: Vector A k): Vector A (Natural.S k),
}

def Vector.head (0 A: Type) (k: Natural) (a : Vector A (Natural.S k)): A
  = ((case a) (λ k' self => ∀ (Equal Natural (Natural.S k) k') -> A)
    (λ e => Empty.absurd A (Natural.Z_isnt_S k e))
    (λ k x xs e => x))
    (Equal.Refl Natural (Natural.S k))

有关 Yatima 代码的更多示例，请参阅标准库 introit：https://github.com/yatima-inc/introit

实现

• Yatima 的核心归约机基于在 自下而上的 β-归约 中描述的 λ-DAG 技术。
• Yatima 的归纳数据类型方法基于 Self Types for Dependently Typed Lambda Encodings。
• Yatima 的量化类型基于 量化类型理论的语法和语义。
• 该语言的许多方面，特别是其库和类型等价算法，都是基于作者在 Formality 证明语言 上的先前工作的。

在 Matrix 上与我们聊天：#yatima:matrix.org 或在 Yatima subreddit

构建说明

克隆此存储库并 cd 进入它

git clone [email protected]:yatima-inc/yatima.git
...
cd yatima

使用二进制缓存（可选）

为了加速构建，请使用来自 cachix 的二进制缓存。安装 cachix 并运行

cachix use yatima

使用 Nix flakes（默认）

假设您已激活了 Nix 的 flakes，否则 请参阅此处。

# Activate shell environment
direnv allow
# Run standalone
nix run
# Build
nix build
# Start dev shell. Handled automatically by direnv
nix develop
# Install into your environment
nix profile install

编译到 WASM

nix-shell
cd web

然后运行以下命令安装所需的依赖项

npm install

之后，可以通过以下方式托管实验性网络版本

npm start

使用 cargo

Yatima 需要 nightly Rust

rustup default nightly

构建 yatima

cargo build

运行测试套件

cargo test --all

安装 yatima 二进制文件

cargo install --path cli

使用说明

使用以下方法解析 .ya 文件（例如从 https://github.com/yatima-inc/introit）

λ yatima parse bool.ya 
Package parsed: bafy2bzacedl5jeqjqvvykquxjy53xey2l2hvcye2bi2omddjdwjbfqkpagksi
...

使用以下方法进行类型检查

λ yatima check bool.ya
Checking package bool at bafy2bzacedl5jeqjqvvykquxjy53xey2l2hvcye2bi2omddjdwjbfqkpagksi
Checking definitions:
✓ Bool: Type
✓ Bool.True: Bool
✓ Bool.False: Bool
✓ Bool.eql: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.lte: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.lth: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.gte: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.gth: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.and: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.or: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.xor: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.not: ∀ (x: Bool) -> Bool
✓ Bool.neq: ∀ (x: Bool) (y: Bool) -> Bool
✓ Bool.if: ∀ (A: Type) (bool: Bool) (t: A) (f: A) -> A

使用以下方法在 Yatima 包中运行 main 表达式

yatima run HelloWorld.ya

使用以下方法进入交互式 Yatima REPL

yatima repl

动机

我们仍然处于计算革命的早期阶段。第一台通用数字计算机仅在 75 年前投入使用。你父母的记忆和祖父母的记忆都延伸到计算机出现之前的过去。这些机器令人震惊地新，作为一个物种，我们真的不知道它们是用来做什么的。我们正处于一场划时代的转变之中，其最近的前例是 书写 的发明。关于这将对我们的未来意味着什么有许多预言；有许多不同的、有时相互矛盾的计算将如何继续塑造我们的心灵、我们的身体以及我们彼此之间关系的愿景。

作为一项工程，Yatima对未来有着自己的看法。我们认为计算应该属于个人用户，而不是企业或国家。编程语言是个人表达的一种赋权媒介，用户通过计算机器遭遇并扩展他们的思想。我们认为“程序员”不应再是工作描述，就像在几乎全民识字的世界上，“抄写员”也不再是工作描述一样。计算属于每个人，因此计算机编程应该对每个人都是最大程度可获取的。

目前并非如此：全球约有50亿互联网用户，但只有约2500万软件开发者。这是不到1%的“编程识字率”。此外，这一群体在人口统计学上并不具有代表性。它严重偏向男性、全球北方以及来自享有特权的经济社会或种族背景的人。这是可耻的。就像我们生活在某种荒谬的反乌托邦中，只有绿色眼睛的人才能演奏音乐。

一种新的编程语言不会是某种万能药，可以自行解决这个问题，但编程语言确实有一些可以帮助的方法。

1. 构建一个简单但功能强大的编程语言。Yatima的核心逻辑不超过500行代码，但在类型系统、运行时和语法方面非常具有表现力。我们希望减少语言的概念负担，而不妨碍语言学习者的未来成长和力量。

2. 在语言中明确计算与数学之间的联系。这两个看似不同的领域实际上在本质上是一样的：所有证明都是程序，所有程序都是证明。一个做数学作业的学生其实是在编程，即使他们没有这样的概念。

   许多人因为手动计算的繁琐和结果的不明确相关性而讨厌数学。许多人也因为具体的机制往往显得任意和令人沮丧而讨厌编程。这些是互补的抱怨。当你有电脑帮你处理细节工作时，数学更有趣。当你对你所做事情的理论有清晰的认识时，计算会容易得多。

3. 在执行上具有可移植性。在本地、浏览器、移动设备、分布式进程中运行。人们不应该担心他们想做什么的细节，而应该关注他们想做什么。

4. 在语义上具有可移植性。纯语义和可重复构建让人们能够关注程序的实际内容，而不是配置基础设施的繁琐工作。

5. 与去中心化技术集成，尽可能消除社会障碍和摩擦。像大多数现代软件包管理器这样的集中式服务引发了一个问题：“谁控制着软件包服务器？”著名的leftpad事件通常被呈现为一个构建系统问题（这绝对是一个），但讨论较少的是，引发事件的原因是npm管理员在没有得到开发者同意的情况下，将一个软件包的所有权从个人开发者转让给了一家大公司。

6. 制定明确的道德规范来对抗当代编程文化的普遍毒性。有些人可能会觉得这有争议，但不应如此。计算既是一项技术项目，也是一项社会和文化项目。那些延续创伤循环的文化在长远来看不如那些不这样做的事业成功。

我们想要建设的未来是一个数十亿人使用、理解和热爱他们的数学计算机器的未来，这是他们自身自然的延伸。一个用户对自己的系统和数据拥有自主权和隐私的未来。一个可靠、类型检查、形式验证的软件成为常态的未来，这样你就可以像在桥上开车时对土木工程有日常信心一样，信赖软件工程。

感谢我们的支持者！