append and split NP

[echatav]

Add functions to append and split n-ary products.

[RyanGlScott]

This is actually exporting the term-level (++) from the Prelude, not the type-level (++) that you defined. I think you intended to export type (++) instead.

[echatav]

Thanks. Fixed! I'm not dedicated to the names btw.

[kosmikus]

Thanks!

Could you provide a bit of motivation of why these functions are required / what your use case is?

I think @phadej wanted to add something similar. Perhaps he could have a look whether the proposed changes are sufficient for his purposes.

The general question I'm uncertain about is whether functions that presumably have no purpose for the "generics" application of n-ary sums and products should go into sop-core, or into a separate package that depends on sop-core, but is not a dependency of generics-sop.

Regarding the actual contribution: according to current naming conventions, the functions should not be called happend and hsplit if they're NP-specific. They should rather be called append_NP and split_NP. However, it's probably possible to define overloaded versions that work at least on POP as well, which could then be called happend and hsplit.

[phadej]

append and split make sense for NS and SOP too:

append_NS :: Either (NS f xs) (NS f ys) -> NS f (Append xs ys)

And indeed, I have Append and Concat and few other type-families with related NS/NP/... isomorphisms in private sourcces. We can make sop-core-extra package for those (and other future stuff which isn't useful in generics-sop)

[RyanGlScott]

I need the (++) type family to fix #116 (which affects Geneics.SOP.GGP in generics-sop), since the design for the fix would need the following function:

pad_NS :: NS f xs -> proxy ys -> NS f (xs ++ ys)

[kosmikus]

@phadej Right, I agree that having append and split versions for NS would make sense.

What are the other functions you have?

I have to read up on #116, but I can certainly be convinced to just add these functions to sop-core instead of an additional package. They're not introducing additional dependencies. The primary concern is namespace pollution.

[phadej]

Few, but only Append and Concat are non-controversial;
for others one could argue whether they should defunctionalized etc.
but I needed some of them to implement other ones:
liftA2 (:) is needed for sequence e.g.

(++)
concat
\xss yss -> concatMap (\xs -> map (xss ++) yss) xss -- (SOP f xss, SOP f yss) <-> SOP f (ConcatMapAppend xss yss), for each xs in xss and ys in yss there's (xs ++ ys) in ConcatMapAppend xss yss
concatMap (map concat . sequence)                   -- SOP (SOP f) xssss <-> SOP f (FLATTEN xsssss)
liftA2 (:)
\xss yss -> map (xs ++) yss
map concat
\x ys -> map (x :) ys
sequence @[] @{]                                    -- NP (NS f) xss <-> NS (NP f) (Sequence xss)

E.g. I'm not sure whether these hasochism artifacts should just be kept secret, and people should use singletons or something if they go beyond Append (and Concat).

[phadej]

Side-note: I'd prefer using type family Append over type family (++). I consider TypeOperators a misdesign, and we should treated : as an "upper-case" operator symbol. (Then using :+: would still be valid type-name, but one couldn't do

data a & b = Pair a b -- which is IMHO just causes confusion. I'd like to use (~>) as a type-variable to define my Arrows).

[kosmikus]

Ok, I think I'm nearly convinced that we should just add append and split.

The concrete plan seems to be:

• add hsplit and happend as methods of one or two new classes,
• provide instances for all four of NP, NS, SOP, and POP.

On the naming issue, I think I also prefer Append over (++), but I'm not sure whether I have an entirely logical argument for why. I'm not as generally opposed to TypeOperators as @phadej seems to be.

[phadej]

@kosmikus My logical argument is that ++ looks like a variable; my brain refuses to accept that you can not have operator-named variables in types. I understand where this syntax wart comes from, but it's an inconsistency which I'd prefer not to embrace.

Anyway, back to topic, it's clear where to put append_NP etc. but where to put the ++ / Append family. Currently we have e.g. Head and Tail in Data.SOP.Constraint, should new ones go there too, or should we have an own module for these promoted list functions, leaving only constraint variants (i.e. which compute some Constraint like AllZipF and AllF) in D.S.Constraint?

[echatav]

How do you want to capture happend for both NP and NS in a class?

append_NP :: NP f xs -> NP f ys -> NP f (xs ++ ys)
append_NS :: Either (NS f xs) (NS f ys) -> NS f (xs ++ ys)

It's possible by also adding a Type -> Type -> Type monoidal product to the class and using (,) or Either but that seems complex.

class HSplit prod h where
  happend :: prod (h f xs) (h f ys) -> h f (xs ++ ys)
  hsplit :: SListI xs => h f (xs ++ ys) -> prod (h f xs) (h f ys)
instance HSplit (,) NP
instance HSplit Either NS

And then happend for NP is uncurried.

[phadej]

@echatav we do something like that for hcliftA2, though we convert NP -> NP and NS -> NP there with HProd.

I argue that happend for NP doesn't need to be uncurried. there could be a variant which is defined when this new type family is Tensor ~ (,) (or whatever name which doesn't mention product, as that word is way too overloaded).

Those are details which should be easy enough to polish on the PR.

[kosmikus]

I agree it would be nicer to have the curried variant of append_NP (although it's also nice to see the relation between binary and n-ary products in the uncurried one).

I have in general started to almost always use the non-overloaded versions of the generics-sop operators because they usually have better type inference / interact better with holes. I wonder if we should deprecate the classes and just add cross-references between the "equivalent" operators for different types?

So for the PR, we should at the very least add all of append and split for all four of NP, POP, NS and SOP. Whether there should be a class to combine them is something I'll have to think a while longer. But I'd be willing to merge this without a class to combine them for the time being.