Use instance fields for superclasses (?)

[jespercockx]

I found that the current way of defining a class that has a superclass does not play nice with instance search. Here is a small example using the Alternative typeclass and its ApplicativeZero superclass:

open import Data.List.Base using (List; []; _∷_; [_])
open import Function.Base
open import Level using (Level)

open import Category.Functor renaming (RawFunctor to Functor)
open import Category.Applicative
  renaming ( RawApplicative     to Applicative
           ; RawApplicativeZero to ApplicativeZero
           ; RawAlternative     to Alternative
           )
open Functor         {{...}} using (_<$>_)
open Applicative     {{...}} using ()
open ApplicativeZero {{...}} using () renaming (∅ to empty)
open Alternative     {{...}} using () renaming (_∣_ to _<|>_)

variable
  ℓ ℓ′ : Level
  A B C : Set ℓ
  F M : Set ℓ → Set ℓ′

choice1 : {{_ : Alternative F}} → List (F A) → F A
choice1 []       = empty
  where instance applicativeZeroF = Alternative.applicativeZero it
choice1 (f ∷ []) = f
choice1 (f ∷ fs) = f <|> choice1 fs

This example is accepted, but it is awkward to have to declare the instance applicativeZeroF locally.

In the Agda user manual, it is recommended to use instance fields for encoding superclasses: https://agda.readthedocs.io/en/v2.6.2/language/record-types.html#instance-fields. Unfortunately Agda currently does not provide a way to change a normal field to an instance field when importing a module. So the only solution I can see is to change the definition of these record types in the standard library to use instance fields from the beginning. Making these fields into instance fields should not change anything for people not using instance search, except that the type of the record constructor changes. But actually RawIAlternative currently does not have a record constructor, so AFAICT the change should be 100% backwards compatible.

Also pinging @UlfNorell since he might know alternative solutions.

[MatthewDaggitt]

So concretely you'd be proposing turning the definition of RawIApplicativeZero into the following?

record RawIApplicativeZero
       {I : Set i} (F : IFun I f) :
       Set (i ⊔ suc f) where
  field
    {{applicative}} : RawIApplicative F
    ∅               : ∀ {i j} → F i j A

  open RawIApplicative applicative public

I have no particular problems with that. My main question is how this would be extended to other superclasses? For instance in Relation.Binary.TypeClasses it would be nice to be able to get _≟_ from DecTotalOrder as well. And eventually I guess the algebra classes. Should all IsX structures within other IsX structures be made instance arguments? Presumably we're going to have start thinking about overlapping keywords as well.

[jespercockx]

You're right, these would eventually have to be changed as well to be (more) useful with instance search. And having overlap on these fields would indeed be useful as well. Like I said, it is a bit unfortunate that Agda doesn't provide a way to make fields into instance fields post hoc. Perhaps it would be worthwhile to consider if we could add such a feature to Agda instead of changing the library.

[jespercockx]

Some superclasses (such as the Functor superclass of Applicative) are not defined as fields at all, but are instead defined in terms of the functions of the subclass. So here the strategy of turning fields into instance fields would not even apply. Perhaps there is some way this "forward search" part of the instance search could be made more extensible.

[omelkonian]

I think it's important to contrast two different approaches to declaring superclasses and choose one for the standard library after careful consideration.

Here's an example of the Eq typeclass and two subclasses:

private variable A : Set; x y : A

-- 1) using `overlap {{super}}`
module 𝟙 where

  record Eq (A : Set) : Set₁ where
    field _≈_ : Rel₀ A
  open Eq ⦃...⦄

  record DecEq (A : Set) : Set₁ where
    field
      overlap ⦃ super ⦄ : Eq A
      _≈?_ : Decidable² _≈_
  open DecEq ⦃...⦄

  record Equiv (A : Set) : Set₁ where
    field
      overlap ⦃ super ⦄ : Eq A
      ≈-equiv : IsEquivalence {A = A} _≈_
  open Equiv ⦃...⦄

  instance
    _ = Eq ℕ    ∋ λ where ._≈_ → _≡_
    _ = DecEq ℕ ∋ λ where .super → it; ._≈?_ → Nat._≟_

  _ = True (15 ≈? (6 + 9))
    ∋ tt

  _ : ⦃ DecEq A ⦄ → Eq A
  _ = it

  -- **ERROR** (Equiv.super _ Eq.≈ x) x₁ != (_ Eq.≈ x) x₁ of type Set
  -- _ : ⦃ _ : Eq A ⦄ → ⦃ DecEq A ⦄ → ⦃ Equiv A ⦄ → 
  --   Decidable² {A = A} _≈_ × IsEquivalence {A = A} _≈_
  -- _ = _≈?_ , ≈-equiv

-- 2) using parametrised records
module 𝟚 where

  record Eq (A : Set) : Set₁ where
    field _≈_ : Rel₀ A
  open Eq ⦃...⦄

  record DecEq (A : Set) ⦃ _ : Eq A ⦄ : Set₁ where
    field _≈?_ : Decidable² _≈_
  open DecEq ⦃...⦄

  record Equiv (A : Set) ⦃ _ : Eq A ⦄ : Set₁ where
    field ≈-equiv : IsEquivalence _≈_
  open Equiv ⦃...⦄

  instance
    _ = Eq ℕ ∋ λ where ._≈_ → _≡_

    _ : DecEq ℕ
    _ = λ where ._≈?_ → Nat._≟_

  _ = True (15 ≈? (6 + 9))
    ∋ tt

  -- **ERROR** No instance of type Eq A was found in scope.
  -- _ : ⦃ DecEq A ⦄ → Eq A
  -- _ = it

  _ : ⦃ _ : Eq A ⦄ → ⦃ DecEq A ⦄ → Eq A
  _ = it

  _ : ⦃ _ : Eq A ⦄ → ⦃ DecEq A ⦄ → ⦃ Equiv A ⦄ →
    Decidable² {A = A} _≈_ × IsEquivalence _≈_
  _ = _≈?_ , ≈-equiv

Approach (1): superclass as an instance field overlap ⦃ super ⦄ : Eq A

• Pro: we automatically get an Eq instance out of a DecEq instance
• Con: when the context contains instances for two distinct subclasses, we get into trouble identifying which relation they are referring to

Approach (2): superclass as an instance parameter ⦃ _ : Eq A ⦄

• Pro: works for subclasses of a common superclass
• Con: we do not automatically get the superclass instance, hence the need for ⦃ _ : Eq A ⦄ → ⦃ DecEq A ⦄ → ...

[MatthewDaggitt]

We're planning to reorganise Effect.Functor etc. in v2.0 and will come back to this after this...