haskell - Can I constrain a type family?

Question

In this recent answer of mine, I happened to crack open this old chestnut (a program so old, half of it was written in the seventeenth century by Leibniz and written on a computer in the seventies by my dad). I'll leave out the modern bit to save space.

class Differentiable f where
  type D f :: * -> *

newtype K a     x  = K a
newtype I       x  = I x
data (f :+: g)  x  = L (f x)
                   | R (g x)
data (f :*: g)  x  = f x :&: g x

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)

Now, here's the frustrating thing. I don't know how to stipulate that D f must itself be differentiable. Certainly, these instances respect that property, and there might well be fun programs you can write which make use of the ability to keep differentiating a functor, shooting holes in more and more places: Taylor expansions, that sort of thing.

I'd like to be able to say something like

class Differentiable f where
  type D f
  instance Differentiable (D f)

and require a check that instance declarations have type definitions for which the necessary instances exist.

Maybe more mundane stuff like

class SortContainer c where
  type WhatsIn c
  instance Ord (WhatsIn c)
  ...

would also be nice. That, of course, has the fundep workaround

class Ord w => SortContainer c w | c -> w where ...

but to attempt the same trick for Differentiable seems... well... involuted.

So, is there a nifty workaround that gets me repeatable differentiability? (I guess I could build a representation GADT and and and... but is there a way that works with classes?)

And are there any obvious snags with the suggestion that we should be able to demand constraints on type (and, I suppose, data) families when we declare them, then check that the instances satisfy them?

Answer 1

Certainly, the obvious thing would be to simply write the desired constraint directly:

class (Differentiable (D f)) => Differentiable (f :: * -> *) where

Alas, GHC gets huffy about that and refuses to play along:

ConstrainTF.hs:17:1:
    Cycle in class declaration (via superclasses):
      Differentiable -> Differentiable
    In the class declaration for `Differentiable'

So, as is often the case when attempting to describe type constraints fancy enough to leave GHC recalcitrant, we must resort to some manner of underhanded trickery.

Recalling some relevant features of GHC where type hackery is involved:

• It is paranoid about type-level nontermination far out of proportion to the actual inconvenience it entails for the user.
• It will cheerfully commit itself to decisions about classes and instances before it has considered all the information available.
• It will dutifully attempt to check anything you've tricked it into committing to.

These are the devious principles underlying the familiar old faux-generic instances, where types are unified post-hoc with (~) in order to improve the type inference behavior of certain type hackery constructs.

In this case, however, rather than sneaking type information past GHC, we would need to somehow prevent GHC from noticing a class constraint, which is an entirely different kind of... heeeey, waaaitaminute....

import GHC.Prim

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint f = Differentiable f

class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where
  type D f :: * -> *

Hoist by its own petard!

It's the real deal, too. These are accepted, as you'd hope:

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()

But if we offer it some nonsense instead:

instance Differentiable I where
  type D I = []

GHC presents us with precisely the error message we'd like to see:

ConstrainTF.hs:29:10:
    No instance for (Differentiable [])
      arising from the superclasses of an instance declaration
    Possible fix: add an instance declaration for (Differentiable [])
    In the instance declaration for `Differentiable I'

There is one small snag, of course, namely that this:

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

...turns out to be less than well-founded, as we've told GHC to check that, whenever (f :+: g) is Differentiable, so is (D f :+: D g), which does not end well (or at all).

The easiest way to avoid this would usually be to boilerplate on a pile of explicit base cases, but here GHC seems intent on diverging any time a Differentiable constraint appears in an instance context. I would assume it's being unnecessarily eager in checking instance constraints somehow, and could perhaps be distracted long enough with another layer of trickery, but I'm not immediately sure where to start and have exhausted my capacity for post-midnight type hackery tonight.

---

A bit of IRC discussion on #haskell managed to jog my memory slightly on how GHC handles class context constraints, and it appears we can patch things up a little bit by means of a pickier constraint family. Using this:

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint (K a) = Differentiable (K a)
type instance DiffConstraint I = Differentiable I
type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g)

We now have a much more well-behaved recursion for sums:

instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

The recursive case cannot be so easily bisected for products, however, and applying the same changes there improved matters only insofar as I received a context reduction stack overflow rather than it simply hanging in an infinite loop.