Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
class A a b | a -> b where
class B as bs | as -> bs where
type family Pointwise (xs :: [*]) (ys :: [*]) :: Constraint where
Pointwise ' ' = ()
Pointwise (x : xs) (y : ys) = (A x y, Pointwise xs ys)
instance Pointwise as bs => B as bs where
Any idea if there's a way to make this work?
Basically, each pair in the zipped list of as and bs is functionally dependent in the instance of B, but the entire lists aren't.
I tried using some SameShapeAs constraints, but no success.
You mean that as bs determine every A x y in result of Pointwise as bs?
A x y
Pointwise as bs
But doesn't FD mean that such class is a "function" in that direction? In that case, you could determine Pointwise as bs as a whole, but determining separate parts of it sounds like trying to have function with multiple returns
yeah the 'Pointwise' tf seems to determine all of the elements of 'bs' in terms of elements of 'as', but that doesn't say anything about their order (or about duplicates in the list, so about the shape of 'bs' in general), so intuitively it feels like it shouldn't be possible
more concretely, I'm not sure how the fundep checks work, but if they're done at instance declaration instead of instantiation time, then this seems like it shouldn't work, because 'Pointwise' is just stuck in there, giving no info to the type checker (afaiu)
yeah well, I'd need to have a proof that the elements are in the correct order then
instance (A a1 b1, A a2 b2) => B [a1, a2] [b1, b2]
This is fine, however
instance (SListI as, SListI bs, SameShapeAs as bs, SameShapeAs bs as, Pointwise as bs) => B as bs where
forcing them to be lists of the same shape has no effect either (from generics-sop)
what about making the one B instance into two instances, a base one for   and a recursive one, with the usual overlaps pragma?
that's what I'm trying to migrate away from :upside_down: also your solution doesn't need overlap
ah! what I can do is have an auxiliary class just for the fundeps:
class A a b | a -> b where
class ADeps (as :: [*]) (bs :: [*]) | as -> bs where
instance ADeps ' ' where
A a b,
ADeps as bs
) => ADeps (a : as) (b : bs) where
class B (as :: [*]) (bs :: [*]) | as -> bs where
instance ADeps as bs => B as bs where
@Torsten Schmits I believe your question is the same as this one: https://stackoverflow.com/questions/65514023/how-to-require-functional-dependencies-in-kind-signature?noredirect=1#comment115829570_65514023
And you can extend the concept quite nicely: https://github.com/masaeedu/grimoire/blob/master/lib/Data/Typelevel/Function.hs
Ah wait, you're using a type family instead of a class. But you can solve this with a class, and have it be functionally dependent
...which is what you seem to have done in your final snippet :face_palm:
in the final snippet the A you are mapping over the lists is coupled to ADeps (so you need a separate class if you want to map some other functional relation over the list of types), but if you ever need to be more general and implement a map combinator the stuff in that question/library might be useful to you
@Asad Saeeduddin thanks! I incidentally struggled with precisely that issue a few days before (I only asked @Georgi Lyubenov // googleson78 in a DM :sweat_smile: ). your grimoire looks very interesting, I'm gonna rummage around in there a bit!