视图与“`with`”规则

依值模式匹配（Dependent pattern matching）

由于类型可以依赖于值，因此某些参数的形式可以由其他参数的值决定。例如，如果我们写出 (++) 的隐式长度参数，可以看到长度参数的形式取决于向量是否为空：

(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) {n=Z}   []        ys = ys
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

如果 [] 情况下的 n 是后继（successor），或者 :: 情况下的 n 是零（zero），那么该定义将不是良类型的。

`with` 规则 —— 匹配中间值

我们经常需要对中间计算的结果进行匹配。Idris 为此提供了 with 规则，这一构造受 Epigram [1] 中的视图（view）启发。它考虑到，在依值类型语言中对某个值进行匹配，可能会影响我们对其他值形式的认知。在最简单的形式下，with 规则会为正在定义的函数增加一个参数。

当这个中间计算还出现在正在定义的函数的类型中时，with 构造允许我们捕获这些情况，从而使模式中的观察能够反映到类型上。

我们之前已经见过向量过滤（filter）函数。这一次，我们用 with 规则来定义它，如下所示：

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p [] = ( _ ** [] )
filter p (x :: xs) with (filter p xs)
  filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

在这里，with 子句允许我们解构 filter p xs 的结果。视图细化参数模式 filter p (x :: xs) 位于 with 子句下方，后跟竖线 |，再跟解构后的中间结果 ( _ ** xs' )。如果视图细化参数模式与原始函数参数模式一致，则 | 左侧是多余的，可以用下划线 _ 省略：

filter p (x :: xs) with (filter p xs)
  _ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

with 子句也可以嵌套使用：

foo : Int -> Int -> Bool
foo n m with (n + 1)
  foo _ m | 2 with (m + 1)
    foo _ _ | 2 | 3 = True
    foo _ _ | 2 | _ = False
  foo _ _ | _ = False

如果左侧与父级的模式相同，可以用 _ 省略，只关注最内层 with 的模式。也就是说，上面的 foo 可以重写为如下形式：

foo : Int -> Int -> Bool
foo n m with (n + 1)
  _ | 2 with (m + 1)
    _ | 3 = True
    _ | _ = False
  _ | _ = False

同理，多个用 | 分隔的表达式也可以在一个 with 语句中同时解构：

foo : Int -> Int -> Bool
foo n m with (n + 1) | (m + 1)
  _ | 2 | 3 = True
  _ | _ | _ = False

如果中间计算本身具有依值类型，其结果就会影响其他参数的形式——我们可以通过测试一个值来推断另一个值的形式。在这些情况下，视图细化参数模式必须显式给出。例如，一个 Nat 要么是偶数，要么是奇数。如果是偶数，它就是两个相等 Nat 的和；否则，就是两个相等 Nat 的和再加一：

data Parity : Nat -> Type where
   Even : {n : _} -> Parity (n + n)
   Odd  : {n : _} -> Parity (S (n + n))

我们称 Parity 是 Nat 的一个*视图*（view）。它有一个*覆盖函数*（covering function），用于判断其是偶数还是奇数，并据此构造谓词。注意，我们在运行时需要访问 n，因此尽管它是隐式参数，但其复用性（multiplicity）不受限制。

parity : (n:Nat) -> Parity n

我们稍后会回到 parity 的定义。我们可以用它来编写一个函数，将自然数转换为二进制位列表（最低有效位在前），如下所示，使用 with 规则：

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
   natToBin (j + j)     | Even = False :: natToBin j
   natToBin (S (j + j)) | Odd  = True  :: natToBin j

parity k 的值会影响 k 的形式，因为 parity k 的结果依赖于 k。因此，除了在 | 右侧写出中间计算结果（Even 和 Odd）的模式外，我们还要在左侧写出这些结果如何影响其他模式。即：

当 parity k 计算为 Even 时，我们可以根据 Even 构造子的 Parity (n + n)，将原始参数 k 细化为 (j + j)。因此，(j + j) 替换了 | 左侧的 k，而 Even 构造子出现在右侧。细化模式中的自然数 j 可以在等号 = 右侧使用。
否则，当 parity k 计算为 Odd 时，根据 Odd 构造子的 Parity (S (n + n))，原始参数 k 被细化为 S (j + j)，而 Odd 出现在 | 右侧，同样细化模式中的自然数 j 可在等号右侧使用。

注意，模式中出现了函数（+）和重复的 j，这是允许的，因为另一个参数已经决定了这些模式的形式。

定义 `parity`

parity 的定义稍显复杂，需要一些定理证明（theorem proving）知识（参见定理证明），但为完整起见，现附上如下：

parity : (n : Nat) -> Parity n
parity Z = Even {n = Z}
parity (S Z) = Odd {n = Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j))) | Even
      = rewrite plusSuccRightSucc j j in Even {n = S j}
  parity (S (S (S (j + j)))) | Odd
      = rewrite plusSuccRightSucc j j in Odd {n = S j}

关于 rewrite 的详细内容，请参阅定理证明教程定理证明。

视图与“with”规则

依值模式匹配（Dependent pattern matching）

with 规则 —— 匹配中间值

定义 parity

视图与“`with`”规则

`with` 规则 —— 匹配中间值

定义 `parity`