There should be level-polymorphic versions of the combinators in `Data.List.Categorical`

[laMudri]

The definitions of RawFunctor, RawApplicative, &c, by necessity, make it so that their fields (like _<$>_) only work on functions between types at the same level. This means, for example, that the _⊛_ we get from applicative in Data.List.Categorical has type ∀ {ℓ} {A B : Set ℓ} → List (A → B) → List A → List B. However, it would be convenient to have a definition of _⊛_ somewhere with type ∀ {a b} {A : Set a} {B : Set b} → List (A → B) → List A → List B.

Probably these definitions should go in Data.List.Base, though this would probably break any code using the categorical combinators because of name clashes.

There are probably similar problems in all of the other Categorical modules, but I haven't had a look at them yet.

[gallais]

Yep. See for instance the level polymorphic _>>=_ in Data.Maybe.Base.

[laMudri]

Another funny thing is that RawMonad is not a subclass of RawApplicative, so the _⊛_ coming from monad is different to the one coming from applicative. When I tried just using the definition from applicative, it broke some proofs.

[gallais]

I'd argue that is a bug that we should definitely fix in version 2.0.

[MatthewDaggitt]

I'd argue that is a bug that we should definitely fix in version 2.0.

@laMudri maybe open a new issue for it?

[laMudri]

#952

[MatthewDaggitt]

If people are keen to include this in v1.2 as the milestone suggests, could someone open a PR in the next couple of days?

[JacquesCarette]

It's easy enough to hand-code something, but that feels like cheating (and non-scalable). I do have a more level-polymorphic RawFunctor, but RawApplicative has resisted all my attempts at generalization.