Idris 教程 - 中缀形式的命名实现函数

Question

我正在阅读 named implementations 的教程，其中以 Semigroup Nat 为例：

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

如果我想使用 Plus 定义，(<+>) @{PlusNatSemi} Z (S Z) 可以。但是有没有办法更中缀地写这个？ Z <+> S Z 抱怨缺乏实施，Z <+> @{PlusNatSemi} S Z 和 Z (<+> @{PlusNatSemi}) S Z 都不起作用。

Answer 1

在这种情况下，您需要明确定义要使用的命名实现。

但是 Idris 允许命名实现在默认情况下在带有 using 符号的声明块中可用。因此，在您的示例中，它将是这样的：

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

using implementation PlusNatSemi
  semiPlus : Nat -> Nat -> Nat
  semiPlus x y = x <+> y

using implementation MultNatSemi
  semiMul : Nat -> Nat -> Nat
  semiMul x y = x <+> y

Idris 教程 - 中缀形式的命名实现函数

Idris Tutorial - Functions of named implementations in infix form

syntax

idris