Why is this? I’ve typically seen HFunctor without that constraint, and it seems kind of funny to constrain f in this construction without also constraining g.
I have actually stumbled upon your posts in the barbies’ issue tracker which prompted me to check out hypertypes. However, the library is very abstract and the documentation is sparse, making it quite hard to understand. In addition, it is not a library specific to HKD use cases, and there is no readily available example for such a use case (as you have also mentioned in the hypertypes’ issue tracker). Considering all these, I thought rolling my own thing could be easier. I would love to see an HKD example in hypertypes though!
This is interesting! I tried playing with it a little bit, and I actually could proceed further with the constraint-related problems with this representation, though I am still far from getting something usable. Just to make sure I got the basic idea right, here is how I defined the instances for the two data types:
instance HFunctor Inner where
hmap :: (forall a c. (a -> c) -> f a -> g c) -> Inner f -> Inner g
hmap f (Inner inner) = Inner (f id inner)
instance HFunctor Outer where
hmap :: (forall a c. (a -> c) -> f a -> g c) -> Outer f -> Outer g
hmap f (Outer outer) = Outer $ f (hmap f) outer
I don’t perfectly understand what I am doing, I just let the types guide the implementation, and it seems to work fine:
-- >>> hmap (\f -> maybeToList . fmap f) (Inner (Just "foo"))
-- Inner {inner = ["foo"]}
-- >>> hmap (\f -> maybeToList . fmap f) (Outer (Just (Inner (Just "foo"))))
-- Outer {outer = [Inner {inner = ["foo"]}]}
For the usual use case, I could even recover the original Functorial definition for ease of use:
hmap' :: (HFunctor b, Functor f) => (forall a. f a -> g a) -> b f -> b g
hmap' f = h (\f' -> f . fmap f')
-- So this still works:
-- >>> hmap' maybeToList (Inner (Just "foo"))
-- Inner {inner = ["foo"]}
I will try working with this representation a little bit to see if it would fully solve the “constraints problem”.
1 Like
With the usual representation, if you don’t have the Functor constraint, you can’t possibly write an HFunctor instance for the Outer data type that I presented above because of the “nestedness”. Adapting the example from the related barbies issue:
instance HFunctor Outer where
hmap h (Outer fibf)
= -- because Inner is an HFunctor, we can use `hmap h` on it; we only need to
-- pass it through the outer f with an `fmap`; unfortunately this won't typecheck...
Outer $ h (hmap h <$> fibf)
As for why g doesn’t have the same constraint, well, it wasn’t required to write the above instance, so I left it out. Though barbies-layered has both of them constrained, so maybe there is merit in doing so.
It’s an arbitrary choice. You could instead have written
instance HFunctor Outer where
hmap :: Functor g => (forall a. f a -> g a) -> Outer f -> Outer g
hmap f (Outer outer) = Outer $ fmap (hmap f) . f $ outer
and if f represents a natural transformation, this will be equivalent, because naturality means fmap g . f = f . fmap g for any g, including, in this case, hmap f.
But I don’t believe your showIt is natural. I expect different results when you first map inner structure from Maybe to Const and then call show on the outer structure, and when you first call show and then map inner structure. You’re trying to lift an infranatural transformation up through your HFunctor and I wouldn’t think that this is something that an HFunctor should adapt its signature in order to allow, but that’s just my gut check.
1 Like
I also have the same intuition, but I have not been able to come up with a compelling example. I’m not convinced that this "nesting of f" pattern in Barbies is a coherent thing to do, but I can’t put my finger on why not, exactly.
For what it’s worth, the motivation for me is fairly simple; I have a simple data structure, but I want to wrap it in a “diff”.
data X = { a :: Int, b :: B }
data B = { x :: Int }
To:
data X = { a :: Diff Int, b :: Diff B }
data B = { x :: Diff Int }
Seems fairly uncontroversial to me.
By “nesting” I mean what @ozkutuk referred to here:
That’s what you end up with if you implement the Diff thing in barbies with sub-records able to be diffed.
Do you mean that you want diffs between diffs?
No; just the record example I gave above.
That doesn’t involve any nesting of f (i.e. of Diff), just nesting of records. It’s nesting of f that I doubt to be coherent.
EDIT: It does involve nesting of Diff, but I don’t understand what that means.
You will find that it does, when you implement it in barbies 
Or at least, I did.
If there’s another approach, I’d be very happy to know about it!
To write your example the Barbies way, wouldn’t you define
data X f = { a :: f Int, b :: B f }
data B f = { x :: f Int }
and then use X Diff and B Diff?
EDIT: fixed (twice) thanks to @jaror
[this comment was pointing out an issue that is now fixed]
1 Like
Now you can see you need f (B f) which is where it all goes wrong.
That was a typo (now fixed). I don’t understand why you want Diff B where B itself is a Diff. That’s why I asked whether you want diffs between diffs. You’re ending up with something isomorphic to
(Diff Int, Diff (Diff Int))
Do you really want a Diff (Diff Int)? What does it mean?
Just for now suppose Diff is list; i.e. it’s at least coherent.
It happens that I do want this, but I agree it isn’t perfect; but for me I think it’s more convenient than not having it. I.e. I sort it out at the value level.
To be fair it’s been a while and I’ll have to remind myself if that style you suggest works. As I recall I didn’t want to do it, but maybe I was wrong. I’ll revisit.
Sure, I agree that nesting particular type constructors is a coherent thing to do! What I’m not yet able to understand is how nesting type constructors arbitrarily and generically is coherent. The difficulty involved in writing generic operations that work on them suggests it might not be a coherent thing to do.
I can see that it is coherent to write data types which are trees with f-labelled types at the leaves. That’s what Barbies are. I don’t understand what it means, in general, to also apply f arbitrarily at branches, and then generically map to another tree that has g at the branches (which is what this thread is about).
The difficulty seems to arise when keeping track of all the constraints that you’re going to need when traversing the structure. Maybe there’s a convenient way of packaging up the constraints, but I don’t see what it could be, yet. On the other hand, I can’t construct an example that shows definitively that it’s a doomed idea, in general.
1 Like