Idris2
Idris2 copied to clipboard
Redesign Functor interface hierarchy ala Semigroupoids
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
andFoldable1
) - Use
WriterT
to accumulate values with aSemigroup
but noMonoid
instance (List1
, for instance, but alsoFirst
andLast
(both not yet in Idris2), which keep the first or last occurrence of a value).
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
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