RE: patch applied (ghc): Deriving for indexed data types

Thinking about this more, I realise that the "right" place for the Typable instance is the type-constructor declaration itself.  We should not have a Typeable instance for each indexed type; rather just one for the whole type.  Thus

        data family T :: *->*
        instance Typeable1 T where
          typeOf1 _ = ...

        data instance T [a] = T1 a | T2 deriving( Eq )

We could not define Eq on T; it must be done per-instance. But we can define Typeable on T; and indeed we should do so; it seems silly to have lots of instances.

I'm not quite sure how to do this.
        data family T :: * -> * deriving( Typeable )
Or with separate deriving (which I like)
        derive Typeable a => Typeable (T a)


Does that make sense?

Simon

| -----Original Message-----
| From: Manuel M T Chakravarty [mailto:[email protected]]
| Sent: 20 December 2006 17:30
| To: Simon Peyton-Jones
| Cc: [email protected]
| Subject: RE: patch applied (ghc): Deriving for indexed data types
|
| Simon,
|
| > |   - We cannot derive Typeable.  This seems a problem of notation,
| more
| > | than
| > |     anything else.  Why?  For a binary vanilla data type "T a b",
| we
| > | would
| > |     generate an instance Typeable2 T; ie, the instance is for the
| > | constructor
| > |     alone.  In the case of a family instance, such as (S [a] (Maybe
| > | b)), we
| > |     simply have no means to denote the associated constuctor.  It
| > | appears to
| > |     require type level lambda - something like (/\a b. S [a] (Maybe
| b).
| >
| > Suppose you have an indexed data type with kind
| >         T :: * -> * -> * -> *
| > Of these parameters, suppose 2 are type indices and 1 is fully
| polymorphic.
|
| Just to ensure that I understand exactly what you mean, for indexed
| data
| types (as opposed to indexed synonyms) we dropped this whole arity
| business and distinction between arguments that can be indexes and
| others that must be parametric.  (We can drop that distinction for
| indexed data types as they only ever induce injective type functions;
| ie, ones for which decomposition is valid.)
|
| However, for every individual instance of an indexed data type, we
| could
| peel of any trailing variable-only arguments.  (Somewhat like the eta
| business for newtype deriving.)  So, for
|
|   data instance T [a] b = ... deriving Typeable
|
| we could generate
|
|   instance Typeable a => Typeable1 (T [a]) where ...
|
| However, for
|
|   data instance T [a] (Maybe b) = ... deriving Typeable
|
| we would generate
|
|   instance (Typeable a, Typeable b) => Typeable (T [a] (Maybe b)) where
| ...
|
| So, for different instances of the same family, we would use different
| TypeableX classes.  Do you think that might be too confusing.
|
| > Then shouldn't we generate an instance for Typeable1, *not*
| Typeable3:
| >         instance (Typeable a, Typeable b) => Typeable1 (T a b)
| where...
| >
| > Then there is no difficulty about generating its type representation
| is there?
|
| I didn't look at the type representation yet, as I stumbled over the
| mentiond issue first.  But I think it should be ok.
|
| Manuel
|