使用说明

读者指南

《编程语言基础：Agda 语言描述》的使用方法与《Programming Language Foundations in Agda》一致。

本书可访问 PLFA-zh 在线阅读。

要参与翻译，请先阅读翻译规范。

你可以在线阅读 PLFA，无需安装任何东西。 然而，如果你想要交互式编写代码或完成习题，那么就需要几样东西：

• macOS 上：XCode 命令行工具
• Git
• GHC and Cabal
• Agda
• Agda 标准库
• PLFA

PLFA 只针对特定的 Agda 和标准库版本进行了测试，相应版本已在前面的徽章中指明。 Agda 和标准库变化得十分迅速，而这些改变经常搞坏 PLFA，因此使用旧版或新版通常会出现问题。

Agda 和 Agda 标准库有多个版本。如果你使用了包管理器（如 Homebrew 或者 Debian apt），Agda 的版本可能不是最新的。除此之外，Agda 仍然在活跃的开发之中，如果你从 GitHub 上安装了开发版本，开发者的新变更也可能让这里的代码出现问题。 因此，使用上述版本的 Agda 和 Agda 标准库很重要。

macOS 平台：安装 XCode 命令行工具

在 macOS 平台，你需要安装 XCode 命令行工具。 在大多数 macOS 系统版本上，你可以用下面的命令安装它们：

xcode-select --install

安装 Git

你可以使用下面的命令来检查你是否安装了 Git。

git --version

如果你没有 Git，请参阅 Git 下载页面。

安装 GHC 和 Cabal

Agda 是用 Haskell 写成的，所以为了安装它我们需要 Glorious Haskell Compiler 和它的包管理器 Cabal。PLFA 应该在任何 >=8.10 的 GHC 版本下运行，在 8.10 到 9.8 版本下完成测试。我们建议使用 ghcup 来安装两者。 在 ghcup 安装好之后，输入下列命令：

ghcup install ghc 9.4.8
ghcup install cabal recommended

ghcup set ghc 9.4.8
ghcup set cabal recommended

或使用 ghcup tui 来『设置』合适的工具。

安装 Agda

安装 Agda 最简单的方法是通过 Cabal。PLFA 使用 Agda 版本 2.7.0。运行下面的命令：

cabal update
cabal install Agda-2.7.0

这一步会消耗很长时间和很多内存来完成。

如果你遇到了问题，或者想参考替代的方法，可参阅 Agda 安装指引。

如果你愿意，你可以测试 Agda 是否已正确安装。

安装 PLFA 和 Agda 标准库

我们建议你使用下面的命令把 PLFA 安装至你的家目录：

git clone --depth 1 https://github.com/plfa/plfa.github.io plfa

PLFA 包括了所需的 Agda 标准库版本，你可以在安装 PLFA 的目录下运行以下命令来下载它。

git submodule update --init

最后，我们需要让 Agda 知道如何找到标准库和 PLFA。 你需要两个配置文件，一个用于指定库的路径，一个用于指定默认载入的库。

在 macOS 和 Unix 上，如果 PLFA 已经安装至 Home 目录，且你没有希望保存的配置文件，运行下面的命令：

mkdir -p ~/.agda
cp ~/plfa/data/dotagda/* ~/.agda

这条命令提供了 Agda 标准库，也让 PLFA 可以当作一个 Agda 库来使用。

否则，你需要手动编辑相关的配置文件。两者都位于 AGDA_DIR 目录下。 在 UNIX 和 macOS 平台，AGDA_DIR 默认为 ~/.agda。在 Windows 平台，AGDA_DIR 一般默认为 %AppData%\agda，而 %AppData% 默认为 C:\Users\USERNAME\AppData\Roaming。

• 如果 AGDA_DIR 文件夹不存在，创建它。
• 在 AGDA_DIR 中，创建一个纯文本文件 libraries，内容为 /path/to/standard-library.agda-lib （即上文中记录的路径）。 这个文件让 Agda 知道有一个名为 standard-library 的库可用。
• 在 AGDA_DIR 中，创建一个纯文本文件 defaults，内容__仅__为 standard-library 这一行。
• 如果你想导入书中的模块，那么需要将 PLFA 设置为 Agda 库。假设 PLFA 是 PLFA 的根目录，完成此设置需要将 PLFA/src/plfa.agda-lib 作为单独的一行添加到 AGDA_DIR/libraries，并将 plfa 作为单独的一行添加到 AGDA_DIR/defaults。

关于放置标准库的更多信息可以参阅 Agda 文档中的库管理。

设置 Agda 的编辑器

Emacs

推荐的 Agda 编辑器是 Emacs。安装 Emacs 可以用下面的方法：

• UNIX：包管理器中的 Emacs 应该可以使用（只要它的版本比较新），GNU Emacs 下载页面也有最近发布版本的链接。
• MacOS：推荐的 Emacs 是 Aquamacs，但是 GNU Emacs 也可以通过 Homebrew 或者 MacPorts 安装。参阅 GNU Emacs 下载页面中的指示。
• Windows：参阅 GNU Emacs 下载页面中的指示。

确保你可以用你安装的版本打开、编辑、保存文件。GNU Emacs 网站上的 Emacs 向导描述了如何打开 Emacs 安装中的教程。

Agda 自带了 Emacs 编辑器支持，如果你安装了 Agda，运行下面的命令来配置 Emacs：

agda-mode setup
agda-mode compile

如果你已经是 Emacs 用户，并有自己的设置，你可能需要留意 setup 命令追加到 .emacs 文件中的配置，并将其与你已有的设置整合。

在 Emacs 中自动加载 agda-mode

从版本 2.6.0 开始，Agda 支持 Markdown 风格的文学编程，文件使用 .lagda.md 扩展名。 该扩展名的一个问题就是 Emacs 默认会进入 Markdown 编辑模式。 而为了让 agda-mode 在你打开 .agda 或 .lagda.md 文件时自动加载， 请将以下内容放到你的 Emacs 配置文件中：

;; auto-load agda-mode for .agda and .lagda.md
(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

如果你的配置中已有了改变 auto-mode-alist 的设置，将上述内容放置在已有的设置__之后__，或者将其与已有设置合并（如果你对 Emacs Lisp 足够了解）。 Emacs 的配置文件通常位于 ~/.emacs 或 ~/.emacs.d/init.el，然而 Aquamacs 用户需要将启动设置放到位于 ~/Library/Preferences/Aquamacs Emacs/Preferences 的 Preferences.el 文件中。 对于 Windows 平台，请参阅 GNU Emacs 文档 来寻找配置文件的位置。

可选：在 Emacs 中使用 JuliaMono 字体

Agda 中的很多重要符号是用 Unicode 来表示的，因此用来显示和编辑 Agda 的字体需要正确地显示这些符号。最重要的是你使用的字体需要有好的 Unicode 字符支持。我们推荐 JuliaMono， 其他的备选字体有 mononoki、Source Code Pro、 DejaVu Sans Mono 和 FreeMono。

你可以直接从此网站 下载并安装 JuliaMono。对于大多数系统来说，安装字体只是简单的下载 .otf 或者 .ttf 文件。 如果你的包管理器提供了 JuliaMono 的包，那样可能更加简单。 例如，macOS 的 Homebrew 提供了 [font-juliamono][font-JuliaMono-homebrew] 包。 将下面的内容加入 Emacs 配置文件，可以把 JuliaMono 设置为 Emacs 的默认字体：

;; default to JuliaMono
(set-face-attribute 'default nil
                    :family "JuliaMono"
                    :height 120
                    :weight 'normal
                    :width  'normal)

检查 agda-mode 是否正确安装

在 Emacs 中打开本书的第一章 (plfa/src/plfa/part1/Naturals.lagda.md)，输入 C-c C-l 来载入和类型检查这个文件。

在 Emacs 中使用 agda-mode

要加载文件并对其执行类型检查，请使用 C-c C-l。

Agda 的编辑是通过使用「洞」来交互的，它表示程序中尚未填充的片段。 如果用问号作为表达式，并用 C-c C-l 加载缓冲区，Agda 会将问号替换为一个「洞」。 当光标在洞中时，你可以做以下这些事情：

• C-c C-c: 分项（询问变量名，case）
• C-c C-空格：填洞
• C-c C-r：用构造子精化（refine）
• C-c C-a：自动填洞（automatic）
• C-c C-,：目标类型和语境
• C-c C-.：目标类型，语境，以及推断的类型

更多细节请见 emacs-mode 文档。

如果你想在 Agda 代码的侧边而非底栏查看信息，那么可以这样做：

• 打开 Agda 文件并按 C-c C-l；
• 按 C-x 1 来仅显示当前 Agda 文件；
• 按 C-x 3 来垂直分割窗口；
• 将光标移动到右侧窗口；
• 按 C-x b 并输入「Agda information」切换到该缓冲区。

现在，Agda 的错误消息将会在代码右侧显示，而非被挤压在底部的狭小空间里。

在 Emacs 中使用 agda-mode 输入 Unicode 字符

当你书写 Agda 代码时，你需要输入标准键盘上没有的字符。Emacs 的「Agda-mode」定义了字符翻译来让这件事更容易：当你输入特定普通字符的序列时，Emacs 会在 Agda 文件中使用对应的特殊字符来替换。

例如，我们可以在之前的 .agda 测试文件中加入一条注释。 比如说，我们想要加入下面的注释：

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

前几个字符都是普通字符，我们可以如往常的方式输入它们……

{- I am excited to type

在最后一个空格之后，我们无法在键盘上找到 ∀ 这个键。这个字符的输入序列是四个字符 \all，所以我们输入这四个字符，当我们完成时，Emacs 会把它们替换成我们想要的……

{- I am excited to type ∀

我们继续输入其他字符。有时字符会在输入时发生变化，因为一个字符的输入序列是另一个字符输入序列的前缀。 在我们输入箭头时会出现这样的情况，它的输入序列是 \->。在输入 \- 之后我们会看到……

{- I am excited to type ∀ and -

……因为输入序列 \- 对应了一定长度的短横。当我们输入 > 时，­ 变成了 →！ ≤ 的输入序列是 \<=，≡ 的是 \==。

{- I am excited to type ∀ and → and ≤ and ≡

最后几个字符又回归了普通字符……

{- I am excited to type ∀ and → and ≤ and ≡ !! -}

如果你在 Emacs 中输入 Unicode 时遇到了问题，可以在每章的最后找到当前章节中用到的 Unicode 字符。

带有 agda-mode 的 Emacs 提供了很多有用的命令，其中有两个对处理 Unicode 字符时特别有用。 支持的字符的完整列表可使用 agda-input-show-translations 命令查看：

M-x agda-input-show-translations

agda-mode 支持的所有字符都会列出来。

如果你想知道如何在 agda 文件中输入一个特定的 Unicode 字符，请将光标移动到该字符上并输入以下命令：

M-x quail-show-key

你会在迷你缓冲区中看到该字符对应的按键序列。

Spacemacs

Spacemacs 是一个「社区引领的 Emacs 版本」，对 Emacs 和 Vim 的编辑方式都有很好的支持。它自带集成了 agda-mode，所需的只是在 .spacemacs 中启用 Agda 支持。

Visual Studio Code

Visual Studio Code 是一个微软开发的开源代码编辑器。 Visual Studio 市场中有 Agda 插件。

贡献者指南

如果你打算在本地构建 PLFA，请参阅贡献指南以获取更多说明。