From: Simon PeytonJones
To: "chak@cse.unsw.edu.au"
Date: Thu, 21 Dec 2006 09:12:48 +0000
CC: "cvsghc@haskell.org" , Simon PeytonJones
Subject: 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 typeconstructor 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 _ =3D ...
data instance T [a] =3D T1 a  T2 deriving( Eq )
We could not define Eq on T; it must be done perinstance. But we can defin=
e 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 =3D> Typeable (T a)
Does that make sense?
Simon
 Original Message
 From: Manuel M T Chakravarty [mailto:chak@cse.unsw.edu.au]
 Sent: 20 December 2006 17:30
 To: Simon PeytonJones
 Cc: cvsghc@haskell.org
 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 variableonly arguments. (Somewhat like the eta
 business for newtype deriving.) So, for

 data instance T [a] b =3D ... deriving Typeable

 we could generate

 instance Typeable a =3D> Typeable1 (T [a]) where ...

 However, for

 data instance T [a] (Maybe b) =3D ... deriving Typeable

 we would generate

 instance (Typeable a, Typeable b) =3D> 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) =3D> 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
