... | ... | @@ -85,129 +85,6 @@ Currently there is no support for promoted datatypes, or the kind `Constraint`, |
|
|
|
|
|
**Future work:** address [ \#5612](http://hackage.haskell.org/trac/ghc/ticket/5612), designing and implementing a way for Template Haskell to reify the new kinds.
|
|
|
|
|
|
# Kind-polymorphic `Typeable`
|
|
|
|
|
|
|
|
|
The paper describes an improved implementation of `Typeable` (section 2.5). This has not
|
|
|
yet been implemented; the current `Typeable` class is:
|
|
|
|
|
|
```wiki
|
|
|
class Typeable (a :: *) where
|
|
|
typeOf :: a -> TypeRep
|
|
|
```
|
|
|
|
|
|
|
|
|
The new proposal makes it into:
|
|
|
|
|
|
```wiki
|
|
|
data Proxy a = Proxy
|
|
|
|
|
|
class Typeable a where
|
|
|
typeRep :: Proxy a -> TypeRep
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that `Proxy` is kind polymorphic, and so is the new `Typeable`: its type argument
|
|
|
`a` can have any kind `k`. The paper goes on to describe how we can then give
|
|
|
kind-specific instances:
|
|
|
|
|
|
```wiki
|
|
|
instance Typeable Int where typeRep _ = ...
|
|
|
|
|
|
instance Typeable [] where typeRep _ = ...
|
|
|
```
|
|
|
|
|
|
|
|
|
The following changes need to done in the compiler:
|
|
|
|
|
|
- Update `Data.Typeable` in `base` (mostly deleting classes and adding `Proxy`).
|
|
|
|
|
|
- Rewrite the `deriving Typeable` mechanism in `TcGenDeriv`.
|
|
|
|
|
|
|
|
|
From the user's perspective nothing has to change. We can make the new implementation
|
|
|
backwards-compatible by:
|
|
|
|
|
|
- Calling the method of `Typeable``typeRep`, and not `typeOf`
|
|
|
- Defining `typeOf`, `typeOf1`, ..., separately
|
|
|
|
|
|
|
|
|
Concretely, the new `Data.Typeable` will look something like this:
|
|
|
|
|
|
```wiki
|
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
|
{-# LANGUAGE PolyKinds #-}
|
|
|
|
|
|
-- Type representation: unchanged
|
|
|
data TypeRep = ...
|
|
|
|
|
|
-- Kind-polymorphic proxy
|
|
|
data Proxy t = Proxy
|
|
|
|
|
|
-- Kind-polymorphic Typeable
|
|
|
class Typeable a where
|
|
|
typeRep :: Proxy a -> TypeRep
|
|
|
|
|
|
-- Instances for base types
|
|
|
instance Typeable Char where ...
|
|
|
instance Typeable [] where ...
|
|
|
instance Typeable Either where ...
|
|
|
|
|
|
-- Old methods for backwards compatibility
|
|
|
typeOf :: forall a. Typeable a => a -> TypeRep
|
|
|
typeOf x = typeRep (getType x) where
|
|
|
getType :: a -> Proxy a
|
|
|
getType _ = Proxy
|
|
|
|
|
|
typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep
|
|
|
typeOf1 x = typeRep (getType1 x) where
|
|
|
getType1 :: t a -> Proxy t
|
|
|
getType1 _ = Proxy
|
|
|
```
|
|
|
|
|
|
|
|
|
This is nearly enough; remember that currently we can do things like this:
|
|
|
|
|
|
```wiki
|
|
|
typeOf "p"
|
|
|
typeOf1 "p"
|
|
|
```
|
|
|
|
|
|
|
|
|
And they mean different things: the first is the representation of `[Char]`,
|
|
|
whereas the second is the representation of `[]`. In particular,
|
|
|
`typeOf1 "p" == typeOf1 [()]`, for instance. To keep this behavior we have
|
|
|
to guarantee that a datatype `T` with type parameters `a1` through `an` gets instances:
|
|
|
|
|
|
```wiki
|
|
|
data T a1 ... an
|
|
|
|
|
|
instance Typeable T
|
|
|
instance (Typeable a1) => Typeable (T a1)
|
|
|
...
|
|
|
instance (Typeable a1, ..., Typeable an) => Typeable (T a1 ... an)
|
|
|
```
|
|
|
|
|
|
|
|
|
We can do this as before, by defining the arity `n-1` instance from the
|
|
|
arity `n` instance:
|
|
|
|
|
|
```wiki
|
|
|
instance (Typeable t, Typeable (a :: *)) => Typeable (t a)
|
|
|
instance (Typeable t, Typeable (a :: *), Typeable (b :: *)) => Typeable (t a b)
|
|
|
```
|
|
|
|
|
|
|
|
|
If we're willing to use `-XUndecidableInstances`, we can even do this with
|
|
|
a single instance, relying on `-XPolyKinds`:
|
|
|
|
|
|
```wiki
|
|
|
instance (Typeable t, Typeable a) => Typeable (t a)
|
|
|
```
|
|
|
|
|
|
|
|
|
In this instance, `t` has kind `k -> *` and `a` has kind `k`.
|
|
|
|
|
|
# Generalized Algebraic Data Kinds (GADKs)
|
|
|
|
|
|
**Future work:** this section deals with a proposal to collapse kinds and sorts into a single system
|
... | ... | |