title: In Idris, why do interface parameters have to be type or data constructors?
body: <p>To get some practice with Idris, I've been trying to represent various basic algebraic structures as interfaces. The way I thought of organizing things at first was to make the parameters of a given interface be the set <em>and</em> the various operations over it, and the methods/fields be proofs of the various axioms. For example, I was thinking of defining <code>Group</code> like so:</p>
  
  <pre><code>Group (G : Type) (op : G -&gt; G -&gt; G) (e : G) (inv : G -&gt; G) where
    assoc : {x,y,z : G} -&gt; (x `op` y) `op z = x `op` (y `op` z)
    id_l  : {x : G} -&gt; x `op` e = x
    id_r  : {x : G} -&gt; x `op` e = x
    inv_l : {x : G} -&gt; x `op` (inv x) = e
    inv_r : {x : G} -&gt; (inv x) `op` x = e
  </code></pre>
  
  <p>My reasoning for doing it this way instead of just making <code>op</code>, <code>e</code>, and <code>inv</code> methods was that it would be easier to talk about the same set being a group in different ways. Like, mathematically, it doesn't make sense to talk about a set being a group; it only makes sense to talk about a set with a specified operation being a group. The same set can correspond to two completely different groups by defining the operation differently. On the other hand, the proofs of the various interface laws don't affect the group. While the inhabitants (proofs) of the laws may be different, it doesn't result in a different group. Thus, one would have no use for declaring multiple implementations.</p>
  
  <p>More fundamentally, this approach seems like a better representation of the mathematical concepts. It's a category error to talk about a set being a group, so the mathematician in me isn't thrilled about asserting as much by making the group operation an interface method.</p>
  
  <hr>
  
  <p>This scheme isn't possible, however. When I try, it actually <em>does</em> typecheck, but as soon as I try to define an instance, it doesn't: idris complains that e.g.:</p>
  
  <pre><code>(+) cannot be a parameter of Algebra.Group
  (Implementation arguments must be type or data constructors)
  </code></pre>
  
  <p>My question is: why this restriction? I assume there's a good reason, but for the life of me I can't see it. Like, I thought Idris collapses the value/type/kind hierarchy, so there's no real difference between types and values, so why do implementations treat types specially? And why are data constructors treated specially? It seems arbitrary to me.</p>
  
  <hr>
  
  <p>Now, I could just achieve the same thing using named implementations, which I guess I'll end up doing now. I guess I'm just used to Haskell, where you can only have one instance of a typeclass for a given datatype. But it still feels rather arbitrary.... In particular, I would like to be able to define, e.g., a semiring as a tuple <code>(R,+,*,0,1)</code> where <code>(R,+,0)</code> is a monoid and <code>(R,*,1)</code> is a monoid (with the distributivity laws tacked on). But I don't think I can do that very easily without the above scheme, even with named implementations. I could only say whether or not R is a monoid---but for semirings, it needs to be a monoid in two distinct ways! I'm sure there are workarounds with some boilerplate type synonyms or something (which, again I'll probably end up doing), but I don't really see why that should be necessary.</p>
  
  <hr>
  
  <pre><code>$ idris --version
  1.2.0
  </code></pre>