Multi-Parameter Sub-Classes in Idris
<p>Inspired by <a href="http://sitr.us/2014/05/05/category-theory-proofs-in-idris.html" rel="noreferrer">this blog post</a> and <a href="https://github.com/TimRichter/CId/blob/master/Category.lidr" rel="noreferrer">this code</a> I thought I'd try some category theory in Idris using its interfaces (type-classes).</p>

<p>I defined <code>Category</code> as follows, which works fine:</p>

<pre><code>interface Category (obj : Type) (hom : obj -&gt; obj -&gt; Type) where
  id : {a : obj} -&gt; hom a a
  comp : {a, b, c : obj} -&gt; hom b c -&gt; hom a b -&gt; hom a c
</code></pre>

<p>Then, in the spirit of the <a href="https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Classes/Verified.idr" rel="noreferrer"><code>Verified</code></a> module, I thought I'd define a verified category:</p>

<pre><code>interface Category obj hom =&gt;
          VerifiedCategory (obj : Type) (hom : obj -&gt; obj -&gt; Type) where
  categoryAssociativity : {a, b, c, d : obj} -&gt;
                          (f : hom c d) -&gt; (g : hom b c) -&gt; (h : hom a b) -&gt;
                          (comp (comp f g) h = comp f (comp g h))
  categoryLeftIdentity : {a, b : obj} -&gt; (f : hom a b) -&gt; (comp id f = f)
  categoryRightIdentity : {a, b : obj} -&gt; (f : hom a b) -&gt; (comp f id = f)
</code></pre>

<p>Unfortunately, Idris rejects that code with the following error message:</p>

<pre><code>When checking type of constructor of CategoryTheory.VerifiedCategory:
Can't find implementation for Category obj hom
</code></pre>

<p>Am I doing something wrong, or am I trying to do something with multi-parameter sub-classes that Idris cannot do?</p>

<p>All this code is in its own module, called <code>CategoryTheory</code>, without any imports.</p>

<p>I'm working with Idris v0.12.</p>