Changes between Version 21 and Version 22 of GhcKinds


Ignore:
Timestamp:
Dec 15, 2011 2:23:58 PM (4 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) =