运算符（Operators）

Idris2 没有语法块（如 Idris1）或混合型运算符（如 Agda）。相反，它扩展了中缀运算符的能力，使库设计者能够编写领域特定语言（DSL），同时保持错误信息的可控性。

由于运算符不与函数定义直接关联，它们也属于文件命名空间的一部分，并遵循与其他定义相同的规则。

警告

运算符有时会降低代码可读性。请谨慎、合理地使用。本文件主要面向库作者和高级用户。如果你对是否使用运算符犹豫不决，建议谨慎为上，尽量避免使用。

基础（Basics）

在介绍高级特性之前，先说明运算符对大多数用户的基本用法。

当你看到如下表达式时

1 + n

这意味着作用域内有一个函数 (+) 和一个 *fixity*（结合性）声明。该运算符的结合性声明如下：

infixl 8 +

声明以结合性关键字开头，你可以选择 infixl、infixr、infix 或 prefix。

infixl 表示运算符是左结合的，因此连续应用时会向左括号归组：n + m + 3 + x = (((n + m) + 3) + x)。同理，infixr 表示右结合，infix 表示无结合性，此时括号是必须的。这里我们选择 + 为左结合，因此用 infixl。

fixity 后的数字表示运算符的 优先级，即在同一表达式中遇到其他运算符时，是否需要加括号。例如，我们希望 * 的优先级高于 +，可以这样声明：

infixl 9 *

这样，表达式 n + m * x 会被正确解析为 n + (m * x)。

fixity 声明是可选的，会影响文件的解析方式，但你可以用括号包裹任意运算符符号定义的函数来使用它：

-- those two are the same
n + 3
(+) n 3

由于 fixity 与函数定义分离，一个运算符可以有 0 个或多个 fixity 声明。下一节将介绍如何处理多个 fixity 声明。

结合性与优先级命名空间（Fixity & Precedence Namespacing）

有时你可能需要导入两个导出冲突 fixity 的库。此时编译器会发出警告，并选择其中一个 fixity 解析文件。遇到这种情况，你应隐藏不想使用的 fixity 声明。为此，使用 %hide 指令，方法与隐藏函数定义类似，但要在末尾指定 fixity 和运算符。下面举例说明：

module A
export infixl 8 -

module B
export infixr 5 -

module C

import A
import B

test : Int
test = 1 - 3 - 10

该程序会在模块 C 的最后一行发出警告，因为作用域内有两个冲突的 fixity。表达式应解析为 (1 - 3) - 10 还是 1 - (3 - 10)？此时可用 %hide 隐藏不想用的 fixity：

module C

import A
import B

%hide A.infixl.(-)

test : Int
test = 1 - 3 - 10 -- all good, no error

这样程序会被解析为 1 - (3 - 10)，且不会报错。

fixity 的导出修饰符（Export modifiers on fixities）

与语言中的其他顶层声明一样，fixity 可以用 export 修饰符导出，也可以用 private 保持私有。

private fixity 会在本文件剩余部分可用，但对导入该模块的用户不可见。由于 fixity 与运算符分离，这并不意味着你不能用该运算符名的函数，只是不能以中缀形式使用。你仍可用括号以普通函数方式调用。如下所示：

module A

private infixl &&& 8

-- a binary function making use of our fixity definition
export
(&&&) : ...

module B

import A

main : IO ()
main = do print (a &&& b) -- won't work
          print ((&&&) a b) -- ok

下文有两个示例，说明将 fixity 声明为 private 而非 export 的好处。

私有记录 fixity 模式（Private record fixity pattern）

私有 fixity 声明在与记录结合时很有用。当你声明一个以运算符为字段的记录时，使用中缀形式书写很方便。但编译器还会为该字段生成投影函数，其第一个参数为要投影的记录值。这样一来，该运算符就变成了 3 个参数，无法作为二元中缀运算符使用。

infixl 7 <@>

record SomeRelation (a : Type) where
  (<@>) : a -> a -> Type
  -- we use the field here in infix position
  compose : {x, y, z : a} -> x <@> y -> y <@> z -> x <@> z

lteRel : SomeRelation Nat
lteRel = ...

-- we want to use <@> in infix position here as well but we cannot
natRel : Nat -> Nat -> Type
natRel x y = (<@>) lteRel x y

我们真正想写的是 natRel x y = (<@>) x y，但此时 (<@>) 的类型已变为 SomeRelation a -> a -> a -> Type。

解决方法是定义一个带有私有 fixity 的私有字段，以及一个依赖证明搜索自动补全参数的公有字段：

private infixl 7 <!@>
export  infixl 7 <@>

record SomeRelation (a : Type) where
  (<!@>) : a -> a -> Type
  compose : {x, y, z : a} -> x <!@> y -> y <!@> z -> x <!@> z

export
(<@>) : (rel : SomeRelation a) => a -> a -> Type
x <@> y = (<!@>) rel x y

%hint
lteRel : SomeRelation Nat
lteRel = ...

natRel : Nat -> Nat -> Type
natRel x y = x <@> y

我们将 (<@>) 定义为带有隐式参数的投影函数，使其再次可用作二元运算符。

私有本地定义（Private Local definition）

当在模块中重新定义运算符 fixity 时，私有 fixity 定义很有用。比如同时导入多个 DSL，又不希望暴露冲突的 fixity 声明时：

module Coproduct

import Product

-- mark this as private since we don't want to clash
-- with the Prelude + when importing the module
private infixr 5 +

data (+) : a -> a -> Type where
  ...

distrib1 : {x, y, z : a} -> x + y + z -> (x + y) + z

这里 distrib1 明确利用了该运算符的右结合性。

类型绑定运算符（Typebind Operators）

在依赖类型编程中，我们可以定义构造子，其第一个参数是类型，第二个参数是以第一个参数为索引的类型。典型例子是依赖线性箭头：

infixr 0 =@
0 (=@) : (x : Type) -> (x -> Type) -> Type
(=@) x f = (1 v : x) -> f v

但在尝试以中缀形式使用时，必须用 lambda 填充第二个参数：

linearSingleton : Nat =@ (\x => Singleton x)
linearSingleton = ...

我们真正想写的是类似依赖箭头 -> 的语法，但用于线性类型：

linearSingleton : (x : Nat) =@ Singleton x
linearSingleton = ...

如果运算符声明为 typebind，上述语法是允许的。只需在 fixity 声明前加上 typebind 关键字即可。

typebind infixr 0 =@

typebind 是类似 export 的修饰符，两者可以同时使用。

声明为 typebind 的运算符不能再以常规方式使用，写 Nat =@ (\x => Singleton x) 会报错。

这种新语法纯属语法糖，会将 (name : type) op expr 转换为 type op (\name : type => expr)。

由于其自左向右的绑定结构，typebind 运算符只能是 infixr，且优先级为 0。

自动绑定运算符（Autobind Operators）

typebind 运算符允许在运算符左侧绑定一个类型，以便作为第二个参数的索引。但有时第一个和第二个参数之间没有依赖关系，但我们仍希望使用绑定语法，这时可以用 autobind。

例如，在依赖类型编程语言的 DSL 中，Pi 构造子左侧为项，右侧为 lambda：

VPi : Value -> (Value -> Value) -> Value

sig : Value
sig = VPi VStar                 (\fstTy -> VPi
      (VPi fstTy (const VStar)) (\sndTy -> VPi
      fstTy                     (\val1 -> VPi
      (sndTy `vapp` val1)       (\val2 ->
      VSigma fstTy sndTy)))))

我们希望用自定义运算符构造 VPi 的值，但其签名不符合 typebind 的模式。此时可用 autobind，让编译器自动推断 lambda 的类型。为此用 := 替代 :：

autobind infixr 0 =>>
(=>>) : Value -> (Value -> Value) -> Value
(=>>) = VPi


sig : Value
sig =
    (fstTy := VStar) =>>
    (sndTy := (_ := fstTy) =>> VStar) =>>
    (val1 := fstTy) =>>
    (val2 := sndTy `vapp` val1) =>>
    VSigma fstTy sndTy

这种新语法更贴近依赖类型编程语言用户的习惯写法。

更具体地说，任何 autobind 运算符都用 (name := expr) op body 语法调用，并被展开为 expr op (\name : ? => body)。如需显式指定类型，可用完整语法：(name : type := expr) op body，其会被展开为 expr op (\name : type => body)。

与 typebind 类似，autobind 运算符不能再作为常规运算符使用，且 autobind 运算符也不能使用 typebind 语法。