How to require functional dependencies in kind signature?

Question

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 '[] '[]
instance (c x y, MapList c xs ys) => MapList c (x ': xs) (y ': ys)

This works fine, but it's desirable in some situations to "make things compute" by introducing a functional dependency of the form:

class MapList c xs ys | c xs -> ys

With the functional dependency we have 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 | c xs -> ys
instance MapList c '[] '[]
instance (c x y, MapList c xs ys) => MapList c (x ': xs) (y ': ys)

This does not compile however, and produces the following error on the last instance:

[typecheck] [E] • Illegal instance declaration for ‘MapList c (x : xs) (y : ys)’
    The liberal coverage condition fails in class ‘MapList’
      for functional dependency: ‘c xs -> ys’
    Reason: lhs types ‘c’, ‘x : xs’
      do not jointly determine rhs type ‘y : ys’
    Un-determined variable: y
• In the instance declaration for ‘MapList c (x : xs) (y : ys)’

This makes sense: c + xs determines ys due to the recursive use of MapList c xs ys (which has a functional dependency). But c + x ': xs determines c + y ': ys only if x determines y, which is a property we must require of the class being passed in for c.

But how can we adjust the CFunctor kind to demand this? As far as I'm aware there is no vocabulary in kind signatures to discuss functional dependencies. Is there still a way I can make this work?

Answer 1

One workaround is to create a wrapper class that simply demands whatever your original constraint was, plus a functional dependency. The only way to satisfy the functional dependency in the wrapper is to have a functional dependency in the original class.

To wit:

type FDep :: (a -> b -> Constraint) -> a -> b -> Constraint
class c x y => FDep c x y | c x -> y

Now we can write:

type MapList :: CFunctor []
class MapList c xs ys | c xs -> ys
instance MapList (FDep c) '[] '[]
instance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)

And have it type check.

When passing in some arrow, e.g.:

class Fst ab a | ab -> a
instance Fst '(a, b) a

We simply instantiate FDep for it as well, to witness the fact that it has the relevant functional dependency:

instance Fst ab a => FDep Fst ab a

Somewhat curiously, our functor mappings are closed with respect to FDep-ness, as illustrated below:

type MapList :: CFunctor []
class MapList c xs ys | c xs -> ys
instance MapList c xs ys => FDep (MapList c) xs ys

instance MapList (FDep c) '[] '[]
instance (FDep c x y, MapList (FDep c) xs ys) => MapList (FDep c) (x ': xs) (y ': ys)

This is nice, because it allows functors to compose arbitrarily. It suggests we are doing some kind of weird Constraint enriched category theory whose objects are kinds, and whose morphisms are functionally dependent classes.

Here is a worked example of using our type level computer:

(^$) :: FDep c x y => Proxy c -> Proxy x -> Proxy y
(^$) _ _ = Proxy

class Fst ab a | ab -> a
instance Fst ab a => FDep Fst ab a

instance Fst '(a, b) a

test :: _
test = Proxy @(MapList (FDep Fst)) ^$ Proxy @'[ '(0, 1)]

The type hole error that results is:

[typecheck] [E] • Found type wildcard ‘_’ standing for ‘Proxy '[0]’
  To use the inferred type, enable PartialTypeSignatures
• In the type signature: test :: _