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.

Answer 2

Your best bet might be to define something using the constraints package:

import Data.Constraint

class Differentiable (f :: * -> *) where
  type D f :: * -> *
  witness :: p f -> Dict (Differentiable (D f))

then you can manually open the dictionary whenever you need to recurse.

This would let you employ the general shape of the solution in Casey's answer, but not have the compiler (or runtime) spin forever on induction.

Answer 3

With the new UndecidableSuperclasses in GHC 8

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

works.

Answer 4

This can be accomplished in the same manner as Edward suggests with a tiny implementation of Dict. First, let's get the language extensions and imports out of the way.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

TypeOperators is only for your example problem.

Tiny Dict

We can make our own tiny implementation of Dict. Dict uses a GADT and ConstraintKinds to capture any constraint in the constructor for a GADT.

data Dict c where
    Dict :: c => Dict c  

withDict and withDict2 reintroduce the constraint by pattern matching on the GADT. We only need to be able to reason about terms with one or two sources of constraints.

withDict :: Dict c -> (c => x) -> x
withDict Dict x = x

withDict2 :: Dict a -> Dict b -> ((a, b) => x) -> x
withDict2 Dict Dict x = x

Infinitely differentiable types

Now we can talk about infinitely differentiable types, whose derivatives must also be differentiable

class Differentiable f where
    type D f :: * -> *
    d2 :: p f -> Dict (Differentiable (D f))
    -- This is just something to recover from the dictionary
    make :: a -> f a

d2 takes a proxy for the type, and recovers the dictionary for taking the second derivative. The proxy allows us to easily specify which type's d2 we are talking about. We can get to deeper dictionaries by applying d:

d :: Dict (Differentiable t) -> Dict (Differentiable (D t))
d d1 = withDict d1 (d2 (pt (d1)))
    where
        pt :: Dict (Differentiable t) -> Proxy t
        pt = const Proxy

Capturing the dictonary

The polynomial functor types, products, sums, constants, and zero, are all infinitely differentiable. We will define the d2 witnesses for each of these types

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

Zero and constants don't require any additional knowledge to capture their derivative's Dict

instance Differentiable K where
  type D K = K
  make = const K
  d2 = const Dict

instance Differentiable I where
  type D I = K
  make = I
  d2 = const Dict

Sum and product both require the dictionaries from both of their component's derivatives to be able to deduce the dictionary for their derivative.

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
  make = R . make
  d2 p = withDict2 df dg $ Dict
    where
        df = d2 . pf $ p
        dg = d2 . pg $ p
        pf :: p (f :+: g) -> Proxy f
        pf = const Proxy
        pg :: p (f :+: g) -> Proxy g
        pg = const Proxy

instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
  make x = make x :&: make x
  d2 p = withDict2 df dg $ Dict
    where
        df = d2 . pf $ p
        dg = d2 . pg $ p
        pf :: p (f :*: g) -> Proxy f
        pf = const Proxy
        pg :: p (f :*: g) -> Proxy g
        pg = const Proxy

Recovering the dictionary

We can recover the dictionary for constraints that we otherwise wouldn't have adequate information to deduce. Differentiable f would normally only let use get to make :: a -> f a, but not to either make :: a -> D f a or make :: a -> D (D f) a.

make1 :: Differentiable f => p f -> a -> D f a
make1 p = withDict (d2 p) make

make2 :: Differentiable f => p f -> a -> D (D f) a
make2 p = withDict (d (d2 p)) make