Changes between Version 28 and Version 29 of GhcKinds


Ignore:
Timestamp:
Feb 10, 2012 3:41:36 PM (2 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds

    v28 v29  
    7979 
    8080 
    81 = Kind-polymorphic `Typeable` = 
    82  
    83 The paper describes an improved implementation of `Typeable` (section 2.5). This has not 
    84 yet been implemented; the current `Typeable` class is: 
    85 {{{ 
    86 class Typeable (a :: *) where 
    87   typeOf :: a -> TypeRep 
    88 }}} 
    89  
    90 The new proposal makes it into: 
    91 {{{ 
    92 data Proxy a = Proxy 
    93  
    94 class Typeable a where 
    95   typeRep :: Proxy a -> TypeRep 
    96 }}} 
    97 Note that `Proxy` is kind polymorphic, and so is the new `Typeable`: its type argument 
    98 `a` can have any kind `k`. The paper goes on to describe how we can then give 
    99 kind-specific instances: 
    100 {{{ 
    101 instance Typeable Int where typeRep _ = ... 
    102  
    103 instance Typeable []  where typeRep _ = ... 
    104 }}} 
    105  
    106 The following changes need to done in the compiler: 
    107   * Update `Data.Typeable` in `base` (mostly deleting classes and adding `Proxy`). 
    108  
    109   * Rewrite the `deriving Typeable` mechanism in `TcGenDeriv`. 
    110  
    111 From the user's perspective nothing has to change. We can make the new implementation 
    112 backwards-compatible by: 
    113   * Calling the method of `Typeable` `typeRep`, and not `typeOf` 
    114   * Defining `typeOf`, `typeOf1`, ..., separately 
    115  
    116 Concretely, the new `Data.Typeable` will look something like this: 
    117 {{{ 
    118 {-# LANGUAGE ScopedTypeVariables #-} 
    119 {-# LANGUAGE PolyKinds           #-} 
    120  
    121 -- Type representation: unchanged 
    122 data TypeRep = ... 
    123  
    124 -- Kind-polymorphic proxy 
    125 data Proxy t = Proxy 
    126  
    127 -- Kind-polymorphic Typeable 
    128 class Typeable a where 
    129   typeRep :: Proxy a -> TypeRep 
    130  
    131 -- Instances for base types 
    132 instance Typeable Char   where ... 
    133 instance Typeable []     where ... 
    134 instance Typeable Either where ... 
    135  
    136 -- Old methods for backwards compatibility   
    137 typeOf :: forall a. Typeable a => a -> TypeRep 
    138 typeOf x = typeRep (getType x) where 
    139   getType :: a -> Proxy a 
    140   getType _ = Proxy 
    141  
    142 typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep 
    143 typeOf1 x = typeRep (getType1 x) where 
    144   getType1 :: t a -> Proxy t 
    145   getType1 _ = Proxy 
    146 }}} 
    147  
    148 This is nearly enough; remember that currently we can do things like this: 
    149 {{{ 
    150 typeOf  "p" 
    151 typeOf1 "p" 
    152 }}} 
    153 And they mean different things: the first is the representation of `[Char]`, 
    154 whereas the second is the representation of `[]`. In particular,  
    155 `typeOf1 "p" == typeOf1 [()]`, for instance. To keep this behavior we have 
    156 to guarantee that a datatype `T` with type parameters `a1` through `an` gets instances: 
    157 {{{ 
    158 data T a1 ... an 
    159  
    160 instance Typeable T 
    161 instance (Typeable a1) => Typeable (T a1) 
    162 ... 
    163 instance (Typeable a1, ..., Typeable an) => Typeable (T a1 ... an) 
    164 }}} 
    165  
    166 We can do this as before, by defining the arity `n-1` instance from the 
    167 arity `n` instance: 
    168  
    169 {{{ 
    170 instance (Typeable t, Typeable (a :: *)) => Typeable (t a) 
    171 instance (Typeable t, Typeable (a :: *), Typeable (b :: *)) => Typeable (t a b) 
    172 }}} 
    173  
    174 If we're willing to use `-XUndecidableInstances`, we can even do this with 
    175 a single instance, relying on `-XPolyKinds`: 
    176 {{{ 
    177 instance (Typeable t, Typeable a) => Typeable (t a) 
    178 }}} 
    179 In this instance, `t` has kind `k -> *` and `a` has kind `k`. 
    180  
    18181 
    18282= Generalized Algebraic Data Kinds (GADKs) =