最近在 Idris 中实现了“绑定”应用作为一种语言特性。该特性可更方便地编写依赖对类型等，无需依赖特殊编译器魔法，编译器魔法对所有人可用，此文是此特性使用的集合。此特性尚未公开，但计划近期提供。

什么是它？

绑定语法和绑定应用是几年前的想法，在WITS 2024上提出，是依赖编程语言函数空间上的语法特性，为“绑定”概念提供了一些定制。主要用例是方便编写如(Π)或(Σ)类型，在 Idris 中可将此类函数标记为typebind，其会自动推断类型。

具体使用案例

• Sigma：依赖对或 sigma 类型在依赖类型编程中很常见，定义自己的 sigma 类型时需用 lambda 描述第二个投影的类型，标记为绑定后可使用更自然的语法形式。
• Exists：Idris base库中的Exists类型与依赖对相同，只是第一个参数被擦除，标记为typebind后可写Exists (a : Type) | p a，便于自然数学阅读。
• Subset：base中类似类型，其表示受谓词约束的值，运行时无需携带谓词，标记为typebind后可写Subset (x : Nat) | LTE x 9。
• Ornaments：是类型描述符，Sig和Del可利用绑定应用，重命名并标记为绑定后使用更方便，如装饰Nat描述为Fin n时使用Δ。
• ForAll：base中的All类型，用于对列表中每个元素应用谓词，使用绑定别名可写ForAll (x <- xs) | LTE x 9，使其更易读。
• ForSome：除All外还有Any，用于表示列表中存在一个元素满足谓词，可通过绑定别名实现类似语法。
• For-Loops：在 Idris 中可通过traverse函数定义类似 for 循环的语法，如for (x <- xs) | putStrLn x可模仿其他编程语言的列表迭代语法，ignore丢弃迭代结果。