Can I constrain a type family?
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?
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:
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.
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.
With the new UndecidableSuperclasses in GHC 8
class Differentiable (D f) => Differentiable (f :: Type -> Type) where
works.
链接地址: http://www.djcxy.com/p/66626.html上一篇: 应用变压器是否真的是多余的？
下一篇: 我可以限制类型家庭吗？