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
Maybe the intuition should be that if there are at least some cases where it’s reasonable, and some where it’s questionable, it should at least be up to me the writer of f to decide that. As it stands it isn’t.
What goes wrong if, having decided that Diff is a reasonable thing to nest, you try to write functions that specifically work on Barbies restricted to Diff? Presumably that works.
EDIT: Hmm, I suppose I don’t really mean Barbies, I mean things that are quite similar to Barbies but that also have this nesting of Diff.
Well yeah, I haven’t experimented with that because there’s no such thing 
But, in my mind, there’s many completely reasonable computations to be defined on this Diff structure; namely “has anything changed?” etc. I’m not sure if that’s what you’re asking.
At present, I’ve just computed these things by hand (terrible) but if i had a traversable thing, I could just do something magical like traverse changed ... with changed :: Diff a -> Bool and everything would be amazing.
Ah ok, this could be a useful example to work with! Going back to something like the original example (but Int instead of String):
data Inner f = Inner
{ inner :: f Int }
data Outer f = Outer
{ outer :: f (Inner f) }
Suppose we instantiate this with f ~ Diff. What would the function Outer Diff :: Bool do? Would it run changed on the Inner Diff at all, or would it only inspect the Diff at the outer level?
In your original scenario, I wonder if you’d be interested in this sort of approach:
{-# LANGUAGE QuantifiedConstraints, TypeFamilies, UndecidableInstances #-}
import Data.Functor.Const
import Data.Kind
import Data.Proxy
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)
-- A constrained higher-order substitution class. Instances define the domains
-- over which the argument to chsubst must be specialized.
class CHSubst (h :: (Type -> Type) -> Type) where
type Dom h (c :: Type -> Constraint) (f :: Type -> Type) (g :: Type -> Type) :: Constraint
chsubst :: forall c f g. Dom h c f g => Proxy c -> (forall a. c a => f a -> g a) -> h f -> h g
instance CHSubst Inner where
type Dom Inner c f g = c String
chsubst _ f (Inner inner) = Inner $ f inner
-- The commented-out lines represent an alternate implementation that gives
-- **different results**. No naturality here; a CHSubst is not a functor.
instance CHSubst Outer where
type Dom Outer c f g = (Functor f, c (Inner g), Dom Inner c f g)
--type Dom Outer c f g = (Functor g, c (Inner f), Dom Inner c f g)
chsubst c f (Outer outer) = Outer $ f' outer
where
f' = f . fmap (chsubst c f)
--f' = fmap (chsubst c f) . f
showIt :: Show a => Maybe a -> Const String a
showIt = Const . show
main :: IO ()
main = print $ chsubst (Proxy @Show) showIt $ Outer (Just $ Inner $ Just "hi")
See if deep-transformations solves your problem. I’m the author, and I’ve used it successfully for wrapping every AST node in different kinds of … wrappers. It’s based on rank2lasses rather than barbies, but it’s HKD nonetheless.
1 Like
Is this something to be used alongside the original HKD approach (that is, hmap for the regular transformations, and CHSubst for the ones with constraints), or something that completely replaces it? I tried to use it with a function that doesn’t involve any constraints (such as maybeToList as in the original example) but couldn’t figure out how. I defined the following constraint to be passed as the proxy argument:
type Empty :: Type -> Constraint
type Empty a = ()
However, it doesn’t work for reasons I can’t understand:
ghci> :k Show
Show :: * -> Constraint
ghci> :k Empty
Empty :: * -> Constraint
ghci> :t Proxy @Show
Proxy @Show :: Proxy Show
ghci> :t Proxy @Empty
<interactive>:1:1: error:
• The type synonym ‘Empty’ should have 1 argument, but has been given none
• In the expression: Proxy @Empty
…I can’t see how Empty is different from Show for my purposes here.
On the other hand, is the proxy argument argument really necessary, or is it just for the convenience in the implementation? The constraint is already part of the provided mapping function (showIt in this case), so I believe it should be possible to omit the proxy, though simply removing it didn’t work. Maybe it would be possible if a type signature fo f' is provided in instance CHSubst Outer, but I couldn’t come up with something that works.
Also, kind of unrelated, but I also wonder if this CHSubst implementation serves to show that my original approach was unsound because of showIt not being a natural transformation (since the two potential implementations you provided for instance CHSubst Outer yield different results for the given example).
Two things here. The first is that a type synonym that isn’t fully applied can’t be assigned to a type variable like c, even with a type application. If you want to test out the null constraint, you’ll have do something like this instead:
class Empty a
instance Empty a
main :: IO ()
main = do
let it = Outer (Just $ Inner (Just "hi"))
print $ chsubst (Proxy @Empty) maybeToList $ it
print $ chsubst (Proxy @Show) showIt $ it
But yes, with that trick, you should be able to work with constraint-less substitutions, or substitutions with multiple constraints via an analogous trick with superclasses, for higher-kinded types that use nested applications of the argument.
The second: yes, the proxy can be dropped, but then you’ll have to use type applications; I don’t think GHC will instantiate constraint-kinded type variables in a useful way here, because it’s ambiguous whether to bind the constraint needed by the f function to c or whether to solve for instances of that constraint and let c be something else. So you’d be looking at:
class CHSubst (h :: (Type -> Type) -> Type) where
type Dom h (c :: Type -> Constraint) (f :: Type -> Type) (g :: Type -> Type) :: Constraint
chsubstImpl :: forall c f g. Dom h c f g => (forall a. c a => f a -> g a) -> h f -> h g
-- reorders h and c, for convenience
chsubst :: forall c h f g. (CHSubst h, Dom h c f g) => (forall a. c a => f a -> g a) -> h f -> h g
chsubst = chsubstImpl @h @c
instance CHSubst Inner where
type Dom Inner c f g = c String
chsubstImpl f (Inner inner) = Inner $ f inner
instance CHSubst Outer where
type Dom Outer c f g = (Functor f, c (Inner g), Dom Inner c f g)
--type Dom Outer c f g = (Functor g, c (Inner f), Dom Inner c f g)
-- This type signature is required to put `c` in scope
chsubstImpl :: forall c f g. Dom Outer c f g => (forall a. c a => f a -> g a) -> Outer f -> Outer g
chsubstImpl f (Outer outer) = Outer $ f' outer
where
f' = f . fmap (chsubst @c f)
--f' = fmap (chsubst @c f) . f
main :: IO ()
main = do
let it = Outer (Just $ Inner (Just "hi"))
print $ chsubst @Empty maybeToList $ it
print $ chsubst @Show showIt $ it
Yeah, that’s what I was trying to suggest. The very existence of the constraint is part of the reason that such functions aren’t natural; the free theorem for forall a. f a -> g a for functors f and g says that every such function is natural, when unconstrained, but when adding in a constraint the free theorem takes a different form.