Split off HFunctor from HAp

[edsko]

Currently we only have a generalization of HAp (HApplicative), and functions that could be defined in terms of a (hypothetical) HFunctor class are defined in terms of HAp instead. This is fine for the SOP types, but it makes it impossible to declare some other types to be instances.

[kosmikus]

So probably, if we were to add our own HFunctor class, it'd look like this:

class HFunctor (h :: (k -> Type) -> (l -> Type)) where
  hmap :: (SListIN (Prod h) xs) => (forall a . f a -> f' a) -> h f xs -> h f' xs
  hcmap :: (AllN (Prod h) c xs) => proxy c -> (forall a . c a => f a -> f' a) -> h f xs -> h f' xs

I'm not really opposed to this, but I'm wondering if it will end there ...

In general, the classes in generics-sop are not really intended to be used for other datatypes.

I'm not very happy with the overall situation, and I'd be willing to consider using more general-purpose type classes for higher-order variants of standard type classes instead.

Just a cursory scan of Hackage reveals e.g. higher-order functors at least in the following places:

• https://hackage.haskell.org/package/category-extras-0.53.5/docs/Control-Functor-HigherOrder.html
• http://hackage.haskell.org/package/compdata-0.12/docs/Data-Comp-Multi-HFunctor.htm
• http://hackage.haskell.org/package/hschema-0.0.1.1/docs/Control-Functor-HigherOrder.html
• https://hackage.haskell.org/package/type-combinators-0.2.4.3/docs/Type-Class-Higher.html#t:Functor1
• https://hackage.haskell.org/package/quickcheck-state-machine-0.6.0/docs/Test-StateMachine-Types-Rank2.html#t:Functor
• https://hackage.haskell.org/package/functor-combinators-0.1.1.1/docs/Data-HFunctor.html#t:HFunctor
• http://hackage.haskell.org/package/fused-effects-0.5.0.1/docs/Control-Effect-Carrier.html#t:HFunctor

Some observations:

• Not all of these classes are kind-polymorphic, which we need.
• Most of these classes do not offer constrained variants of the functions (such as hcmap in generics-sop). While strictly speaking these would probably not be necessary because one could always construct products of dictionaries, I think they make a huge practical difference.
• Our classes currently have strange constructs like Prod (which I feel we should perhaps get rid of) and SListIN constraints on the index parameters, thereby morally indicating that the index type should always be a type-level list.

One way in which we could make our own classes be much closer to the classes used elsewhere would be by flipping the type arguments of NP, NS, POP, SOP so that we e.g. have

NP :: [k] -> (k -> Type) -> Type

rather than

NP :: (k -> Type) -> [k] -> Type

This would allow us to say that NP xs is an instance of a HFunctor class for all xs that are in SListI, rather than making NP an instance of HFunctor itself and infecting the class declaration with properties of xs. The HFunctor class would then look like:

class HCFunctor Top h => HFunctor (h :: (k -> Type) -> Type) where
  hmap :: (forall a . f a -> f' a) -> h f -> h f'
  hmap = hcmap (Proxy :: Proxy @Top)

class HCFunctor (c :: k -> Type) (h :: (k -> Type) -> Type) where
  hcmap :: Proxy c -> (forall a . c a => f a -> f' a) -> h f -> h f'

instance SListI xs => HFunctor (NP xs) where ...
instance All c xs => HCFunctor (NP xs) where ...

I'm not sure if it's worth making such a drastic change though in order to clean up the internals.

Anyway, to cut this short, I think it wouldn't do any harm to add an HFunctor class similar to the one outlined at the beginning to the library, if that remains the only change needed for your purposes.

[edsko]

Yeah, I know that they weren't intended to be used by other types, but sometimes that does arise naturally. But perhaps this is indeed a bit of a quagmire (did I spell that right...? 🤔 ). The other one we might ponder is a HTraversable. That trio (functor, applicative, traversable) seems like a reasonable answer to "where does it stop".

I suspect that flipping the arguments will cause more pain than it solves?

We don't need both hcmap and hmap right? One can be derived from the other; but yes, having the constrained version available I think is essential.

And yes, I found that Prod type family confusing also :)

[edsko]

(Actually, it's HTraversable that we ended up using in the end.)

[kosmikus]

The constrained and unconstrained variants are in principle derivable from each other, yes. Going from constrained to unconstrained is now the easier direction, especially since we now have that SListI xs ~ All Top xs.

I'd only flip the arguments if we'd decide to do a big breaking release. I'd then be inclined to also rename NP to Product and NS to Sum. I'd push for this more strongly if I'd be completely convinced that SumOfProducts and ProductOfProducts aren't too much typing.

Re Prod: we introduced it so that we could use hap with a sum and a product. But I don't think that we should use the same combinator for this, and keep hap limited to two products.

HTraversable: with what definition? I guess incompatible with the existing HTraverse_?

[edsko]

Yeah, we have

-- | N-ary traversable functors
--
-- TODO: Don't provide Elem explicitly (just instantiate @c@)?
-- TODO: Introduce HTraverse into SOP?
class NTraversable (f :: (k -> Type) -> [k] -> Type) where
  nctraverse :: (Applicative m, All c xs)
             => proxy c
             -> (forall a. c a => Elem xs a -> g a -> m (h a))
             -> f g xs -> m (f h xs)

The Elem thing could probably easily(ish) be removed. But the existing HTraverse_ class doesn't give a result.

[phadej]

@edsko are you looking for https://hackage.haskell.org/package/sop-core-0.5.0.0/docs/Data-SOP-Classes.html#t:HSequence ?

class HAp h => HSequence (h :: (k -> Type) -> l -> Type) where
  hctraverse'
    :: (AllN h c xs, Applicative g)
    => proxy c -> (forall a. c a => f a -> g (f' a)) -> h f xs -> g (h f' xs)

[edsko]

Oh! Yes, perhaps so 😳

[edsko]

Why do we have both? 🤔