在 Idris 中，为什么接口参数必须是类型或数据构造函数？

问：

为了练习 Idris，我一直在尝试将各种基本代数结构表示为接口。我最初想到的组织方式是让给定接口的参数成为集合和它上面的各种操作，方法/字段是各种公理的证明。例如，我正在考虑这样定义：Group

Group (G : Type) (op : G -> G -> G) (e : G) (inv : G -> G) where
  assoc : {x,y,z : G} -> (x `op` y) `op z = x `op` (y `op` z)
  id_l  : {x : G} -> x `op` e = x
  id_r  : {x : G} -> x `op` e = x
  inv_l : {x : G} -> x `op` (inv x) = e
  inv_r : {x : G} -> (inv x) `op` x = e

我这样做的原因是，不仅仅是制造 、 和方法，因为以不同的方式谈论同一个集合是一个群会更容易。就像，从数学上讲，谈论一个集合是一个群是没有意义的;只有将具有指定操作的集合讨论为一个组才有意义。通过以不同的方式定义操作，同一集合可以对应于两个完全不同的组。另一方面，各种界面定律的证明不会影响组。虽然法律的居民（证据）可能不同，但这并不会导致不同的群体。因此，声明多个实现是没有用的。opeinv

更根本的是，这种方法似乎更好地代表了数学概念。把一个集合说成一个群是一个类别错误，所以在我心中，数学家对通过将群运算作为接口方法来断言这一点并不感到兴奋。

但是，此方案是不可能的。当我尝试时，它实际上会进行类型检查，但是一旦我尝试定义一个实例，它就没有：idris 抱怨例如：

(+) cannot be a parameter of Algebra.Group
(Implementation arguments must be type or data constructors)

我的问题是：为什么会有这个限制？我想有一个很好的理由，但就我的生命而言，我看不到它。比如，我认为 Idris 折叠了 value/type/kind 层次结构，所以类型和值之间没有真正的区别，那么为什么实现会特别对待类型呢？为什么数据构造函数会受到特殊处理？这对我来说似乎是武断的。

现在，我可以使用命名实现实现相同的目标，我想我现在最终会这样做。我想我只是习惯了 Haskell，对于给定的数据类型，您只能有一个类型类的实例。但它仍然感觉相当武断......特别是，我希望能够将半环定义为元组，其中是幺半群并且是幺半群（附加了分配律）。但我认为如果没有上述方案，即使使用命名实现，我也不能很容易做到这一点。我只能说 R 是否是幺半群---但对于半环来说，它需要以两种不同的方式成为幺半群！我敢肯定有一些样板类型同义词或其他东西的解决方法（我可能最终会这样做），但我真的不明白为什么这应该是必要的。(R,+,*,0,1)(R,+,0)(R,*,1)

$ idris --version
1.2.0