Multiparameter subclass in Idris

Question

Inspired by this blog post and this code, I thought that I would try the theory of some categories in Idris using its interfaces (class types).

I defined Categoryas 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 module Verified, I thought I would define a proven 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 this 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 subclasses that Idris cannot do?

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

I work with Idris v0.12.

Answer 1

, ( !), , id comp VerifiedCategory. , , 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)

. , , - hom , .. , . Category, VerifiedCategory ( , ), :

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

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

. a | hom where.

, , - id VerifiedCategory, :

  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

reddit, .