Multi-Parameter Sub-Classes in Idris

Question

Inspired by this blog post and this code I thought I'd try some category theory in Idris using its interfaces (type-classes).

I defined Category as follows, which works fine:

interface Category (obj : Type) (hom : obj -> obj -> Type) where
  id : {a : obj} -> hom a a
  comp : {a, b, c : obj} -> hom b c -> hom a b -> hom a c

Then, in the spirit of the Verified module, I thought I'd define a verified category:

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

Unfortunately, Idris rejects that code with the following error message:

When checking type of constructor of CategoryTheory.VerifiedCategory:
Can't find implementation for Category obj hom

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

All this code is in its own module, called CategoryTheory, without any imports.

I'm working with Idris v0.12.

Answer 1

I don't know why (and would be very curious to find out!) but it works if you specify all the implicit arguments to id and comp in VerifiedCategory explicitly. It is pretty ugly and tedious to figure out, but this typechecks:

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

Edit: Another way I just found is to explicitly designate hom as a determining parameter, i.e. the parameter of the type class that is sufficient to find an implementation. This has to happen in Category as well as in VerifiedCategory (I'm not sure, why), like so:

interface Category (obj : Type) (hom : obj -> obj -> Type) | hom where
-- ...

interface Category obj hom => VerifiedCategory (obj : Type) (hom : obj -> obj -> Type) where
-- ...

i.e. by putting a | hom before the where.

One thing you have to do in addition to that is qualify the usage of id in VerifiedCategory, because otherwise it is interpreted as implicit parameter for whatever reason:

  categoryLeftIdentity : {a, b : obj} ->
                         (f : hom a b) ->
                         comp CategoryTheory.id f = f
  categoryRightIdentity : {a, b : obj} ->
                          (f : hom a b) ->
                          comp f CategoryTheory.id = f

See also this reddit thread that might be illuminating in the future.