#5391: Better deriving for Typeable
-+--
Reporter: simonpj |Owner:
Type: bug | Status: new
Priority: normal|Milestone:
Component: Compiler | Version: 7.0.4
Keywords:| Testcase:
Blockedby:| Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
-+--
In a [http://www.haskell.org/pipermail/glasgow-haskell-
users/2011-July/020574.html message to GHC users], provoked by [http://www
.mail-archive.com/haskell-cafe@haskell.org/msg91830.html a thread on
Haskell Cafe] I proposed the following improvement to deriving `Typeable`:
David Mazieres and others comment that you can't derive `Typeable` for
types like this:
{{{
data T f = MkT (f Int)
}}}
So he defines his own instance like this
{{{
[C] instance Typable1 f = Typeable (T f) where
typeOf = ...
}}}
So why can't GHC do this? Well, here's what GHC does. Given a bog
standard data type like `Maybe`
{{{
data Maybe a = Nothing | Just a deriving( Typeable )
}}}
GHC generates this instance
{{{
[A] instance Typeable1 Maybe where
typeOf = ...
}}}
Remember that `Typeable1` takes a type ''constructor'', of kind `(*-*)`,
as its argument.
Now if we need `(Typeable (Maybe Int))`, GHC first uses an instance from
the `Typeable` library:
{{{
[B] instance (Typeable1 f, Typeable a) = Typeable (f a) where
typeOf = ...
}}}
And now it uses the `(Typeable1 Maybe)` instance [A]. So it's kind of
cool... the applications are decomposed by [B], leaving the tycon to [A].
But this doesn't work for T above. We can't make `(Typeable1 T)` because
T has kind `((*-*)-*)`, not `(*-*`) as `Typeable1` requires. Hence
David defining his own instance.
GHC could do this too. Indeed it could do so for `Maybe` too, thus:
{{{
instance Typeable a = Typeable (Maybe a) where
typeOf = ...
}}}
But then, alas, we could not get `(Typeable (T Maybe))`, because [C] needs
`Maybe` to be in `Typeable1`.
= Proposal =
So here is a compromise, which would at least do better than the current
story:
{{{
When deriving Typeable for a data type S of kind
S :: k1 - .. - kn - * - ... - *
(where kn is not *, and there are M trailing * arguments),
generate the instance
instance (Typeable_x1 a1, ..., Typeable_xn an)
= TypeableM (S a1 .. an)
}}}
That is, knock off all the trailing `*` args, and then generate an
instance for the remaining stub.
= Example=
Example from iterIO:
{{{
newtype Iter (t :: *) (m :: *-*) (a :: *)
= Iter { runIter :: Chunk t - IterR t m a }
deriving( Typeable )
}}}
This should generate
{{{
instance (Typeable t, Typeable1 m) = Typeable1 (Iter t m)
}}}
where we knock off the trailing `(a :: *`) argument.
= Question =
This approach is not beautiful. It does not solve the underlying problem,
which is a lack of kind polymorphism, but that is a battle for another
day. Until that day, this alternative way of deriving `Typeable` would
automate significantly more cases, I think. Of course, it also makes it
more complicated to explain when deriving `Typeable` will succeed.
= State of play =
As it happens, I'm working with Dimitrios and Julien on adding a proper
kind system to GHC, and that will in turn affect the whole Typeable story.
See [wiki:GhcKinds our wiki page on kinds].
So I'm going to put this thread on ice for now, but I'm attaching a
partial patch I did earlier so I don't lose it.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/5391
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
