pointwise fundeps - Haskell

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?

hmm yes

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 true

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

instance (
    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

fuckin A!

thanks georgi

"clever girl"

@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!