Tuesday, 27 November 2012

Coming soon in GHC HEAD: poly-kinded Typeable

With the implementation of DataKinds and kind polymorphism being complete in the 7.6 branch of GHC, it's time to start adapting libraries to make full use of this new potential. Lately I've been working on implementing the kind-polymorphic Typeable class as described in the original promotion paper in GHC. And I'm happy to say the work is nearly finished; it wasn't much, but there were some important design decisions to take. You can play with it by checking out the new-typeable GHC branch.

The Typeable class now looks like this:
  data Proxy (t :: k) = Proxy

  class Typeable (a :: k) where
    typeRep :: Proxy (a :: k) -> TypeRep
Note that the kind annotations are optional in this case, but I've included them to stress that this class is indeed kind-polymorphic. In this new class, we are no longer restricted to datatypes with a maximum of 7 parameters, nor do we require the parameters to be of kind *. We've renamed typeOf to typeRep, but we still define the old methods for backwards compatibility:
  typeOf :: forall a. Typeable a => a -> TypeRep
  typeOf _ = typeRep (Proxy :: Proxy a)

  typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep
  typeOf1 _ = typeRep (Proxy :: Proxy t)

  typeOf2 :: forall t (a :: *) (b :: *). Typeable t => t a b -> TypeRep
  typeOf2 _ = typeRep (Proxy :: Proxy t)
Now, each datatype only has one Typeable instance. Lists, for example, have an instance Typeable [], and Either has an instance Typeable Either. We then have a single, poly-kinded instance to deal with type application:
  instance (Typeable s, Typeable a) => Typeable (s a) where
    typeRep _ = typeRep (Proxy :: Proxy s) `mkAppTy` typeRep (Proxy :: Proxy a)
(Note that we're using ScopedTypeVariables in the examples.) Another cool thing is that now even type classes can have Typeable instances; since we allow abstraction over Constraint, datatypes may have parameters involving the Constraint kind, so to support Typeable for those datatypes, we need to support Typeable for type classes in general (as pointed out by Gábor Lehel). We cannot attach deriving clauses to type classes, but we can use standalone deriving:
  deriving instance Typeable Eq
To make things easier we also provide a AutoDeriveTypeable language extension that generates a derived instance of Typeable for every data and class declaration in the module it's used.

Since every datatype can now be given a Typeable instance, and since handwritten instances of Typeable can lead to segmentation faults, we will also prevent users from writing their own instances of Typeable. Such instances, if present, will be ignored and raise a warning. To allow old code to still compile without changes, we've moved the monomorphic Typeable class to module Data.OldTypeable (which is deprecated).

After some more testing and documentation, the new-typeable branch will be merged with master, and kind-polymorphic Typeable will be available in GHC HEAD.

[Edited to replace github gists with more RSS/embed-friendly CSS/JS.]


  1. FWIW (I don't really mind either way) weren't most opinions in the mailing list thread in favor of deriving Typeable unconditionally? Was it later decided to require a language pragma after all?

  2. I guess unconditional deriving of unuesd things makes compiling unnecessary slow.

  3. We've decided to take this more conservative route, for now at least, until we know the effects of AutoDeriveTypeable on compilation time and code size. If it's ok, then AutoDeriveTypeable might be on by default at some point...