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`?

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 (
A a b,
) => ADeps (a : as) (b : bs) where

class B (as :: [*]) (bs :: [*]) | as -> bs where

instance ADeps as bs => B as bs where
``````

fuckin A!

@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

Consider the following code: type CFunctor f = forall x y. (x -> y -> Constraint) -> f x -> f y -> Constraint type MapList :: CFunctor [] class MapList c xs ys instance MapList c '[...

And you can extend the concept quite nicely: https://github.com/masaeedu/grimoire/blob/master/lib/Data/Typelevel/Function.hs

Contribute to masaeedu/grimoire development by creating an account on GitHub.

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!