为普通的旧递归数据类型实现接口

Question

我似乎在与 Idris 语法作斗争。

module Test

data Nat = Z | S Nat

Eq Nat where
  Z == Z = True
  S n1 == S n2 = n1 == n2
  _ == _ = False

这抱怨以下错误（v1.1.1）：

.\.\Test.idr:5:8: error: expected: "@",
    "with", argument expression,
    constraint argument,
    function right hand side,
    implicit function argument,
    with pattern
Eq Nat where
       ^
Type checking .\.\Test.idr

我不明白为什么，我基本上使用了与文档相同的语法。

当我为自定义的非递归类型（例如 Bool）编写 Eq 实现时，它编译得很好。

Answer 1

您需要将S n 模式括在括号中。完成此操作后，您将收到编译器错误，因为Nat 已在Prelude 中定义。因此，要编译您的代码，只需将 Nat 替换为 Natural（或其他任何内容）即可。不过，Z 和 S 构造函数也在 Prelude 中定义，因此您要么需要重命名所有内容才能在 REPL 中轻松测试，要么使用 %hide directive。

但至少这段代码可以编译：

module Test

data Natural = Z | S Natural

Eq Natural where
  Z == Z = True
  (S n1) == (S n2) = n1 == n2
  _ == _ = False