Changes between Version 43 and Version 44 of Commentary/Compiler/GenericDeriving


Ignore:
Timestamp:
Dec 20, 2011 10:45:52 AM (2 years ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/GenericDeriving

    v43 v44  
    3434 * Base types like `[]`, `Maybe`, tuples, come with Generic instances. 
    3535 
     36== To be done == 
     37 
     38 * Derive `Generic1` instances 
     39 
    3640== Testing == 
    3741 
     
    4044= Kind polymorphic overhaul = 
    4145 
    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 }}} 
     46With 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 
     59module GHC.NewGenerics where 
     60 
     61import Prelude hiding (Functor(..), Show(..)) -- we'll redefine them 
     62import 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 
     67can't write kinds directly, since `Universe` is also a datatype (even if 
     68we're only interested in its promoted version). So we pass `f` and `x` 
     69only to set them to `* -> *` and `*`, respectively, in `Interprt`. 
     70`m` is different: it stands for the kind of metadata representation types, 
     71and we really want to be polymorphic over that, since each user datatype 
     72will introduce a new metadata kind. 
     73{{{ 
     74data 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 
     100infixr 5 :++: 
     101infixr 6 :**: 
     102infixr 6 :*: 
     103infixr 7 :..: 
     104 
     105-- Some shortcuts 
     106data MetaData = CC | DD | SS 
     107data Constant = PP | RR 
     108 
     109data ConstantV (c :: Constant) where 
     110  P :: ConstantV PP 
     111  R :: ConstantV RR 
     112   
     113data MetaDataV (m :: MetaData) where 
     114  C :: MetaDataV CC 
     115  D :: MetaDataV DD 
     116  S :: MetaDataV SS 
     117}}} 
     118 
     119== Universe interpretation == 
     120 
     121As promised, we set `f` to `* -> *` and `x` to `*`. 
     122Unfortunately we don't have [GhcKinds#Explicitkindvariables explicit kind variable annotations] 
     123yet, so we cannot leave `m` polymorphic! So this code doesn't compile: 
     124{{{ 
     125data 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{{{ 
     160data Proxy d = Proxy -- kind polymorphic 
     161 
     162-- Meta data classes 
     163class Datatype d where 
     164  -- The name of the datatype, fully qualified 
     165  datatypeName :: Proxy d -> String 
     166}}} 
     167There'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 * 
     173class 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 * -> * 
     179class 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 
     187User-visible class, exported: 
     188{{{ 
     189class 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 
     195Defined by the generic programmer, not exported: 
     196{{{ 
     197class GFunctor (f :: Universe (* -> *) * m) where 
     198  gfmap :: (a -> b) -> Interprt f a -> Interprt f b 
     199   
     200instance GFunctor UU where 
     201  gfmap _ U1 = U1 
     202   
     203instance GFunctor PAR where 
     204  gfmap f (Par1 a) = Par1 (f a) 
     205 
     206instance GFunctor (KK i c) where 
     207  gfmap _ (K1 a) = K1 a 
     208 
     209instance (Functor f) => GFunctor (REC f) where 
     210  gfmap f (Rec1 a) = Rec1 (fmap f a) 
     211 
     212instance (GFunctor f) => GFunctor (MM m c f) where 
     213  gfmap f (M1 a) = M1 (gfmap f a) 
     214 
     215instance (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 
     219instance (GFunctor f, GFunctor g) => GFunctor (f :**: g) where 
     220  gfmap f (a :*: b) = gfmap f a :*: gfmap f b 
     221 
     222instance (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 
     228User-visible class, exported: 
     229{{{ 
     230class Show (a :: *) where 
     231  show :: a -> String 
     232  default show :: (Generic a, GShow (Rep a)) => a -> String 
     233  show = gshow . from 
     234}}} 
     235   
     236Defined by the generic programmer, not exported: 
     237{{{ 
     238class GShow (f :: Universe (* -> *) * m) where 
     239  gshow :: Interprt f x -> String 
     240   
     241instance GShow UU where 
     242  gshow U1 = "" 
     243   
     244instance (P.Show c) => GShow (KK i c) where 
     245  gshow (K1 a) = P.show a 
     246   
     247instance (Datatype c, GShow f) => GShow (MM DD c f) where 
     248  gshow (M1 x) = datatypeName (Proxy :: Proxy c) ++ " " ++ gshow x 
     249}}} 
     250 
     251The other cases do not add any further complexity. 
     252   
     253   
     254== Example datatype encoding: lists (derived by the compiler) == 
     255{{{   
     256instance 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 
     267data List_Meta = DList | DList_Nil | DList_Cons 
     268}}} 
     269 
     270Note 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?) 
     273But we don't do that because `Universe` is polymorphic only over `m`, so 
     274a single metadata representation type. If we want a more fine-grained 
     275distinction then we would need more parameters in `Universe`, and also to 
     276split the `MM` case. 
     277{{{ 
     278instance Datatype DList where datatypeName _ = "[]" 
     279}}} 
     280   
     281   
     282Note: even better would be to index the metadata representation types over 
     283the type they refer to. Something like: 
     284{{{ 
     285  data family MetaTypes a -- kind polymorphic 
     286  data instance MetaTypes [] = DList | DList_Nil | DList_Cons 
     287}}} 
     288But now we are basically asking for promotion of data families, since we want 
     289to use promoted `DList`. Also, the case for `MM` in `Universe` would then 
     290be something like: 
     291{{{ 
     292  | MM MetaData (MetaTypes m) (Universe f x m) 
     293}}} 
     294But I'm not entirely sure about this.