实现概述
这些是关于实现方面的一些未分类的注释。粗略的，并不总是完全最新的，但希望能提供一些关于正在发生的事情的提示以及在代码中查看某些功能如何工作的一些想法。
介绍
核心语言 TT（在 Core.TT 中定义），基于定量类型理论（参见 https://bentnib.org/quantitative-type-theory.html）。具有 0 、 1 或 unlimited 的 “多重性”。
术语在范围内的名称上编入索引，因此我们知道术语始终具有良好的范围。值（即标准形式）在 Core.Value 中定义为 NF ；在明确请求之前，构造函数不会对参数进行求值。
从更高级别的语言 TTImp*（定义在 ``TTImp.TTImp`` ）中细化到 *TT，这是带有隐式参数、局部函数定义、案例块、作为模式、具有自动类型导向消歧的限定名称的 TT , 还有证明搜索。
细化依赖于 unification（在 Core.Unify 中），它允许推迟 unification 问题。基本上与 Ulf Norell 论文中描述的 Agda 的工作方式相同。
一般的想法是高级语言将提供对 TT 的翻译。在 Idris/ 命名空间中，我们定义了 Idris 的高级语法，它通过脱糖操作符、do 符号等转换为 TTImp。
在细化之后有一个单独的线性检查，它会更新孔的类型（并且知道 case 块）。这是在 Core.LinearCheck 中实现的。在此检查期间，我们还重新计算孔应用程序中的多重性，以便它们正确显示（例如，如果线性变量在其他地方未使用，它将始终以多重性 1 出现在孔中）。
目录结构：
Core/-- 与核心 TT、类型检查和 unification 相关的任何内容TTImp/-- 与隐式 TT 及其详细说明相关的任何内容TTImp/Elab/-- 细化状态和细化术语TTImp/Interactive/-- 交互式编辑基础设施
Parser/-- 用于解析和词法分析 TT 和 TTImp（以及其他东西）的各种实用程序Utils/-- 一些通常有用的实用程序Idris/-- 任何与高级语言相关的东西，翻译成 TTImpIdris/Elab/-- 高级构造细化机制（例如接口）
Compiler/-- 编译器后端
核心类型和参考
Core 是一个 “monad”（不是真的，出于效率的原因，目前...）支持 Error 和 IO (我最初确实计划允许将此限制到一些特定的 IO 操作，但尚未完成）。原始语法由 RawImp 类型定义，该类型在每个节点都有一个源位置，详细说明中的任何错误都会记录错误发生点的位置，作为文件上下文 FC 。
Ref 本质上是一个 IORef 。通常我们会隐式传递它们并使用标签来区分我们的意图。有关它们的定义，请参见 Core.Core 。再一次， IORef 是为了提高效率——即使使用 state monad 会更整洁，但结果却快了大约 2-3 倍，所以我选择了 “丑陋” 的选择......
术语表示
核心语言中的术语由作用域内的名称列表索引，最近定义的优先：
data Term : List Name -> Type
这意味着术语总是有恰当的作用域，我们可以使用类型系统来保持我们在操作名称时的正确性。例如，我们有：
Local : FC -> (isLet : Maybe Bool) ->
(idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars
因此，局部变量由局部上下文中的索引（de Bruijn 索引 idx ）表示，并在运行时擦除该索引有效的证明。所以一切都被 de Bruijn 索引了，但是类型检查器仍然跟踪索引，这样我们就不必想太多了！
Core.TT 包含各种方便的工具，用于使用它们的索引来操作术语，例如：
weaken : Term vars -> Term (n :: vars) -- actually in an interface, Weaken
embed : Term vars -> Term (ns ++ vars)
refToLocal : (x : Name) -> -- explicit name of a reference
(new : Name) -> -- name to bind as
Term vars -> Term (new :: vars)
请注意，类型明确说明何时需要在运行时传递 vars ，何时不需要。大多数需要它的地方是帮助显示名称或名称生成，而不是核心中的任何基本原因。一般来说，这在运行时并不昂贵。
在 Core.Env 中定义的环境变量将局部变量映射到绑定器：
data Env : (tm : List Name -> Type) -> List Name -> Type
绑定器通常是 lambda、pi 或 let*（带值），也可以是 *模式变量。更多细节见 TT 的定义。通常有 term 的地方也需要 Env。
我们还有值（value），它们处于头部标准形（head normal form），在 Core.Value 中定义：
data NF : List Name -> Type
我们可以通过归约（normalising）将 term 转换为 value...
nf : {vars : _} ->
Defs -> Env Term vars -> Term vars -> Core (NF vars)
...也可以通过 quoting 反向转换：
quote : {vars : _} ->
Defs -> Env Term vars -> tm vars -> Core (Term vars)
nf 和 quote 都定义在 Core.Normalise 中。我们并不总是知道需要处理 NF 还是 Term，因此还引入了一种“粘合”（glued）表示 Glued vars，同样定义在 Core.Normalise，可按需惰性计算为 NF 或 Term。对 term 进行 elaboration 时，返回的类型就是 Glued vars。
Term 区分了 ``Ref``（全局用户自定义名称）和 ``Meta``（全局定义的元变量）。为提高效率，只有当元变量的多重性不为 0 时，才会将其替换进 term，以尽可能保留共享。
统一（Unification）
统一（unification）可能是 elaboration 过程中最重要的部分，用于推断隐式参数的值。即为 Term 中 Meta 所引用的内容寻找具体值。其定义在 Core.Unify，顶层统一函数类型如下：
unify : Unify tm =>
{vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
UnifyInfo ->
FC -> Env Term vars ->
tm vars -> tm vars ->
Core UnifyResult
之所以有 Unify 接口，是为了方便对 Term、NF 以及 Closure``（``NF 的一部分，用于表示构造器的未求值参数）定义统一操作。
这正是对 vars 进行索引极为重要的地方：我们必须保持环境一致，这样统一过程就不会意外引入作用域错误！
Idris 2 实现了模式统一（pattern unification）——可参考 Adam Gundry 的论文获得易懂的介绍。
上下文（Context）
Core.Context 定义了 TT 所需的所有内容。最重要的是：Def 提供名称的定义（主要是 case 树、内建、构造器和 hole）；GlobalDef 是包含所有其他信息（类型、可见性、完备性等）的定义；Context 是将名称映射到 GlobalDef 的上下文，Defs 是包含类型检查更多定义所需一切的核心数据结构。
主 Context 类型将定义存储在数组中，通过"已解析名称 id"（整数）索引，以便快速查找。这也意味着需要能够在已解析名称和完整名称之间转换。HasNames 接口定义了在可读名称结构和已解析整数名称结构之间相互转换的方法。
由于名称存储在数组中，所有查找函数都需要在 Core monad 中实现。这也有助于加载已检查文件（见下文）。
细化（Elaboration）概述
将 RawImp 细化为 TT 由 TTImp.Elab 驱动，细化 term 的顶层函数定义在 TTImp.Elab.Term，支持函数定义在 TTImp.Elab.Check，各种 TTImp 结构的细化器定义在 TTImp.Elab.* 下的独立文件中。
惰性（Laziness）
与 Idris 1 类似，惰性在类型中用 Lazy、Delay 和 Force 标记，对于 codata 用 Inf``（代替 ``Lazy）。与 Idris 1 不同，这些是语言原语而非特殊名称。
隐式惰性解析在统一（Core.Unify）过程中处理。当以 withLazy 标志调用统一（由 TTImp.Elab.Check 中的 convert 调用）时，会检查是否在将惰性类型转换为非惰性类型。如果是，则继续统一，但会返回需要插入 Force 或 Delay。
TTC 格式
如果为其实现了 TTC 接口，就可以将内容保存为二进制。具体做法见 Utils.Binary。其底层使用 Data.Buffer 的全局引用 Ref Bin Binary。
加载已检查的 TTC 文件时，不会立即处理定义，而是将其存储为 ContextEntry，要么是 Binary 二进制块，要么是已处理的定义。只有首次查找时才处理定义，因为将二进制转换为定义的开销较大（需构造大量 AST 节点），而且导入文件中的定义往往不会被用到。
绑定隐式参数（Bound Implicits）
RawImp 类型有一个构造器 IBindVar。首次遇到 IBindVar 时，会将其名称记录为将被隐式绑定的名称。细化结束时，通过查看作为 IBindVar 绑定的名称列表及其依赖关系，并按依赖顺序排序，决定哪些 hole 应转为绑定变量（类型中的 Pi 绑定、左侧的 Pattern 绑定、右侧仍为 hole）。此过程在 TTImp.Implicit.getToBind 中实现。
确定需要绑定哪些隐式参数后，在 bindImplicits 中进行绑定。任何代表绑定隐式参数的 hole 的应用都会转为局部绑定（类型为 Pi 或 Pat，@-pattern 用 PLet）。
未绑定隐式参数（Unbound Implicits）
任何以小写字母开头的名称都视为未绑定隐式参数。它们在细化时被 elaboration 为 hole，可能依赖于初始环境，细化后会被转换为多重性为 0 的隐式 pi 绑定。例如：
map : {f : _} -> (a -> b) -> f a -> f b
变为：
map : {f : _} -> {0 a : _} -> {0 b : _} -> (a -> b) -> f a -> f b
绑定顺序按依赖关系排列。它会自动推断额外名称，例如：
lookup : HasType i xs t -> Env xs -> t
...其中 xs 是 Vect n a，会自动推断 n 和 a 的绑定。
%unbound_implicits 指令表示不再自动绑定名称（如上例 map 中的 a 和 b），但仍会为额外名称推断类型，例如：
lookup : forall i, x, t . HasType i xs t -> Env xs -> t
...它仍会为 xs 推断类型，并推断 n 和 a 的绑定。
隐式参数（Implicit arguments）
遇到隐式参数（原始语法中的 _，或在细化应用时发现需要隐式参数而添加）时，会创建一个新 hole，即在当前环境下应用的新名称，并将其作为细化后的 term 返回。此过程在 TTImp.Elab.Check 的 metaVar 函数中实现。如果其他地方信息足够，会通过统一找到 hole 的定义。
在细化过程中不会替换 term 中的 hole，若需查看其内部则依赖归约（normalisation）。若定义细化后仍有 hole，需报错（类型中的 hole 只要在定义完成前被解决即可）。
可查看 Elab.App.makeImplicit、Elab.App.makeAutoImplicit，了解在应用中为隐式参数添加 hole 的位置。
Elab.App 做了很多复杂的工作！为帮助解析歧义名称和记录更新，有时会延迟参数的细化（见 App.checkRestApp），以便先获取更多类型信息。
Core.Unify.solveConstraints 会重新检查所有当前未解决的 hole 和受约束的定义，并再次尝试统一它们所需的约束。同时也会尝试解决由 proof search 定义的内容。统一的当前状态定义在 Core.UnifyState，统一约束会记录哪些元变量阻塞了它们。这提升了性能，因为只有当阻塞元变量之一被解决时才会重试约束。
额外类型推断（Additional type inference）
类型中的 ? 表示"推断此部分类型"。这与类型中的 _ 不同，后者表示"我不关心这是什么"。两者的区别在于推断失败时的处理。若 _ 推断失败，会隐式绑定新名称（类似左侧的模式匹配，即匹配任意内容）；若 ? 推断失败，则保留为 hole，稍后再尝试填充。因此，可以这样写：
foo : Vect ? Int
foo = [1,2,3,4]
...此时 ? 会被推断为 4。但如果这样写：
foo : Vect _ Int
foo = [1,2,3,4]
...则会报错，因为 _ 被绑定为新名称。? 和 _ 在 RawImp 中都由 Implicit 构造器表示，带有一个布尔标志，表示"未解决时绑定"。
因此，_ 在左侧和类型中的含义现在是一致的（即推断值，推断失败时绑定变量）。实际使用中，_ 会得到 Idris 旧有行为，而 ? 能获得更多类型推断。
自动隐式参数（Auto Implicits）
自动隐式参数通过 proof search 解析，也可以像普通隐式参数一样显式传参：即用 {x = exp} 指定 auto implicit x 的值。接口（interface）是自动隐式参数的语法糖（解析机制相同——接口会转为 record，实现会转为搜索提示）。
参数语法 @{exp} 表示应用中的下一个自动隐式参数取值为 exp——这与 Idris 1 中调用具名实现的语法相同，但现在接口和自动隐式参数已合并。
隐式参数搜索定义在 Core.AutoSearch。只有当目标的所有*决定性参数*都已确定（即不包含任何 hole）时才会开始搜索。这避免了过早通过搜索（而非统一）解决 hole，除非程序员通过数据类型上的 search 选项明确要求。
点模式（Dot Patterns）
IMustUnify 是 RawImp 的一个构造器。细化时会生成一个 hole，然后细化 term，并添加约束，要求生成的 hole 必须与显式给定的 term 统一（在 UnifyState.addDot 中），但不解决任何 hole。最终在 UnifyState.checkDots 中检查。
证明搜索（Proof Search）
用 Core.Context.BySearch 构造的定义是一个 hole，将通过搜索符合类型的内容来解决。这在 Core.AutoSearch 中实现。它会检查 term 的所有可能提示，确保只有一个可行。
@-模式（@-Patterns）
类型中绑定的名称也会作为 @-模式绑定，意味着函数可以访问它们。例如，可以这样写：
vlength : {n : Nat} -> Vect n a -> Nat
vlength [] = n
vlength (x :: xs) = n
as 模式实现为 TT 的一个构造器，这让许多事情更方便（尤其是 case 树编译）。
线性类型（Linear Types）
根据 Conor McBride 和 Bob Atkey 的工作，所有绑定器都有多重性（RigCount）注解。在 TTImp.Elab 细化后，会单独进行线性检查：a）确保线性变量正好被使用一次；b）更新 hole 类型以正确反映使用信息。
局部定义（Local definitions）
细化时是相对于某个环境进行的，这意味着可以细化局部函数定义。会跟踪嵌套声明块中正在定义的名称，并确保通过应用到作用域内的每个名称，将它们提升为 TT 的顶层定义。
由于无法预知局部定义会被应用多少次，通常所有多重性为 1 的绑定都会以多重性 0 传递给局部定义，因此若要在局部定义中使用它，需要显式传递。
case 块（Case blocks）
与局部定义类似，case 块也会被提升为顶层定义，代表 case 块，并立即应用于 case 的被检对象。细化 case 块时不会尝试计算参数的多重性，因为很可能会出错——而是在后续的线性检查阶段处理，线性检查器了解 case 函数。
局部定义作用域内的 case 块较为棘手，因为名称需要对应，类型可能被细化，但仍需将局部名称应用到其定义时的作用域。这比较繁琐，通过 RawImp 的 ICaseLocal 构造器处理。
系统的多个部分会对 case 块做特殊处理，尽管它们并非严格属于核心内容。尤其是线性检查和完备性检查。
参数（Parameters）
数据类型的参数被视为在数据定义中各处以相同位置、不变出现的参数。
擦除（Erasure）
未绑定隐式参数的多重性为 0，因此现在的规则是：如果你没有在函数或构造器类型中显式写出参数，该参数将在运行时被擦除。
细化和 case 树编译器检查确保 case 树中不会检查多重性为 0 的参数。编译器会完全擦除构造器的 0-多重性参数，而函数的 0-多重性参数会被替换为占位的擦除值。
命名空间与名称可见性（Namespaces and name visibility）
规则基本与 Idris 1 相同。不同之处在于可见性是*按命名空间*而非*按文件*（即文件本身无关紧要，除了引入自己的命名空间和允许单独类型检查）。
这样做的一个结果是：当文件定义嵌套命名空间时，内层命名空间可以访问外层命名空间的内容，反之则不行，除非内层命名空间中定义的名称被显式导出。可见性修饰符 export、public export 和 private 控制名称是否能被其他命名空间访问，与其定义所在文件无关。
与 Idris 1 不同，公共定义是否引用私有名称没有限制。唯一的限制是 private 名称不能在命名空间外被直接引用（即不能在代码中引用）。
记录（Records）
记录属于 TTImp（而非表层语言）。细化 record 声明会创建一个数据类型及其相关投影函数。record 的 setter 在细化 TTImp 时按需生成（在 TTImp.Elab.Record 中）。setter 会直接转为 case 块，这意味着依赖字段的更新会如预期那样工作（即只要所有字段同时一致地更新就是安全的）。