Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Redesign Functor interface hierarchy ala Semigroupoids

Open stefan-hoeck opened this issue 3 years ago • 2 comments

Today, I was in need of Alternative for Either e (well, only the <|> part, but that's the whole point). Yet, of course, there is no such thing, as we can't implement empty. The "alt" operator <|>, however, could be implemented and would be very useful. In a similar way, we could have bind (>>=) for map-like structures like Data.SortedMap, but not pure, so there is neither Applicative nor Monad for those.

The Haskell library semigroupoids fixes this by introducing several intermediary typeclasses. The following diagram was shamelessly copied from there:

Foldable ----> Traversable <--- Functor ------> Alt ---------> Plus           Semigroupoid
     |               |            |                              |                  |
     v               v            v                              v                  v
Foldable1 ---> Traversable1     Apply --------> Applicative -> Alternative      Category
                                  |               |              |                  |
                                  v               v              v                  v
                                Bind ---------> Monad -------> MonadPlus          Arrow

So here's my suggestion: As Idris2 is still at a very early state, we could still redesign the interface hierarchy in the Prelude in a similar manner as what's shown above (minus Plus and MonadPlus: We won't need those). The main pain point would of course be, how much such a change would affect bootstrapping, and in what order things would have to be adjusted where (I'll forever struggle with that one :-) ).

Here are two use cases this would allow us to abstract over:

  • Select the first computation not failing with an error from a non-empty list of choices (nees Alt and Foldable1)
  • Use WriterT to accumulate values with a Semigroup but no Monoid instance (List1, for instance, but also First and Last (both not yet in Idris2), which keep the first or last occurrence of a value).

stefan-hoeck avatar Apr 22 '21 10:04 stefan-hoeck

I'd like to mention that transition from Category to Arrow is also too far. I ran into it when using arrow-like classes for invertible computations -- stuff like *** and +++ is useful, but Arrow also requires arr which contradicts reversibility.

An example of gradual Category to Arrow transition can be seen there: https://hackage.haskell.org/package/semi-iso-1.0.0.0/docs/Control-Category-Structures.html

buzden avatar Apr 26 '21 08:04 buzden

If this large refactoring is done, one could also consider including selective functors as a superclass of Monad. In PureScript, one has to use a newtype hack. Otherwise, it seems to me that the PureScript hierarchy is identical to the one from semigroups.

But it's unclear to me if anything can be done here considering Edwin's comment on the PR.

It seems that the law-only MonadOr from the MonadZero reform proposal was not popular enough to warrant inclusion in PureScript:

  • https://github.com/purescript/purescript-control/issues/35

ysangkok avatar Dec 07 '23 01:12 ysangkok