Inconsistent usage/requirement of SListI

[phadej]

For example, zipList_NP requires SListI:

zipWith_NP :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

However, compare_NS and compare_SOP, don't require nor provide one:

compare_NS ::
     forall r f g xs .
     r                             -- ^ what to do if first is smaller
  -> (forall x . f x -> g x -> r)  -- ^ what to do if both are equal
  -> r                             -- ^ what to do if first is larger
  -> NS f xs -> NS g xs
  -> r
  
compare_SOP ::
     forall r f g xss .
     r                                      -- ^ what to do if first is smaller
  -> (forall xs . NP f xs -> NP g xs -> r)  -- ^ what to do if both are equal
  -> r                                      -- ^ what to do if first is larger
  -> SOP f xss -> SOP g xss
  -> r
compare_SOP lt eq gt (SOP xs) (SOP ys) =
  compare_NS lt eq gt xs ys

which requires to use ccompare_NS variants with Top: compare_SOP ... (\xs ys -> ... $ zipList_NP xs ys) doesn't work.

---

I'd prefer a fix where functions which don't require SList (like map_NP and zipWith_NP) won't actually require it (i.e. fix them, not compare_NS). The reasoning being two fold

• Less "linear sized" data passed around (and constructed)
• If zipWith_NP is used on something else than a [Type] kind. Maybe it's [[Type]] or [[[Type]]], maybe there's something not in sop-core (e.g. type-level Maybe with its own All-like class). So zipWith_NP cannot be ever general enough, and then it's better to use czipWIth_NP. But zipWith_NP is stilluseful, when you are not threading any constraints. (Except it isn't know, as SListI needs to be threaded, or recovered from argument NP).

[kosmikus]

I think providing SListI is a good point. We should in general do this.

As to requiring it: I agree that it's nice to avoid passing info that's not needed. At the same time, it's to some extent an implementation detail whether a function requires SListI or not. So omitting it sometimes closes off potential implementation paths. Therefore, I generally find it a bit cleaner if all functions require it. I'm half convinced by your reasoning though.

[edsko]

FWIW, I also would prefer fewer functions to requite SListI.

[phadej]

To avoid missunderstandings: I consider sop-core usable in other domains than just for implmeneting generics-sop. If that's not the goal of sop-core, then we may stop the discussion right here.

---

It's to some extent an implementation detail

It indeed is. But I argue, that if it's possible to not require SListI, then the "default" implementation should not.

Let's take map_NP or zipWith_NP as a concrete example. There are two implementations I can think about

1. naively by manual recursion, no need for SListI.
2. using ana_NP, needs SListI.

In the domain of generics-sop, the latter might be preferable as there is a chance that GHC will unroll the loop, and inline everything. Good.

But in other domains it's not imporant:

• In staged-sop (or any staged programming) we don't really care about that (naive implementation is definitely fast enough).
• In type-indexed heavy use-cases (e.g. evaluator eval :: NP Value ctx -> Term ctx ty -> Val ctx), having to maintain SListI is just inconvenience, there is nothing to gain if something operating on contexts is implemented using ana_NP, as type-level lists will not be known at compile-time.

---

Therefore, I see two good options:

• one option is to provide two modules of NP (NS, ..) functions. One module with as less requirements as possible (cannot be avoided for pure_NP :: ... -> NP f xs), and one where everything consistently is implemented with ana_NP. E.g. in vec there are Data.Vec.Lazy and Data.Vec.Lazy.Inline modules.
• if only one implementation would be preferred, I'd prefer the naive one. The ana_NP one is less generally useful (though probably preferable for generics-sop use-case)

There is an option of using consistently ana_NP, if so, I'll create a "fork" or companion package to have a module which does the opposite.

The current "something is implemented naively and something using ana_NP" is inconsistent and bad. I consider requiring SListI and not using ana_NP is having the "worst" of both approaches. For example, zipList_NP: the implementation is via ap_NP which is implemented using naive recursion - and ap_NP, doesn't require SListI but zipWith_NP does!