Changes between Version 21 and Version 22 of GhcKinds


Ignore:
Timestamp:
Dec 15, 2011 2:23:58 PM (2 years ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds

    v21 v22  
    2222 
    2323= Kind-polymorphic `Typeable` = 
     24 
     25The paper describes an improved implementation of `Typeable` (section 2.5). This has not 
     26yet been implemented; the current `Typeable` class is: 
     27{{{ 
     28class Typeable (a :: *) where 
     29  typeOf :: a -> TypeRep 
     30}}} 
     31 
     32The new proposal makes it into: 
     33{{{ 
     34data Proxy a = Proxy 
     35 
     36class Typeable a where 
     37  typeRep :: Proxy a -> TypeRep 
     38}}} 
     39Note that `Proxy` is kind polymorphic, and so is the new `Typeable`: its type argument 
     40`a` can have any kind `k`. The paper goes on to describe how we can then give 
     41kind-specific instances: 
     42{{{ 
     43instance Typeable Int where typeRep _ = ... 
     44 
     45instance Typeable []  where typeRep _ = ... 
     46}}} 
     47 
     48The following changes need to done in the compiler: 
     49  * Update `Data.Typeable` in `base` (mostly deleting classes and adding `Proxy`). 
     50 
     51  * Rewrite the `deriving Typeable` mechanism in `TcGenDeriv`. 
     52 
     53From the user's perspective nothing has to change. We can make the new implementation 
     54backwards-compatible by: 
     55  * Calling the method of `Typeable` `typeRep`, and not `typeOf` 
     56  * Defining `typeOf`, `typeOf1`, ..., separately 
     57 
     58Concretely, the new `Data.Typeable` will look something like this: 
     59{{{ 
     60{-# LANGUAGE ScopedTypeVariables #-} 
     61{-# LANGUAGE PolyKinds           #-} 
     62 
     63-- Type representation: unchanged 
     64data TypeRep = ... 
     65 
     66-- Kind-polymorphic proxy 
     67data Proxy t = Proxy 
     68 
     69-- Kind-polymorphic Typeable 
     70class Typeable a where 
     71  typeRep :: Proxy a -> TypeRep 
     72 
     73-- Instances for base types 
     74instance Typeable Char   where ... 
     75instance Typeable []     where ... 
     76instance Typeable Either where ... 
     77 
     78-- Old methods for backwards compatibility   
     79typeOf :: forall a. Typeable a => a -> TypeRep 
     80typeOf x = typeRep (getType x) where 
     81  getType :: a -> Proxy a 
     82  getType _ = Proxy 
     83 
     84typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep 
     85typeOf1 x = typeRep (getType1 x) where 
     86  getType1 :: t a -> Proxy t 
     87  getType1 _ = Proxy 
     88}}} 
     89 
     90This is nearly enough; remember that currently we can do things like this: 
     91{{{ 
     92typeOf  "p" 
     93typeOf1 "p" 
     94}}} 
     95And they mean different things: the first is the representation of `[Char]`, 
     96whereas the second is the representation of `[]`. In particular,  
     97`typeOf1 "p" == typeOf1 [()]`, for instance. To keep this behavior we have 
     98to guarantee that a datatype `T` with type parameters `a1` through `an` gets instances: 
     99{{{ 
     100data T a1 ... an 
     101 
     102instance Typeable T 
     103instance (Typeable a1) => Typeable (T a1) 
     104... 
     105instance (Typeable a1, ..., Typeable an) => Typeable (T a1 ... an) 
     106}}} 
     107 
     108We can do this as before, by defining the arity `n-1` instance from the 
     109arity `n` instance: 
     110 
     111{{{ 
     112instance (Typeable t, Typeable (a :: *)) => Typeable (t a) 
     113instance (Typeable t, Typeable (a :: *), Typeable (b :: *)) => Typeable (t a b) 
     114}}} 
     115 
     116If we're willing to use `-XUndecidableInstances`, we can even do this with 
     117a single instance, relying on `-XPolyKinds`: 
     118{{{ 
     119instance (Typeable t, Typeable a) => Typeable (t a) 
     120}}} 
     121In this instance, `t` has kind `k -> *` and `a` has kind `k`. 
    24122 
    25123= Generalized Algebraic Data Kinds (GADKs) =