42 | | The current implementation supports defining both functions over types of kind `*` (such as `show`) and functions over types of kind `* -> *` (such as `fmap`). Although care has been taken to reduce code duplication, we still need two generic classes, one for each kind (`Generic` and `Generic1`). |
43 | | |
44 | | With the new `-XPolyKinds` functionality, we can make the support for generic programming better typed and more general. The basic idea is to define the universe codes (`M1`, `:+:`, etc.) as constructors of a datatype. Promotion then lifts these constructors to types, which we can use as before, only that now we have them all classified under a new kind: |
45 | | {{{ |
46 | | data Universe x = U |
47 | | | K x |
48 | | | P Nat |
49 | | | Universe x :+: Universe x |
50 | | | Universe x :*: Universe x |
51 | | | M MetaData (Universe x) |
52 | | |
53 | | data MetaData = C | D | S |
54 | | }}} |
| 46 | With the new `-XPolyKinds` functionality we can make the support for generic programming better typed. The basic idea is to define the universe codes (`M1`, `:+:`, etc.) as constructors of a datatype. Promotion then lifts these constructors to types, which we can use as before, only that now we have them all classified under a new kind: |
| 47 | |
| 48 | {{{ |
| 49 | {-# LANGUAGE TypeOperators #-} |
| 50 | {-# LANGUAGE GADTs #-} |
| 51 | {-# LANGUAGE TypeFamilies #-} |
| 52 | {-# LANGUAGE ScopedTypeVariables #-} |
| 53 | {-# LANGUAGE FlexibleContexts #-} |
| 54 | {-# LANGUAGE FlexibleInstances #-} |
| 55 | {-# LANGUAGE PolyKinds #-} |
| 56 | {-# LANGUAGE DefaultSignatures #-} |
| 57 | {-# LANGUAGE NoImplicitPrelude #-} |
| 58 | |
| 59 | module GHC.NewGenerics where |
| 60 | |
| 61 | import Prelude hiding (Functor(..), Show(..)) -- we'll redefine them |
| 62 | import qualified Prelude as P (Show(..)) |
| 63 | }}} |
| 64 | |
| 65 | == Generic representation universe == |
| 66 | `m` is the only real parameter here. `f` and `x` are there because we |
| 67 | can't write kinds directly, since `Universe` is also a datatype (even if |
| 68 | we're only interested in its promoted version). So we pass `f` and `x` |
| 69 | only to set them to `* -> *` and `*`, respectively, in `Interprt`. |
| 70 | `m` is different: it stands for the kind of metadata representation types, |
| 71 | and we really want to be polymorphic over that, since each user datatype |
| 72 | will introduce a new metadata kind. |
| 73 | {{{ |
| 74 | data Universe f x m = |
| 75 | -- Void (used for datatypes without constructors) |
| 76 | VV |
| 77 | |
| 78 | -- Unit |
| 79 | | UU |
| 80 | |
| 81 | -- The parameter |
| 82 | | PAR |
| 83 | |
| 84 | -- Recursion into a type of kind * -> * |
| 85 | | REC f |
| 86 | |
| 87 | -- Constants (either other parameters or recursion into types of kind *) |
| 88 | | KK Constant x |
| 89 | |
| 90 | -- Metadata |
| 91 | | MM MetaData m (Universe f x m) |
| 92 | |
| 93 | -- Sum, product, composition |
| 94 | | Universe f x m :++: Universe f x m |
| 95 | | Universe f x m :**: Universe f x m |
| 96 | | f :..: Universe f x m |
| 97 | -- Note that we always compose a concrete type on the left (like []) with |
| 98 | -- a generic representation on the right |
| 99 | |
| 100 | infixr 5 :++: |
| 101 | infixr 6 :**: |
| 102 | infixr 6 :*: |
| 103 | infixr 7 :..: |
| 104 | |
| 105 | -- Some shortcuts |
| 106 | data MetaData = CC | DD | SS |
| 107 | data Constant = PP | RR |
| 108 | |
| 109 | data ConstantV (c :: Constant) where |
| 110 | P :: ConstantV PP |
| 111 | R :: ConstantV RR |
| 112 | |
| 113 | data MetaDataV (m :: MetaData) where |
| 114 | C :: MetaDataV CC |
| 115 | D :: MetaDataV DD |
| 116 | S :: MetaDataV SS |
| 117 | }}} |
| 118 | |
| 119 | == Universe interpretation == |
| 120 | |
| 121 | As promised, we set `f` to `* -> *` and `x` to `*`. |
| 122 | Unfortunately we don't have [GhcKinds#Explicitkindvariables explicit kind variable annotations] |
| 123 | yet, so we cannot leave `m` polymorphic! So this code doesn't compile: |
| 124 | {{{ |
| 125 | data Interprt :: Universe (* -> *) * m -> * -> * where |
| 126 | |
| 127 | -- No interpretation for VV, as it shouldn't map to any value |
| 128 | |
| 129 | -- Unit |
| 130 | U1 :: Interprt UU p |
| 131 | |
| 132 | -- The parameter |
| 133 | Par1 :: p -> Interprt PAR p |
| 134 | |
| 135 | -- Recursion into a type of kind * -> * |
| 136 | Rec1 :: r p -> Interprt (REC r) p |
| 137 | |
| 138 | -- Constants |
| 139 | K1 :: x -> Interprt (KK c x) p |
| 140 | -- Constants shortcuts |
| 141 | Par0 :: x -> Interprt (KK PP x) p |
| 142 | Rec0 :: x -> Interprt (KK RR x) p |
| 143 | |
| 144 | -- Metadata |
| 145 | M1 :: Interprt x p -> Interprt (MM m c x) p |
| 146 | -- Metadata shortcuts |
| 147 | D1 :: Interprt x p -> Interprt (MM DD c x) p |
| 148 | C1 :: Interprt x p -> Interprt (MM CC c x) p |
| 149 | S1 :: Interprt x p -> Interprt (MM SS c x) p |
| 150 | |
| 151 | -- Sum, product, and composition |
| 152 | L1 :: Interprt a r -> Interprt (a :++: b) r |
| 153 | R1 :: Interprt b r -> Interprt (a :++: b) r |
| 154 | (:*:) :: Interprt a r -> Interprt b r -> Interprt (a :**: b) r |
| 155 | Comp1 :: f (Interprt g r) -> Interprt (f :..: g) r |
| 156 | }}} |
| 157 | |
| 158 | == Metadata representation == |
| 159 | {{{ |
| 160 | data Proxy d = Proxy -- kind polymorphic |
| 161 | |
| 162 | -- Meta data classes |
| 163 | class Datatype d where |
| 164 | -- The name of the datatype, fully qualified |
| 165 | datatypeName :: Proxy d -> String |
| 166 | }}} |
| 167 | There's more of these, but they don't add any new concerns. |
| 168 | |
| 169 | |
| 170 | == Conversion between user datatypes and generic representation == |
| 171 | {{{ |
| 172 | -- Representable types of kind * |
| 173 | class Generic a where |
| 174 | type Rep a :: Universe (* -> *) * m |
| 175 | from :: a -> Interprt (Rep a) x |
| 176 | to :: Interprt (Rep a) x -> a |
| 177 | |
| 178 | -- Representable types of kind * -> * |
| 179 | class Generic1 (f :: * -> *) where |
| 180 | type Rep1 f :: Universe (* -> *) * m |
| 181 | from1 :: f a -> Interprt (Rep1 f) a |
| 182 | to1 :: Interprt (Rep1 f) a -> f a |
| 183 | }}} |
| 184 | |
| 185 | == Example generic function: `fmap` (kind `* -> *`) == |
| 186 | |
| 187 | User-visible class, exported: |
| 188 | {{{ |
| 189 | class Functor (f :: * -> *) where |
| 190 | fmap :: (a -> b) -> f a -> f b |
| 191 | default fmap :: (Generic1 f, GFunctor (Rep1 f)) => (a -> b) -> f a -> f b |
| 192 | fmap f = to1 . gfmap f . from1 |
| 193 | }}} |
| 194 | |
| 195 | Defined by the generic programmer, not exported: |
| 196 | {{{ |
| 197 | class GFunctor (f :: Universe (* -> *) * m) where |
| 198 | gfmap :: (a -> b) -> Interprt f a -> Interprt f b |
| 199 | |
| 200 | instance GFunctor UU where |
| 201 | gfmap _ U1 = U1 |
| 202 | |
| 203 | instance GFunctor PAR where |
| 204 | gfmap f (Par1 a) = Par1 (f a) |
| 205 | |
| 206 | instance GFunctor (KK i c) where |
| 207 | gfmap _ (K1 a) = K1 a |
| 208 | |
| 209 | instance (Functor f) => GFunctor (REC f) where |
| 210 | gfmap f (Rec1 a) = Rec1 (fmap f a) |
| 211 | |
| 212 | instance (GFunctor f) => GFunctor (MM m c f) where |
| 213 | gfmap f (M1 a) = M1 (gfmap f a) |
| 214 | |
| 215 | instance (GFunctor f, GFunctor g) => GFunctor (f :++: g) where |
| 216 | gfmap f (L1 a) = L1 (gfmap f a) |
| 217 | gfmap f (R1 a) = R1 (gfmap f a) |
| 218 | |
| 219 | instance (GFunctor f, GFunctor g) => GFunctor (f :**: g) where |
| 220 | gfmap f (a :*: b) = gfmap f a :*: gfmap f b |
| 221 | |
| 222 | instance (Functor f, GFunctor g) => GFunctor (f :..: g) where |
| 223 | gfmap f (Comp1 x) = Comp1 (fmap (gfmap f) x) |
| 224 | }}} |
| 225 | |
| 226 | == Example generic function: `show` (kind `*`, uses metadata) == |
| 227 | |
| 228 | User-visible class, exported: |
| 229 | {{{ |
| 230 | class Show (a :: *) where |
| 231 | show :: a -> String |
| 232 | default show :: (Generic a, GShow (Rep a)) => a -> String |
| 233 | show = gshow . from |
| 234 | }}} |
| 235 | |
| 236 | Defined by the generic programmer, not exported: |
| 237 | {{{ |
| 238 | class GShow (f :: Universe (* -> *) * m) where |
| 239 | gshow :: Interprt f x -> String |
| 240 | |
| 241 | instance GShow UU where |
| 242 | gshow U1 = "" |
| 243 | |
| 244 | instance (P.Show c) => GShow (KK i c) where |
| 245 | gshow (K1 a) = P.show a |
| 246 | |
| 247 | instance (Datatype c, GShow f) => GShow (MM DD c f) where |
| 248 | gshow (M1 x) = datatypeName (Proxy :: Proxy c) ++ " " ++ gshow x |
| 249 | }}} |
| 250 | |
| 251 | The other cases do not add any further complexity. |
| 252 | |
| 253 | |
| 254 | == Example datatype encoding: lists (derived by the compiler) == |
| 255 | {{{ |
| 256 | instance Generic [a] where |
| 257 | type Rep [a] = MM DD DList |
| 258 | (MM CC DList_Nil UU :++: |
| 259 | MM CC DList_Cons (KK PP a :**: KK RR [a])) |
| 260 | |
| 261 | from [] = D1 (L1 (C1 U1)) |
| 262 | from (h:t) = D1 (R1 (C1 (Par0 h :*: Rec0 t))) |
| 263 | to (D1 (L1 (C1 U1))) = [] |
| 264 | to (D1 (R1 (C1 (Par0 h :*: Rec0 t)))) = h:t |
| 265 | |
| 266 | -- Metadata |
| 267 | data List_Meta = DList | DList_Nil | DList_Cons |
| 268 | }}} |
| 269 | |
| 270 | Note that we use only one datatype; more correct would be to use 3, one for |
| 271 | `DList`, another for the constructors, and yet another for the selectors |
| 272 | (or maybe even n datatypes for the selectors, one for each constructor?) |
| 273 | But we don't do that because `Universe` is polymorphic only over `m`, so |
| 274 | a single metadata representation type. If we want a more fine-grained |
| 275 | distinction then we would need more parameters in `Universe`, and also to |
| 276 | split the `MM` case. |
| 277 | {{{ |
| 278 | instance Datatype DList where datatypeName _ = "[]" |
| 279 | }}} |
| 280 | |
| 281 | |
| 282 | Note: even better would be to index the metadata representation types over |
| 283 | the type they refer to. Something like: |
| 284 | {{{ |
| 285 | data family MetaTypes a -- kind polymorphic |
| 286 | data instance MetaTypes [] = DList | DList_Nil | DList_Cons |
| 287 | }}} |
| 288 | But now we are basically asking for promotion of data families, since we want |
| 289 | to use promoted `DList`. Also, the case for `MM` in `Universe` would then |
| 290 | be something like: |
| 291 | {{{ |
| 292 | | MM MetaData (MetaTypes m) (Universe f x m) |
| 293 | }}} |
| 294 | But I'm not entirely sure about this. |