Support implicit indexes in interfaces

[spcfox]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Motivation

I am currently developing a library with proofs in Idris 2. I want to define an interfaces like this:

interface LawfulSemigroup m {auto 0 semigroup : Semigroup m} where
  -- ...

interface LawfulMonoid m {auto 0 monoid : Monoid m} where
  lawfulSemigroup : LawfulSemigroup m
  -- ...

But interfaces doesn't support implicit indexes. I can use constraints like this:

interface Semigroup m => LawfulSemigroup m where
  -- ...

interface Monoid m => LawfulSemigroup m => LawfulMonoid m where
  -- ...

But this is a bad definition, because it does not guarantee that Monoid and LawfulSemigroup use the same Semigroup instance. Such a definition is impossible to use in practice.

At the same time, it makes sense to make these indexes auto, because in most cases you can deduce from the context for which monoid the proof is required.

The proposal

Add support for implicit indexes to interfaces. When desugaring, they are translated to the same record indexes that already support them.

Alternatives considered

You can use records explicitly, but the syntax for interfaces is more convenient. In addition, the interfaces allow for minimal complete implementation. This can be useful for the above example, since it is possible to provide the user with several equivalent sets of laws and allow to prove the most convenient one.

You can make the indexes explicit. But this is inconvenient because we usually don't have named interface instances.

In Lean 4, classes for LawfulFunctor and LawfulApplicative are indexed by implicit Functor and Applicative.

Conclusion

Implicit interface indexes can be useful, which is why I suggest adding support for them.

[andrevidela]

I just noticed this and how it's similar to something I'm already working on, quick question: Why do you want to use the interface mechanism rather than using records? Is it because other languages do this? or because you're doing something with interface resolution? Or something else?

[spcfox]

I just noticed this and how it's similar to something I'm already working on

Oh, I started working on adding this feature a few days ago

Why do you want to use the interface mechanism rather than using records?

I think using interfaces for this seems natural. I see the following advantages:

1. Convenient syntax
   In the record syntax, I can't define a function via pattern-matching. Right now I'm writing something like this:

   public export %hint
   lawfulFunctor : List lawfulFunctor
   lawfulFunctor = MkLawfulFunctor identityLaw compLaw where
     identityLaw : (xs : List a) -> xs === map Prelude.id xs
     identityLaw [] = Refl
     identityLaw (x :: xs) = cong (x ::) $ identityLaw xs
   
     compLaw : (xs : List a) -> map g (map f xs) === map (g . f) xs
     compLaw [] = Refl
     compLaw (x :: xs) = cong (g (f x) ::) $ compLaw xs

   Or like this:

   public export %hint
   lawfulApplicativeMaybe : LawfulApplicative Maybe
   lawfulApplicativeMaybe = MkLawfulApplicative
     { lawfulFunctor = %search
     , mapApplicativeLaw = mapApplicativeLaw
     , identityApLaw = identityApLaw
     , homomorphismLaw = Refl
     , interchangeLaw = interchangeLaw
     , compositionLaw = compositionLaw
     }
   where
     mapApplicativeLaw : (x : Maybe a) -> (Just f <*> x) === map f x
     mapApplicativeLaw $ Nothing = Refl
     mapApplicativeLaw $ Just _ = Refl

2. Default implementations
   Due to them, we can add a law that follows from the others. Or define two equivalent sets of laws and let the user prove which one is more convenient for his type.

3. Constraints
   In the main post I used the lawfulSemigroup method, but I think it should work with constraints as well:

   interface LawfulSemigroup m => LawfulMonoid m {auto 0 monoid : Monoid m}

4. Interface methods take implementation implicitly, unlike record projections. So now I create an alias for each method:

   record LawfulFunctor t {auto 0 functor : Functor t} where
     constructor MkLawfulFunctor
   
     identityLaw : forall a. (xs : t a) -> xs === map Prelude.id xs
   
     compLaw : forall a, b, c. {0 g : b -> c} -> {0 f : a -> b} ->
               (xs : t a) -> map g (map f xs) === map (g . f) xs
   
   identityLaw : (0 _ : Functor t) => LawfulFunctor t => (xs : t a) -> xs === map Prelude.id xs
   identityLaw = %search.identityLaw
   
   compLaw : (0 _ : Functor t) => LawfulFunctor t =>
             (xs : t a) -> map g (map f xs) === map (g . f) xs
   compLaw = %search.compLaw

[andrevidela]

For point number 1, what you're looking for is copattern syntax https://agda.readthedocs.io/en/latest/language/copatterns.html

I'm not quite sure I'm entirely sold on the design of the feature but if you can make it work that would be interesting

[spcfox]

Copatterns looks interesting. Right now I have a working version with implicit parameters in the interfaces. I'll tidy it up and create a PR for discussions

[spcfox]

I'm not quite sure I'm entirely sold on the design of the feature but if you can make it work that would be interesting

As far as I understand, there are no copatterns in Idris2 right now?
If we are talking about a possible design, we can also look at how it is implemented in Arend with the keyword cowith.

[andrevidela]

there are no copatterns in Idris2 right now?

that's right, we still need to implement copatterns