Changes between Version 28 and Version 29 of GhcKinds


Ignore:
Timestamp:
Feb 10, 2012 3:41:36 PM (4 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) =