On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones
<simonpj@microsoft.com> wrote:
| > Hmm. If you have
| > class (Diff (D f)) => Diff f where
| >
| > then if I have
| > f :: Diff f => ...
| > f = e
| > then the constraints available for discharging constraints arising
| > from e are
| > Diff f
| > Diff (D f)
| > Diff (D (D f))
| > Diff (D (D (D f)))
| > ...
| >
| > That's a lot of constraints.
|
| But isn't it a bit like having an instance
|
| Diff f => Diff (D f)
A little bit. And indeed, could you not provide such instances? That is, every time you write an equation for D, such as
type D (K a) = K Void
make sure that Diff (K Void) also holds.
The way you it, when you call f :: Diff f => <blah>, you are obliged to pass runtime evidence that (Diff f) holds. And that runtime evidence includes as a sub-component runtime evidence that (Diff (D f)) holds. If you like the, the evidence for Diff f looks like this:
data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
So you are going to have to build an infinite data structure. You can do that fine in Haskell, but type inference looks jolly hard.
For example, suppose we are seeking evidence for
Diff (K ())
We might get such evidence from either
a) using the instance decl
instance Diff (K a) where ...
or
b) using the fact that (D I) ~ K (), we need Diff I, so
we could use the instance
instance Diff I
Having two ways to get the evidence seems quite dodgy to me, even apart from the fact that I have no clue how to do type inference for it.
Simon