Ticket #1769: DataFamilyDerivingTypable.txt

File DataFamilyDerivingTypable.txt, 3.4 KB (added by chak, 7 years ago)

Spec

Line 
1From: Simon Peyton-Jones <[email protected]>
2To: "[email protected]" <[email protected]>
3Date: Thu, 21 Dec 2006 09:12:48 +0000
4CC: "[email protected]" <[email protected]>, Simon Peyton-Jones <[email protected]>
5Subject: RE: patch applied (ghc): Deriving for indexed data types
6
7Thinking about this more, I realise that the "right" place for the Typable =
8instance is the type-constructor declaration itself.  We should not have a =
9Typeable instance for each indexed type; rather just one for the whole type=
10  Thus
11
12        data family T :: *->*
13        instance Typeable1 T where
14          typeOf1 _ =3D ...
15
16        data instance T [a] =3D T1 a | T2 deriving( Eq )
17
18We could not define Eq on T; it must be done per-instance. But we can defin=
19e Typeable on T; and indeed we should do so; it seems silly to have lots of=
20 instances.
21
22I'm not quite sure how to do this.
23        data family T :: * -> * deriving( Typeable )
24Or with separate deriving (which I like)
25        derive Typeable a =3D> Typeable (T a)
26
27
28Does that make sense?
29
30Simon
31
32| -----Original Message-----
33| From: Manuel M T Chakravarty [mailto:[email protected]]
34| Sent: 20 December 2006 17:30
35| To: Simon Peyton-Jones
36| Cc: [email protected]
37| Subject: RE: patch applied (ghc): Deriving for indexed data types
38|
39| Simon,
40|
41| > |   - We cannot derive Typeable.  This seems a problem of notation,
42| more
43| > | than
44| > |     anything else.  Why?  For a binary vanilla data type "T a b",
45| we
46| > | would
47| > |     generate an instance Typeable2 T; ie, the instance is for the
48| > | constructor
49| > |     alone.  In the case of a family instance, such as (S [a] (Maybe
50| > | b)), we
51| > |     simply have no means to denote the associated constuctor.  It
52| > | appears to
53| > |     require type level lambda - something like (/\a b. S [a] (Maybe
54| b).
55| >
56| > Suppose you have an indexed data type with kind
57| >         T :: * -> * -> * -> *
58| > Of these parameters, suppose 2 are type indices and 1 is fully
59| polymorphic.
60|
61| Just to ensure that I understand exactly what you mean, for indexed
62| data
63| types (as opposed to indexed synonyms) we dropped this whole arity
64| business and distinction between arguments that can be indexes and
65| others that must be parametric.  (We can drop that distinction for
66| indexed data types as they only ever induce injective type functions;
67| ie, ones for which decomposition is valid.)
68|
69| However, for every individual instance of an indexed data type, we
70| could
71| peel of any trailing variable-only arguments.  (Somewhat like the eta
72| business for newtype deriving.)  So, for
73|
74|   data instance T [a] b =3D ... deriving Typeable
75|
76| we could generate
77|
78|   instance Typeable a =3D> Typeable1 (T [a]) where ...
79|
80| However, for
81|
82|   data instance T [a] (Maybe b) =3D ... deriving Typeable
83|
84| we would generate
85|
86|   instance (Typeable a, Typeable b) =3D> Typeable (T [a] (Maybe b)) where
87| ...
88|
89| So, for different instances of the same family, we would use different
90| TypeableX classes.  Do you think that might be too confusing.
91|
92| > Then shouldn't we generate an instance for Typeable1, *not*
93| Typeable3:
94| >         instance (Typeable a, Typeable b) =3D> Typeable1 (T a b)
95| where...
96| >
97| > Then there is no difficulty about generating its type representation
98| is there?
99|
100| I didn't look at the type representation yet, as I stumbled over the
101| mentiond issue first.  But I think it should be ok.
102|
103| Manuel
104|
105
106