Idris 2能否像Haskell一样将中缀运算符作为参数名使用？

Idris 2 支持将二元函数作为中缀运算符使用，语法和 Haskell 存在差异，你遇到的报错可以通过两种方式解决：

• 方案1：使用反引号包裹函数名实现中缀调用
  这是最简便的写法，不需要额外声明运算符属性，示例代码如下：

  f : (Int -> Int -> Int) -> Int
  f op = 3 `op` 4
  

  调用时传入任意二元Int运算即可正常执行，例如f (+)的返回结果为7。

• 方案2：显式声明局部运算符的固定性
  如果你希望直接用|+|作为参数名并以中缀形式调用，需要在where块中声明该运算符的结合性和优先级，示例代码如下：

  f : (Int -> Int -> Int) -> Int
  f (|+|) = 3 |+| 4
    where
      infixl 6 |+|
  

  这里infixl 6表示该运算符为左结合，优先级为6，和Idris内置的+运算符优先级保持一致，你可以根据需求调整结合性和优先级数值。

你原本的代码报错是因为Idris 2 不会像Haskell一样自动将参数列表中括号包裹的符号识别为合法中缀运算符，必须显式声明其固定性，或者改用反引号调用的形式。

内容的提问来源于stack exchange，提问作者Cactus