gre*_*Dot 8 math types type-theory interface 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
我对做这种方式，而不是仅仅作出推理op，e和inv方法是，它会更容易谈论相同的一组是用不同的方式的一组。就像从数学上来说，谈论一个集合是一个群体是没有意义的。谈论具有指定操作为组的集合是有意义的。通过不同地定义操作，同一组可以对应于两个完全不同的组。另一方面，各种接口法则的证明不影响组。虽然法律的居民（证据）可能有所不同，但不会导致不同的群体。因此，声明多个实现将毫无用处。
从根本上讲，这种方法似乎更好地表示了数学概念。谈论一个集合是一个组是一个类别错误，因此我本人的数学家对通过将组操作作为接口方法来进行断言并不感到兴奋。
但是，这种方案是不可能的。当我尝试时，它实际上会进行类型检查，但是当我尝试定义一个实例时，它不会：idris抱怨例如：
(+) cannot be a parameter of Algebra.Group
(Implementation arguments must be type or data constructors)
我的问题是：为什么要这样限制？我认为这是有充分理由的，但是对于我的一生，我看不到它。就像，我以为Idris破坏了值/类型/种类的层次结构，因此类型和值之间没有真正的区别，那么为什么实现要特别对待类型呢？为什么要特别对待数据构造函数？对我来说似乎是武断的。
现在，我可以使用命名实现来实现相同的目的，我想我现在将做完。我想我只是习惯了Haskell，对于给定的数据类型，您只能拥有一个类型类的实例。但它仍然感觉相当随意。...特别是，我希望能够将一个半圆环定义为一个元组(R,+,*,0,1)，其中(R,+,0)，一个半体和(R,*,1)一个半体（遵守分配律）。但是我不认为没有上述方案也不能轻易做到这一点，即使使用命名实现也是如此。我只能说R是否是一个单面体-但是对于半环，它需要以两种不同的方式成为一个单面体！我敢肯定有些变通方法可以使用一些样板类型的同义词或类似的东西（我可能最终还是会这样做），但是我没有
$ idris --version
1.2.0