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
|
_______________________________________________
Cvs-ghc mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/cvs-ghc
