Defining groups in Idris

Question

I defined monoid in Idris as

interface Is_monoid (ty : Type) (op : ty -> ty -> ty) where
    id_elem : () -> ty
    proof_of_left_id : (a : ty) -> ((op a (id_elem ())) = a)
    proof_of_right_id : (a : ty) -> ((op (id_elem ())a) = a)
    proof_of_associativity : (a, b, c : ty) -> ((op a (op b c)) = (op (op a b) c)) 

then tried to define groups as

interface (Is_monoid ty op) => Is_group (ty : Type) (op : ty -> ty -> ty) where
    inverse : ty -> ty
    proof_of_left_inverse : (a : ty) -> (a = (id_elem ()))

but during compilation it showed

When checking type of Group.proof_of_left_inverse:
Can't find implementation for Is_monoid ty op

Is there a way around it.

Answer 1

The error message is a bit misleading, but indeed, the compiler does not know which implementation of Is_monoid to use for your call to id_elem in your definition of proof_of_left_inverse. You can make it work by making it making the call more explicit:

    proof_of_left_inverse : (a : ty) -> (a = (id_elem {ty = ty} {op = op} ()))

---

Now, why is this necessary? If we have a simple interface like

interface Pointed a where
  x : a

we can just write a function like

origin : (Pointed b) => b
origin = x

without specifying any type parameters explicitly.

One way to understand this is to look at interfaces and implementations through the lens of other, in a way more basic Idris features. x can be thought of as a function

x : {a : Type} -> {auto p : PointedImpl a} -> a

where PointedImpl is some pseudo type that represents the implementations of Pointed. (Think a record of functions.)

Similarly, origin looks something like

origin : {b : Type} -> {auto j : PointedImpl b} -> b

x notably has two implicit arguments, which the compiler tries to infer during type checking and unification. In the above example, we know that origin has to return a b, so we can unify a with b.

Now i is also auto, so it is not only subject to unification (which does not help here), but in addition, the compiler looks for "surrounding values" that can fill that hole if no explicit one was specified. The first place to look after local variables which we don't have is the parameter list, where we indeed find j.

Thus, our call to origin resolves without us having to explicitly specify any additional arguments.

Your case is more akin to this:

interface Test a b where
  x : a
  y : b

test : (Test c d) => c
test = x

This will error in the same manner your example did. Going through the same steps as above, we can write

x : {a : Type} -> {b -> Type} -> {auto i : TestImpl a b} -> a
test : {c : Type} -> {d -> Type} -> {auto j : TestImpl c d} -> c

As above, we can unify a and c, but there is nothing that tells us what d is supposed to be. Specifically, we can't unify it with b, and consequently we can't unify TestImpl a b with TestImpl c d and thus we can't use j as value for the auto-parameter i.

---

Note that I don't claim that this is how things are implemented under the covers. This is just an analogy in a sense, but one that holds up to at least some scrutiny.