Higher-Kinded Data (HKD) pattern with nesting and constraints?

Learn
#1

Recently I have been trying to incorporate Higher-Kinded Data (HKD) approach to the project I am working on, but I am having issues coming up with something that satisfies all my needs. I initially tried to use the barbies library. However, the representation barbies went for doesn’t allow nested HKDs. An example could be the following:

data Inner f = Inner
  { inner :: f String }

data Outer f = Outer
  { outer :: f (Inner f) }

deriving instance (forall a. Show a => Show (f a)) => Show (Inner f)
deriving instance (forall a. Show a => Show (f a)) => Show (Outer f)

The reason why this doesn’t work as-is is briefly explained in this barbies GitHub issue, and an alternative encoding is offered by the author. However, after some time fiddling with it, I couldn’t make it work, so I decided to roll my own thing. Essentially, in order to have these nested HKDs, one needs a Functor constraint on the mapping function, and that’s what I used for my HKD representation:

class HFunctor (b :: (Type -> Type) -> Type) where
  hmap :: forall f g. (Functor f) => (forall a. f a -> g a) -> b f -> b g

instance HFunctor Inner where
  hmap :: Functor f => (forall a. f a -> g a) -> Inner f -> Inner g
  hmap f (Inner inner) = Inner (f inner)

instance HFunctor Outer where
  hmap :: Functor f => (forall a. f a -> g a) -> Outer f -> Outer g
  hmap f (Outer outer) = Outer $ f (hmap f <$> outer)

…and it works as expected:

-- >>> hmap maybeToList (Inner (Just "foo"))
-- Inner {inner = ["foo"]}

-- 'Outer' works too:
-- >>> hmap maybeToList (Outer (Just (Inner (Just "foo"))))
-- Outer {outer = [Inner {inner = ["foo"]}]}

Here comes the problem: I also want to be able to use natural transformations that impose constraints on the argument. However, hmap as we currently have it doesn’t work with such functions:

showIt :: Show a => Maybe a -> Const String a
showIt = Const . show

-- >>> hmap showIt (Inner (Just "foo"))
-- No instance for (Show a_aK2d[sk:2]) arising from a use of `showIt'
-- Possible fix:
--   add (Show a_aK2d[sk:2]) to the context of
--     a type expected by the context:
--       forall a. Maybe a -> Const String a
-- In the first argument of `hmap', namely `showIt'
-- In the expression: hmap showIt (Inner (Just "foo"))
-- In an equation for `it_aK0i':
--     it_aK0i = hmap showIt (Inner (Just "foo"))

The way barbies handles this is by reifying the constraint and pairing it up with the original argument, so that the mapping function fits the expected structure of a natural transformation. I employed the same trick:

-- Set up the machinery to reify the constraint, similar to
-- the 'constraints' library:
data Dict c a where
  Dict :: c a => Dict c a

requiringDict :: (c a => r) -> Dict c a -> r
requiringDict r Dict = r

showItPacked :: Product (Dict Show) Maybe a -> Const String a
showItPacked (Pair d ma) = requiringDict (showIt ma) d

-- Let's try 'hmap' again:

-- >>> :t hmap showItPacked
-- Could not deduce (Functor (Dict Show)) arising from a use of `hmap'
-- from the context: HFunctor b_a1mrR[sk:1]
--   bound by the inferred type of
--              it_a1ms2 :: HFunctor b_a1mrR[sk:1] =>
--                          b_a1mrR[sk:1] (Product (Dict Show) Maybe)
--                          -> b_a1mrR[sk:1] (Const String)
--   at <interactive>:1:1
-- In the expression: hmap showItPacked

Right, Dict Show doesn’t have a Functor instance. However, the way I see it, it can’t have a lawful Functor instance. Just because you have a function that turns a's into b's, and a is Showable, doesn’t mean that b needs to be Showable as well.

At this point, I couldn’t figure out how to proceed further with this. The way I understand it, the Functor constraint on hmap is essential to make nested HKDs work. However, it doesn’t play nicely with constraints. I have tried to employ some (Co)yoneda trickeries to potentially “defer” the Functor constraint on the mapping function, but to no avail.

TL;DR:

I am looking for a way to make nested Higher-Kinded Data approach play nicely with mapping functions that involve constraints.

2 Likes
#2

I too have been frustrated by this, I think, and the only lead I can give you is to perhaps check out hypertypes. That said, I didn’t have much luck with it for solving my actual problem :frowning:

1 Like
#3

Maybe a better HFunctor class that doesn’t require the parameter to be a functor is:

class HFunctor b where
  hmap :: (forall a b. (a -> b) -> f a -> g b) -> b f -> b g
1 Like
#4

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.

#5

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!

#6

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
#7

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.

#8

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
#9

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.

#10

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.

#11

By “nesting” I mean what @ozkutuk referred to here:

Does that clarify?

#12

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.

#13

Do you mean that you want diffs between diffs?

#14

No; just the record example I gave above.

#15

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.

#16

You will find that it does, when you implement it in barbies :slight_smile: Or at least, I did.

If there’s another approach, I’d be very happy to know about it!

#17

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

#18

[this comment was pointing out an issue that is now fixed]

1 Like
#19

Now you can see you need f (B f) which is where it all goes wrong.

#20

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?