# Ticket #1769: DataFamilyDerivingTypable.txt

File DataFamilyDerivingTypable.txt, 3.4 KB (added by , 9 years ago) |
---|

Line | |
---|---|

1 | From: Simon Peyton-Jones <simonpj@microsoft.com> |

2 | To: "chak@cse.unsw.edu.au" <chak@cse.unsw.edu.au> |

3 | Date: Thu, 21 Dec 2006 09:12:48 +0000 |

4 | CC: "cvs-ghc@haskell.org" <cvs-ghc@haskell.org>, Simon Peyton-Jones <simonpj@microsoft.com> |

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

6 | |

7 | Thinking about this more, I realise that the "right" place for the Typable = |

8 | instance is the type-constructor declaration itself. We should not have a = |

9 | Typeable 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 | |

18 | We could not define Eq on T; it must be done per-instance. But we can defin= |

19 | e Typeable on T; and indeed we should do so; it seems silly to have lots of= |

20 | instances. |

21 | |

22 | I'm not quite sure how to do this. |

23 | data family T :: * -> * deriving( Typeable ) |

24 | Or with separate deriving (which I like) |

25 | derive Typeable a =3D> Typeable (T a) |

26 | |

27 | |

28 | Does that make sense? |

29 | |

30 | Simon |

31 | |

32 | | -----Original Message----- |

33 | | From: Manuel M T Chakravarty [mailto:chak@cse.unsw.edu.au] |

34 | | Sent: 20 December 2006 17:30 |

35 | | To: Simon Peyton-Jones |

36 | | Cc: cvs-ghc@haskell.org |

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 |