Lib.rs

鹌鹑语言

• 简介
• 入门
• 基础知识
• Vim 高亮显示

简介

鹌鹑是一种受 Haskell、Idris 和 Elm 启发的编程语言。它旨在探索在不对纯度和完备性这一基本概念做出妥协的情况下，语言设计所能达到的潜力。

纯度是指表达式评估永远不会产生对运行时可见的任何副作用。在鹌鹑中，所有表达式都代表常量值。一旦定义了一个变量，它的值就永远不会改变，因此可以始终用其定义来替换它。纯度要求作者对其代码中的数据流保持纪律。同样，维护者可以免于担心程序的局部行为。

完备性是指评估任何表达式最终都会得到预期的类型值。在鹌鹑中，匹配语句必须覆盖所有可能的案例。没有异常的概念。程序不得陷入无限循环。递归必须是良基的。完备性允许鹌鹑避免需要首选的评估顺序（例如，严格与懒）。它还允许对归纳数据（如列表）和归纳数据（如流）进行有意义的区分。

鹌鹑旨在成为一门适合初学者的语言。由于它们的学术起源，函数式编程语言因其晦涩和难以学习而享有盛誉。这是令人遗憾的，因为函数式编程的优势是由基本思想所赋予的，如强类型、不可变性、模式匹配以及 lambda 演算的整体原则性设计。鹌鹑被设计成最小化、优雅，最重要的是易于学习。

入门

要开始，请克隆存储库，然后运行示例程序之一

$ git clone https://github.com/tac-tics/quail
$ cd quail
$ cargo run --release examples/primes.ql
Finished dev [unoptimized + debuginfo] target(s) in 0.02s
     Running `target/debug/quail examples/primes.ql`
     2
     3
     5
     7
     11
     13

基础知识

鹌鹑中最基本的类型是 Nat，代表自然数。 Nat 通过构造函数 zero 和 succ 构建。数字 zero 应该对您来说很熟悉。函数 succ 简称“后继”，意思是“比...多一个”，由于它是一个函数，所以它必须应用于另一个 Nat。因此，数字一可以表示为 succ zero。数字二可以表示为 succ (succ zero)。

每个自然数都可以这样表示。没有数字字面量，所以你不能写像这样 3 的东西。相反，你必须显式地构造你想要的数字：succ ( succ ( succ zero))。

当你想将数字打印到屏幕上时，你可以使用内置的 show 函数，它将 Nat 转换为 Str，以及 println 函数，它将 Str 打印到屏幕上。

以下是一个Quail的简短程序，用于入门 Nat。

# tutorial.ql
def main : Top = println (show (succ (succ (succ zero))))

你可以将此保存到名为 tutorial.ql 的文件中，然后按以下方式运行它

$ quail tutorial.ql
3

然后你会在控制台看到数字 3 被打印出来。

你可以使用 def 关键字来定义变量。所以也许我们想定义前几个自然数，这样我们就不必一遍又一遍地输入它们

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def main : Top = println (show three)

再次保存并运行它将显示相同的结果。

请注意，one、two 和 three 都在其后写有 : Nat。语法 : 读作 "具有类型"。所以当我们写 def three : Nat = ... 时，我们正在定义一个新的变量 three，它具有 Nat 类型。在Quail中，所有顶层定义都必须注解其类型。

要在Quail中做出决定，我们使用 match 语句。一个 match 语句将查看我们给它提供的值，然后确定接下来要采取什么行动。例如，如果我们想检查一个数字是否为零，我们可以写这个

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def main : Top = match three
    with zero => println "is zero"
    with succ n => println "is not zero"

在 match 语句下面，我们有两个以关键字 with 开头的行。关键字 with 总是后面跟着一个模式，而模式就是我们试图与之匹配的内容。最后，我们有一个粗箭头 => 后面跟着在匹配情况下我们想要的表达式。

第一个 with 子句表示，“当我们用 zero 匹配时，将 is zero 打印到屏幕上”。另一个表示“当我们用 succ 匹配时，将 is not zero 打印到屏幕上”。在 succ 后面的变量 n 在这个例子中没有使用，但它在那里告诉我们模式匹配创建了一个新的变量 n，它可以告诉我们需要调用 succ 来得到 three，即我们要匹配的值。

Quail的一个有趣之处在于，虽然 zero 和 succ 是语言内建的，但熟悉的加法操作不是。为了执行加法，我们必须首先定义它。我们这样做是通过使用 match 和一种称为递归的技术来完成的。

# tutorial.ql
def one : Nat = succ zero
def two : Nat = succ one
def three : Nat = succ two

def add : Nat -> Nat -> Nat =
     fun n m => match n
        with zero => m
        with succ n' => succ (add n' m)

def main : Top = println (show (add two three))

在这里，我们定义了一个新的函数 add。您可以看到它的类型是 Nat -> Nat -> Nat，这意味着它接受两个 Nat 作为参数，并返回一个 Nat。它通过使用 fun 关键字定义为一个函数，我们分别将它的两个参数命名为 n 和 m。

一旦我们接收了两个数字作为输入，我们就通过匹配 n 来继续。这允许我们将 n 分解并查看各个部分。然后我们可以考虑在 Nat 的两个组成部分中，即 zero 和 succ，加法将如何工作。

当 n 与 zero 匹配时，我们考虑 add zero m 的值应该是什么。这似乎很简单：将 zero 添加到任何东西应该只改变那个东西。因此，我们有 with zero => m 告诉我们正是如此。

下一行稍微有些困难。首先，当我们用模式 succ n' 匹配 n 时，我们得到一个新的变量来处理：n'。因为我们用 n 匹配 succ n'，这两个表达式是相等的：n = succ n'。如果您稍微思考一下，这意味着 n' 是比 n 小一的数字。

最后，我们调用了 add 的递归函数。这意味着 add 将通过自身来定义。您可能会认为这会创建一种循环逻辑。但只要我们小心，我们可以避免任何真正的循环。我们用 n' 和 m 作为参数调用 add，由于 n' 总是小于 n，对 add 的重复调用最终会将 n 降低到 zero，我们的递归将终止。

您可以在 nat.ql 中看到 Nat 的更多示例。

Vim 高亮显示

如果您使用 vim，您可以通过以下方式安装语法高亮显示

$ cp -r quail.vim/ ~/.vim/bundle/