Look into graded monads

[gallais]

We could readily make use of them with Data.Vec and Data.List.All.

[iitalics]

Is this a suitable interface?

module _ {a r} (monoid : Monoid a r) where
  open Monoid monoid

  record GradedMonad {ℓ} (_*_ : Carrier → Set ℓ → Set ℓ)
                     : Set (a ⊔ r ⊔ suc ℓ) where
    field
      subst : ∀ {x y A} → (x ≈ y) → (x * A) → (y * A)
      fmap : ∀ {x A B} → (A → B) → (x * A) → (x * B)
      return : ∀ {A} → A → (ε * A)
      join : ∀ {x y A} → (x * (y * A)) → (x ∙ y) * A

And Vec implemenetation:

VecGMonad : ∀ {ℓ} → GradedMonad *-1-monoid {ℓ} (flip Vec)
VecGMonad = record
  { subst = PEq.subst _
  ; fmap = map
  ; return = [_]
  ; join = concat }

However I'm not sure how Data.List.All fits into this.

[gallais]

Is this a suitable interface?

A few remarks:

• The first constraint can be formulated in terms of Respects
• I think this would be a RawGradedMonad as we are not enforcing any laws.
• I think we could have a ∀ {x} → Functor (x *_) constraint rather than the inlined fmap.
• Similarly, we could ask whether it makes sense to talk about a graded applicative
• Is there a reason to pick a join-based presentation rather than the bind-based one we have for RawMonad?

However I'm not sure how Data.List.All fits into this.

I'm not sure whether they do. These "look into" issues (cf. #480 too) where thrown together during ICFP whenever I saw someone talk about a topic that seemed relevant to us but we had not formalized yet.

It's 100% exploratory work (at least for me) and to pin down a design probably implies including many examples and formalizing results that prove they are usable in practice.

[dm606]

A more general version would be graded by a preordered monoid (using the preorder rather than equivalence relation for subst). This would fit better with e.g. BoundedVec, using Data.Nat._≤_ for the preorder.

• Is there a reason to pick a join-based presentation rather than the bind-based one we have for RawMonad?

The two presentations are equivalent, so I think it would be better to use bind for consistency with RawMonad. Something like this:

module _ {a r₁ r₂} (preorderedMonoid : PreorderedMonoid a r₁ r₂) where
  open PreorderedMonoid preorderedMonoid

  record RawGradedMonad {ℓ} (_*_ : Carrier → Set ℓ → Set ℓ)
                        : Set (a ⊔ r₂ ⊔ suc ℓ) where
    field
      respects : ∀ {A} → (_* A) Respects _∼_
      return : ∀ {A} → A → ε * A
      _>>=_ : ∀ {x y A B} → x * A → (A → y * B) → (x ∙ y) * B

    join : ∀ {x y A} → x * (y * A) → (x ∙ y) * A
    join m = m >>= id

[EdNutting]

Waking up seemingly a very old issue here - have graded monads made their way into the stdlib anywhere? If not, what would be required to do so?

[JacquesCarette]

They're not even in agda-categories yet. A PR there would be great!

[EdNutting]

@JacquesCarette Thank you for letting me know. I only learnt of the existence of graded monads this morning - I'm not yet equipped to tackle such a PR myself. I was rather hoping to be able to "play around with them" in Agda (hence my question on this issue). If I happen to learn enough to come up with a suitable implementation I'll be sure to put in a PR! (but probably someone far more capable than me will get there first!)