Opened 3 years ago

Closed 14 months ago

#5391 closed feature request (wontfix)

Better deriving for Typeable

Reported by: simonpj Owned by:
Priority: normal Milestone: 7.6.2
Component: Compiler Version: 7.0.4
Keywords: Cc: dterei, vogt.adam@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

In a message to GHC users, provoked by 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 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.

Attachments (1)

typeable-diff (12.5 KB) - added by simonpj 3 years ago.
Diff for preliminary work on extending "deriving Typeable"

Download all attachments as: .zip

Change History (8)

Changed 3 years ago by simonpj

Diff for preliminary work on extending "deriving Typeable"

comment:1 Changed 3 years ago by simonpj

  • Type changed from bug to feature request

comment:2 Changed 2 years ago by igloo

  • Milestone set to 7.6.1

comment:3 Changed 2 years ago by dterei

  • Cc dterei added

comment:4 Changed 19 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:5 Changed 16 months ago by aavogt

  • Cc vogt.adam@… added

comment:6 Changed 14 months ago by monoidal

Now Typeable is kind-polymorphic, should this be closed?

comment:7 Changed 14 months ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to wontfix
  • Status changed from new to closed

Yes, the polykinded Typeable is strictly better than the compromise offered here.

Note: See TracTickets for help on using tickets.