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


Ignore:
Timestamp:
Dec 20, 2011 10:45:52 AM (4 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.