如何在总计函数中的某个范围内的所有整数上进行匹配？

2024-05-20 • 问答

假设我们要检查Int的奇偶校验：

data Parity = Even | Odd

Nat非常简单：

parity0: Nat -> Parity
parity0 Z = Even
parity0 (S k) = case parity0 k of
  Even => Odd
  Odd => Even

首次尝试为Int实现该目标：

parity1: Int -> Parity
parity1 x = if mod x 2 == 0 then Even else Odd

此功能不完整：

Main.parity1可能不总计，原因是：Prelude.Interfaces.Integral的Prelude.Interfaces.Int实现

这是有道理的，因为mod并非Int的总和。（尽管我不确定如何提前知道它。REPL显示mod是总数。显然，您可以使用部分函数来实现接口的总函数？很奇怪。）

接下来，我尝试使用DivBy视图：

parity2: Int -> Parity
parity2 x with (divides x 2)
  parity2 ((2 * div) + rem) | (DivBy prf) =
    if rem == 0 then Even else Odd

此函数有效并且是完整的，但是该实现容易出错，并且无法扩展到我们具有多个可能值的情况。我想断言rem只能是0或1。所以我尝试在case上使用rem：

parity3: Int -> Parity
parity3 x with (divides x 2)
  parity3 ((2 * div) + rem) | (DivBy prf) = case rem of
    0 => Even
    1 => Odd

此功能也可以使用，但不完整。如何使用prf提供的DivBy来说服编译器的全部信息？我一般如何使用此prf？

是否使用Integer或其他某种类型的字体可以使此问题更易于解决？

还有另一件事非常令人担忧。我尝试对prf进行大小写分割，发现下面的函数是合计的：

parity4: Int -> Parity
parity4 x with (divides x 2)
  parity4 ((2 * div) + rem) | (DivBy prf) impossible

那是个错误吗？我可以使用此函数在仅包含全部函数的程序中产生运行时崩溃。