More granular hierarchy

[joneshf]

How would we feel about making the Functor hierarchy a little more granular? I.e. following PS's lead rather than Haskell's. We could go from:

to:

The impetus for this issue is that when trying to address #52, it's worlds easier if we have List/extend/List/duplicate. List cannot be a Comonad (because there's no way to implement extract). List can be a very useful Extend though. There are many other data types that make great Applys/Binds/Extends that don't necessarily have the right structure to implement Applicative/Monad/Comonad.

[sellout]

Yeah, I am all for this. map2 (aka liftA2), join, and duplicate are the semigroup operation of the Applicative, Monad, and Comonad (co)monoids, respectively. And ap, bind, and extend can be defined in terms of those semigroup operations, so it’s a reasonable separation.

(Ideally, I’d say the type classes should have map2, join, and deplicate as their operations, with the others derived, but reasonable people differ.)

[FintanH]

Ya I'm totally up for this for 3 reasons

1. It will make defining dhall-bhat in terms of kind-poly easier
2. Can document as we split out these main pieces
3. You're dead right about functionality around extend and duplicate

[FintanH]

Is worth having Pointed as well? The graph above would be Applicative <- (Pointed, Apply)

laws:

• fmap f . point === point . f
• fmap point === point

[joneshf]

I'll have a think about the first one, but the second one seems like it might not always hold. E.g., if point :: a -> [a] then:

fmap point [1, 2, 3]
  = [[1], [2], [3]]
  /= [[1, 2, 3]]
  = point [1, 2, 3]

[FintanH]

Ah good point! I was thinking of Optional when I was riffing on it.

[FintanH]

lmao https://wiki.haskell.org/Why_not_Pointed%3F

(he still provides the pointed package only because “people were whinging”).

[FintanH]

Seems like it's not as useful as I thought according to Kmett, so maybe it's best left out unless you can think of anything :) fwiw Kmett says the first law is a free theorem so that's all G :ok_hand:

[sellout]

Yeah, I’m sympathetic to wanting Pointed, but it ends up being “Default in the category of endofunctors”.

[FintanH]

Ran into a roadblock when prototyping this work.

We can't do Applicative f //\\ Bind f because they share fields. We also can't project fields for type records :(

One workaround is have Monad/Type be defined as Bind f //\\ { pure : forall(a : Type) -> a -> f a }

[joneshf]

Huh, I wonder why there isn't a "prefer" operator for types–like // for terms.