... | ... | @@ -3,7 +3,8 @@ |
|
|
## Overview
|
|
|
|
|
|
|
|
|
This page describes a new API for type indexed type representations, basic `Dynamic` functionality, static pointers and distributed closures. It is a specific realisation of the ideas in [DistributedHaskell](distributed-haskell).
|
|
|
This page describes a new API for type indexed type representations, basic `Dynamic` functionality, static pointers and distributed closures.
|
|
|
It is a specific realisation of the ideas in [DistributedHaskell](distributed-haskell).
|
|
|
|
|
|
|
|
|
Just as in [DistributedHaskell](distributed-haskell), we provide 4 APIs
|
... | ... | @@ -12,9 +13,9 @@ Just as in [DistributedHaskell](distributed-haskell), we provide 4 APIs |
|
|
|
|
|
- `Data.Dynamic`: dynamically-typed values; replaces the existing `Data.Dynamic`. The API is almost unchanged.
|
|
|
|
|
|
- `Data.StaticPtr`: static pointers. The idea is that this will ultimately by the foundation for the Cloud Haskell `xxx` package.
|
|
|
- `Data.StaticPtr`: static pointers. The idea is that this will ultimately by the foundation for the `[https://hackage.haskell.org/package/distributed-static Cloud Haskell]` package.
|
|
|
|
|
|
- `DistributedClosure`: serialisable closures. The idea is that this will ultimately by the foundation for the Cloud Haskell `distributed-closure` package.
|
|
|
- `Control.DistributedClosure`: serialisable closures. The idea is that this will ultimately by the foundation for the Cloud Haskell `distributed-static` package.
|
|
|
|
|
|
|
|
|
Each is described in more detail below.
|
... | ... | @@ -24,7 +25,9 @@ Each is described in more detail below. |
|
|
|
|
|
We propose to
|
|
|
|
|
|
- *Outright replace* the existing `Typeable` class with the new one; ditto the `TypeRep` type. This seems better than inventing new names for everything (e.g. class `TypeableT`, data type `TypeRepT`. Not many packages use `TypeRep` explicitly, we want to encourage those that do to switch over.
|
|
|
- *Outright replace* the existing `Typeable` class with the new one; ditto the `TypeRep` type.
|
|
|
This seems better than inventing new names for everything (e.g. class `TypeableT`, data type `TypeRepT`.
|
|
|
Not many packages use `TypeRep` explicitly, we want to encourage those that do to switch over.
|
|
|
|
|
|
- GHC magic for the `Typeable` class will apply to the new class.
|
|
|
|
... | ... | @@ -35,30 +38,28 @@ We propose to |
|
|
|
|
|
## Questions
|
|
|
|
|
|
|
|
|
See also the individual questions sections below.
|
|
|
|
|
|
- Now is the easiest time to rename things - do you have suggestions for better naming schemes?
|
|
|
- Any comments would be gladly recieved!
|
|
|
- Any comments would be gladly received!
|
|
|
|
|
|
---
|
|
|
|
|
|
## Data.Typeable
|
|
|
|
|
|
|
|
|
For `Data.Typeable` we ultimately need Richard Eisenberg's kind
|
|
|
equalities. But until GHC gets kind equalities we offer variant ("homogeneous case")
|
|
|
that doens't need them,
|
|
|
but has an extra `unsafeCoerce` or two.
|
|
|
|
|
|
|
|
|
offer two variants, one for ghc as of 2015-07-10 with kind-homogenous equalities `a:~:b` only, and one for kind-hetrogenous type equalities `a:~~:b`.
|
|
|
For `Data.Typeable` we ultimately need Richard Eisenberg's kind equalities.
|
|
|
But until GHC gets kind equalities we offer a variant ("homogeneous case") that doesn't need them, but has an extra `unsafeCoerce` or two, and returns `Bool` rather than a type equality on kind-heterogeneous comparisons.
|
|
|
|
|
|
### Without kind equalities
|
|
|
|
|
|
```
|
|
|
dataTypeRep(a :: k)-- abstractappR::TypeRep(a :: k -> k')->TypeRep(b :: k)->TypeRep(a b)classTypeable(a :: k)where
|
|
|
typeRepT ::TypeRep a
|
|
|
typeRep ::TypeRep a
|
|
|
|
|
|
-- GHC has magic built-in support for Typeable instances-- but the effect is similar to declarations like these:instance(Typeable c,Typeable a)=>Typeable(c a)instanceTypeableBoolinstanceTypeable(->)withTypeRep::TypeRep a ->(Typeable a => b)-> b
|
|
|
-- c.f. Trac #2439eqRR::TypeRep(a :: k1)->TypeRep(b :: k2)->BooleqRRHom::TypeRep(a :: k)->TypeRep(b :: k)->Maybe(a :~: b)dataGetAppT(a :: k)whereGA::TypeRep(a :: k1 -> k2)->TypeRep(b :: k1)->GetAppT(a b)getAppR::TypeRep(a :: k)->Maybe(GetAppT a)dataG1 c a whereG1::TypeRep(a :: k)->G1(c :: k -> k')(c a)getR1::TypeRep(ct :: k1 -> k)->TypeRep(c'at :: k)->Maybe(G1 ct c'at)-- Implementation uses an unsafeCoercedataG2 c a whereG2::TypeRep(a :: k1)->TypeRep(b :: k2)->G2(c :: k1 -> k2 -> k3)(c a b)getR2::TypeRep(c :: k2 -> k1 -> k)->TypeRep(a :: k)->Maybe(G2 c a)-- Implementation uses an unsafeCoerce-- rest are for conveniencetypeOf::Typeable a =>(a ::*)->TypeRep a
|
|
|
-- c.f. Trac #2439eqRR::TypeRep(a :: k1)->TypeRep(b :: k2)->BooleqRRHom::TypeRep(a :: k)->TypeRep(b :: k)->Maybe(a :~: b)dataGetApp(a :: k)whereGA::TypeRep(a :: k1 -> k2)->TypeRep(b :: k1)->GetApp(a b)getAppR::TypeRep(a :: k)->Maybe(GetApp a)dataG1 c a whereG1::TypeRep(a :: k)->G1(c :: k -> k')(c a)getR1::TypeRep(ct :: k1 -> k)->TypeRep(c'at :: k)->Maybe(G1 ct c'at)-- Implementation uses an unsafeCoercedataG2 c a whereG2::TypeRep(a :: k1)->TypeRep(b :: k2)->G2(c :: k1 -> k2 -> k3)(c a b)getR2::TypeRep(c :: k2 -> k1 -> k)->TypeRep(a :: k)->Maybe(G2 c a)-- Implementation uses an unsafeCoerce-- rest are for conveniencetypeOf::Typeable a =>(a ::*)->TypeRep a
|
|
|
getFnR::TypeRep(a ::*)->Maybe(G2(->) a)castR::TypeRep(a ::*)->TypeRep(b ::*)-> a ->Maybe b
|
|
|
cast::(Typeable(a ::*),Typeable(b ::*))=> a ->Maybe b
|
|
|
gcastR::TypeRep(a :: k)->TypeRep(b :: k)-> c a ->Maybe(c b)gcast::(Typeable(a :: k),Typeable(b :: k))=> c a ->Maybe(c b)gcastR1::TypeRep(t :: k1 -> k2)->TypeRep(t' :: k1 -> k2)-> c (t a)->Maybe(c (t' a))gcast1::(Typeable(t :: k1 -> k2),Typeable(t' :: k1 -> k2))=> c (t a)->Maybe(c (t' a))gcastR2::TypeRep(t :: k1 -> k2 -> k3)->TypeRep(t' :: k1 -> k2 -> k3)-> c (t a b)->Maybe(c (t' a b))gcast2::(Typeable(t :: k1 -> k2 -> k3),Typeable(t' :: k1 -> k2 -> k3))=> c (t a b)->Maybe(c (t' a b))
|
... | ... | @@ -67,7 +68,8 @@ gcastR::TypeRep(a :: k)->TypeRep(b :: k)-> c a ->Maybe(c b)gcast::(Typeable(a :: |
|
|
|
|
|
Notes:
|
|
|
|
|
|
- Many of these functions come in two variants: one which takes an explicit `TypeRep` argument, and one that take an implicit `TypeRep` argument via a `Typeable a` constraint. We use a consistend naming scheme: put an `R` suffix on variants that take an explicit `TypeRep` parameter, no suffix for `Typeable` constraint versions.
|
|
|
- Many of these functions come in two variants: one which takes an explicit `TypeRep` argument, and one that take an implicit `TypeRep` argument via a `Typeable a` constraint.
|
|
|
We use a consistent naming scheme: put an `R` suffix on variants that take an explicit `TypeRep` parameter, no suffix for `Typeable` constraint versions.
|
|
|
|
|
|
- Note that the type `(:~:)` comes from `Data.Type.Equality`.
|
|
|
|
... | ... | @@ -75,48 +77,55 @@ Notes: |
|
|
|
|
|
### Key differences from GHC 7.10
|
|
|
|
|
|
- The key difference is that `TypeRep` becomes type-indexed, so that if `x :: TypeRep [Int]` then `x` is a runtime-inspectable type representation for `[Int]`. It is poly-kinded, of course, so that `TypeRep Maybe` is fine.
|
|
|
- The key difference is that `TypeRep` becomes type-indexed, so that if `x :: TypeRep [Int]` then `x` is a runtime-inspectable type representation for `[Int]`.
|
|
|
It is poly-kinded, of course, so that `TypeRep Maybe` is fine.
|
|
|
|
|
|
- In class `Typeable`, the `typeRep` method therefore no longer needs a proxy arguemnt. Indeed the class dictionary precisely is a single type representation.
|
|
|
- In class `Typeable`, the `typeRep` method therefore no longer needs a proxy argument.
|
|
|
Indeed the class dictionary precisely is a single type representation.
|
|
|
|
|
|
- Functions for constructing and destructing `TypeRep`s differ, in particular destructing needs a GADT return type to deal with existentially hidden `TypeRep` indices.
|
|
|
|
|
|
### With kind equalities
|
|
|
|
|
|
|
|
|
Once we have kind equalities, we have a kind-hetrogenous `:~~:`. Now we do not `unsafeCoerce` in `getT1` and the like, so we can now just export `getAppT` and leave the rest to the users.
|
|
|
Once we have kind equalities, we have a kind-heterogeneous `:~~:`.
|
|
|
Now we do not `unsafeCoerce` in `getR1` and the like, so we can now just export `getAppR` and leave the rest to the users.
|
|
|
|
|
|
|
|
|
The changes are that `eqRR` now return `a:~~:b` rather than `Bool`, and are more useful (don't force us to use `unsafeCoerce`); `getT1` and `getT2` don't need `unsafeCoerce`, and we can generalise `getFnT` to be poly-kinded.
|
|
|
We obviously may want to provide (and deprecate) `getT1`, `eqRRHom` etc. for compatibility, and maybe provide `getFnT` for convenience, if it turns out to be used a lot etc.
|
|
|
The changes are that `eqRR` now return `a:~~:b` rather than `Bool`, and are more useful (don't force us to use `unsafeCoerce`); `getR1` and `getR2` don't need `unsafeCoerce`, and we can generalise `getFnR` to be poly-kinded.
|
|
|
We obviously may want to provide (and deprecate) `getR1`, `eqRRHom` etc. for compatibility, and maybe provide `getFnR` for convenience, if it turns out to be used a lot etc.
|
|
|
|
|
|
|
|
|
(I am not yet sure whether it would be useful to keep the homogenous equality functions around --- potentially enforcing kind homogeneity could be useful)
|
|
|
(I am not yet sure whether it would be useful to keep the homogeneous equality functions around --- potentially enforcing kind homogeneity could be useful)
|
|
|
|
|
|
### Trusted code base
|
|
|
|
|
|
|
|
|
The TCB consists of (in the homogenous case), the implementation of `data TypeRep`, `class Typeable` and its implementations, `eqRR` and `eqRRHom` (comparison of `TypeRep`s), `getR1` and `getR2` (decomposing `TypeRep`s); and the RTS support for building the static pointer table.
|
|
|
The TCB consists of (in the homogeneous case), the implementation of `data TypeRep`, `class Typeable` and its implementations, `eqRR` and `eqRRHom` (comparison of `TypeRep`s), `getR1` and `getR2` (decomposing `TypeRep`s).
|
|
|
As is currently done for `Typeable`, the instances for `Typeable` should be "magically" provided by GHC.
|
|
|
|
|
|
|
|
|
In the kind-hetrogenous case, `getR1` and `getR2` come out of the TCB.
|
|
|
In the kind-heterogeneous case, `getR1` and `getR2` come out of the TCB.
|
|
|
|
|
|
### Questions
|
|
|
|
|
|
- How many `getR1`, `getR2` etc should we provide?
|
|
|
- Do we want explicit names for some type representations?
|
|
|
Perhaps `typeRepTBool` etc., and just for Prelude defined types.
|
|
|
(It is nice to avoid writing `typeRepT :: TypeRep Bool`)
|
|
|
(It is nice to avoid writing `typeRep :: TypeRep Bool`)
|
|
|
- `TyCon` is now entirely hidden from the user.
|
|
|
Is there a use-case where this is not desirable?
|
|
|
|
|
|
---
|
|
|
|
|
|
## Data.Dynamic
|
|
|
|
|
|
|
|
|
Dynamic should be a fairly seamless changeover, since `Dynamic` is abstract currently (although we cannot provide a `dynTypeRep :: Dynamic -> TypeRep ?` function - this does not seem oft-used & can be avoided by pattern matching as our `DynamicT` is not abstract, or by providing a `Typeable` based on top of `Typeable`).
|
|
|
This should be a fairly seamless changeover, since `Dynamic` is abstract currently (although we cannot provide a `dynTypeRep :: Dynamic -> TypeRep ?` function - this does not seem oft-used & can be avoided by pattern matching as our `Dynamic` is not abstract).
|
|
|
|
|
|
|
|
|
API follows current API, except missing `dynTypeRep`, as detailed above.
|
|
|
Provide varients of functions that take explicit `TypeRep` arguments.
|
|
|
The API follows the current API, except missing `dynTypeRep`, as detailed above.
|
|
|
We provide variants of functions that take explicit `TypeRep` arguments.
|
|
|
|
|
|
```
|
|
|
dataDynamicwhereDynamic::TypeRep a -> a ->DynamictoDynR::TypeRep a -> a ->DynamictoDyn::Typeable a => a ->DynamicfromDynamicR::TypeRep a ->Dynamic->Maybe a
|
... | ... | @@ -136,7 +145,7 @@ fromSDyn::Typeable a =>SDynamic s -> s a -> s a |
|
|
|
|
|
Notes
|
|
|
|
|
|
- These is no trusted code here; i.e. no `unsafeCoreces` in the implementation.
|
|
|
- These is no trusted code here; i.e. no `unsafeCorece`s in the implementation.
|
|
|
|
|
|
- `Dynamic` is *not* abstract so that you can pattern match on it. If it was abstract we'd need to add
|
|
|
|
... | ... | @@ -144,10 +153,12 @@ Notes |
|
|
unpackDynamic :: Dynamic -> (forall a. TypeRep a -> a -> r) -> r
|
|
|
```
|
|
|
|
|
|
- `SDynamic` a mid-point between fully dynamic & fully static types. We statically know some "Shape" information, but not all info about type. e.g., `SDynamic Maye` contains a value that is definitely a `Maybe ty` for some type `ty`, but the type `ty` can vary between values of type `SDynamic Maybe`.
|
|
|
- `SDynamic` is a mid-point between fully dynamic & fully static types.
|
|
|
We statically know some "Shape" information, but not all info about type.
|
|
|
e.g., `SDynamic Maybe` contains a value that is definitely a `Maybe ty` for some type `ty`, but the type `ty` can vary between values of type `SDynamic Maybe`.
|
|
|
|
|
|
>
|
|
|
> One use-case is in the implementation of `StaticPtr`.
|
|
|
> >
|
|
|
> > One use-case is in the implementation of `StaticPtr`.
|
|
|
|
|
|
### Questions
|
|
|
|
... | ... | @@ -163,6 +174,11 @@ Note that the static pointer support requires a static pointer table in a differ |
|
|
|
|
|
TODO api, talk about poly
|
|
|
|
|
|
### Trusted Code Base
|
|
|
|
|
|
|
|
|
Just the RTS support for building the static pointer table.
|
|
|
|
|
|
### Questions
|
|
|
|
|
|
- The static "polymorphism" support is a bit kludgy - any comments on this would be most helpful!
|
... | ... | |