... | @@ -5,28 +5,59 @@ This is Ben Gamari's plan for moving ahead with the type-indexed `Typeable` |
... | @@ -5,28 +5,59 @@ This is Ben Gamari's plan for moving ahead with the type-indexed `Typeable` |
|
scheme, described most recently in
|
|
scheme, described most recently in
|
|
[ A reflection on types](http://research.microsoft.com/en-us/um/people/simonpj/papers/haskell-dynamic/).
|
|
[ A reflection on types](http://research.microsoft.com/en-us/um/people/simonpj/papers/haskell-dynamic/).
|
|
|
|
|
|
## `Data.Typeable`
|
|
## `Type.Reflection`
|
|
|
|
|
|
|
|
|
|
The user-visible interface of `Data.Typeable` will look like this,
|
|
The new type-indexed typeable machinery will be exposed via a new module
|
|
|
|
(`Type.Reflection` is chosen here, although this name is still up in the air;
|
|
|
|
`Reflection` in particular has an unfortunate conflict with Edward Kmett's `reflection`
|
|
|
|
library). The user-visible interface of `GHC.Reflection` will look like this,
|
|
|
|
|
|
```
|
|
```
|
|
-- The user-facing interfacemoduleData.TypeablewhereclassTypeable(a :: k)-- This is how we get the representation for a typetypeRep:: forall (a :: k).Typeable a =>TypeRep a
|
|
-- The user-facing interfacemoduleType.ReflectionwhereclassTypeable(a :: k)-- This is how we get the representation for a typetypeRep:: forall (a :: k).Typeable a =>TypeRep a
|
|
|
|
|
|
-- This is merely a record of some metadata about a type constructor.-- One of these is produced for every type defined in a module during its-- compilation.---- This should also carry a fingerprint; to address #7897 this fingerprint-- should hash not only the name of the tycon, but also the structure of its-- data constructorsdataTyContyConPackage::TyCon->StringtyConModule::TyCon->StringtyConName::TyCon->String-- A runtime type representation with O(1) access to a fingerprint.dataTypeRep(a :: k)instanceShow(TypeRep a)-- Since TypeRep is indexed by its type and must be a singleton we can trivially-- provide theseinstanceEq(TTypeRep a)where(==)__=TrueinstanceOrd(TTypeRep a)where compare __=EQ-- While TypeRep is abstract, we can pattern match against it:patternTRApp:: forall k2 (fun :: k2).()=> forall k1 (a :: k1 -> k2)(b :: k1).(fun ~ a b)=>TypeRep a ->TypeRep b ->TypeRep fun
|
|
-- This is merely a record of some metadata about a type constructor.-- One of these is produced for every type defined in a module during its-- compilation.---- This should also carry a fingerprint; to address #7897 this fingerprint-- should hash not only the name of the tycon, but also the structure of its-- data constructorsdataTyContyConPackage::TyCon->StringtyConModule::TyCon->StringtyConName::TyCon->String-- A runtime type representation with O(1) access to a fingerprint.dataTypeRep(a :: k)instanceShow(TypeRep a)-- Since TypeRep is indexed by its type and must be a singleton we can trivially-- provide theseinstanceEq(TypeRep a)where(==)__=TrueinstanceOrd(TypeRep a)where compare __=EQ-- While TypeRep is abstract, we can pattern match against it.-- This can be a bi-directional pattern (using mkTrApp for construction).patternTRApp:: forall k2 (fun :: k2).()=> forall k1 (a :: k1 -> k2)(b :: k1).(fun ~ a b)=>TypeRep a ->TypeRep b ->TypeRep fun
|
|
|
|
|
|
-- Open question: Should this pattern include the kind of the constructor?-- It seems you often need it.patternTRCon:: forall k (a :: k).TyCon->TypeRep a
|
|
-- Open question: Should this pattern include the kind of the constructor?-- In practice you often need it when you need the TyConpatternTRCon:: forall k (a :: k).TyCon->TypeRep a
|
|
|
|
|
|
-- decompose functionspatternTRFun:: forall fun.()=> forall arg res.(fun ~(arg -> res))=>TypeRep arg
|
|
-- decompose functionspatternTRFun:: forall fun.()=> forall arg res.(fun ~(arg -> res))=>TypeRep arg
|
|
->TypeRep res
|
|
->TypeRep res
|
|
->TypeRep fun
|
|
->TypeRep fun
|
|
|
|
|
|
-- We can also request the kind of a typetTypeRepKind::TypeRep(a :: k)->TypeRep k
|
|
-- We can also request the kind of a typetypeRepKind::TypeRep(a :: k)->TypeRep k
|
|
|
|
|
|
|
|
-- and compare typeseqTypeRep:: forall k (a :: k)(b :: k).TypeRep a ->TypeRep b ->Maybe(a :~: b)eqTypeRep':: forall k1 k2 (a :: k1)(b :: k2).TypeRep a ->TypeRep b ->Maybe(a :~~: b)-- it can also be useful to quantify over the type such that we can, e.g.,-- index a map on a typedataTypeRepXwhereTypeRepX:: forall a.TypeRep a ->TypeRepX-- these have some useful instancesinstanceEqTypeRepXinstanceOrdTypeRepXinstanceShowTypeRepX-- A `TypeRep a` gives rise to a `Typeable a` instance without loss of-- confluence.withTypeable::TypeRep a ->(Typeable a => b)-> b
|
|
withTypeable= undefined
|
|
withTypeable= undefined
|
|
|
|
|
|
|
|
-- We can also allow the user to build up his own applicationsmkTrApp:: forall k1 k2 (a :: k1 -> k2)(b :: k1).TypeRep(a :: k1 -> k2)->TypeRep(b :: k1)->TypeRep(a b)-- However, we can't (easily) allow instantiation of TyCons since we have-- no way of producing the kind of the resulting type...--mkTrCon :: forall k (a :: k). TyCon -> [TypeRepX] -> TypeRep a
|
|
|
|
```
|
|
|
|
|
|
|
|
## Preserving compatibility with `Data.Typeable`
|
|
|
|
|
|
|
|
|
|
|
|
Note how above we placed the new type-indexed typeable in an entirely new
|
|
|
|
module. The goal of this is to preserve compatibility with the old
|
|
|
|
`Data.Typeable`. Notice how the old `Data.Typeable.TypeRep` is essentially
|
|
|
|
`TypeRepX` under the new scheme. This gives us a very nice compatibility story,
|
|
|
|
as noted by Richard Eisenberg,
|
|
|
|
|
|
|
|
```
|
|
|
|
moduleData.Typeable(I.Typeable,moduleData.Typeable)whereimportType.Reflectionas I
|
|
|
|
|
|
|
|
-- | A quantified type representation.typeTypeRep=I.TypeRepXtypeOf:: forall a.Typeable a => a ->TypeReptypeOf_=I.typeRepX (Proxy::Proxy a)typeRep:: forall proxy a.Typeable a => proxy a ->TypeReptypeRep=I.typeRepX
|
|
|
|
|
|
|
|
cast:: forall a b.(Typeable a,Typeable b)=> a ->Maybe b
|
|
|
|
cast x
|
|
|
|
|JustHRefl<- ta `I.eqTypeRep` tb =Just x
|
|
|
|
| otherwise =Nothingwhere
|
|
|
|
ta =I.typeRep ::I.TypeRep a
|
|
|
|
tb =I.typeRep ::I.TypeRep b
|
|
|
|
|
|
|
|
eqT:: forall a b.(Typeable a,Typeable b)=>Maybe(a :~: b)eqT|JustHRefl<- ta `I.eqTypeRep` tb =JustRefl| otherwise =Nothingwhere
|
|
|
|
ta =I.typeRep ::I.TypeRep a
|
|
|
|
tb =I.typeRep ::I.TypeRep b
|
|
|
|
|
|
|
|
typeRepTyCon::TypeRep->TyCon-- the old typeOfN exports from the pre-PolyKinds days can-- also be trivially provided.
|
|
```
|
|
```
|
|
|
|
|
|
## The representation serialization problem
|
|
## The representation serialization problem
|
... | @@ -73,9 +104,6 @@ Now let's try deserialization. |
... | @@ -73,9 +104,6 @@ Now let's try deserialization. |
|
### Deserialization
|
|
### Deserialization
|
|
|
|
|
|
|
|
|
|
We first need to consider which of these two types, `TypeRep` and `TypeRepX`, we want to imp
|
|
|
|
|
|
|
|
|
|
|
|
First, we need to define how deserialization should behave. For instance, defining
|
|
First, we need to define how deserialization should behave. For instance, defining
|
|
|
|
|
|
```
|
|
```
|
... | @@ -84,89 +112,67 @@ getTypeRep::Get(TypeRep a) |
... | @@ -84,89 +112,67 @@ getTypeRep::Get(TypeRep a) |
|
|
|
|
|
|
|
|
|
is a non-starter as we have no way to verify that the representation that we
|
|
is a non-starter as we have no way to verify that the representation that we
|
|
read plausibly represents the type `a` that the user requests.
|
|
deserialize plausibly represents the type `a` that the user requests.
|
|
|
|
|
|
|
|
|
|
For this we need more information: a `Typeable` dictionary,
|
|
Instead, let's first consider `TypeRepX` (thanks to Adam Gundry for his guidance),
|
|
|
|
|
|
```
|
|
```
|
|
getTypeRep::TypeRep a ->Get(TypeRep a)getTypeRep ty =do
|
|
getTypeRepX::GetTypeRepXgetTypeRepX=do
|
|
tag <- get ::GetWord8case tag of0|TRCon con <- ty ->do
|
|
tag <- get ::GetWord8case tag of0->do con <- get ::GetTyConTypeRepX rep_k <- getTypeRepX
|
|
con' <- get
|
|
case rep_k `eqTypeRep`(typeRep ::TypeRepType)ofJustHRefl-> pure $TypeRepX$ mkTrCon con rep_k
|
|
when (con' /= con)$ fail "Binary: Mismatched type constructors"
|
|
Nothing-> fail "getTypeRepX: Kind mismatch"1->doTypeRepX f <- getTypeRepX
|
|
getTypeRep (typeRepKind ty)1|TRApp rep_f rep_x <- ty ->do
|
|
TypeRepX x <- getTypeRepX
|
|
getTypeRep rep_f
|
|
case typeRepKind f ofTRFun arg _|JustHRefl<- arg `eqTypeRep` x ->
|
|
getTypeRep rep_x
|
|
pure $TypeRepX$ mkTrApp f x
|
|
pure ty
|
|
_-> fail "getTypeRepX: Kind mismatch"_-> fail "getTypeRepX: Invalid TypeRepX"
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
|
Note how here we aren't even constructing a new representation; we are merely
|
|
Note how we need to invoke type equality here to ensure,
|
|
verifying that what we deserialize matches the representation that we expect.
|
|
|
|
Of course, the fact that we must know the type we are trying to deserialize
|
|
|
|
means that `getTypeRep` isn't terribly useful on its own; it certainly won't
|
|
|
|
help us to deserialize a `TMap`.
|
|
|
|
|
|
|
|
|
|
|
|
Then what of `TypeRepX`? We clearly can't use the `getTypeRep` defined above
|
|
|
|
since it requires that we already know which type we expect.
|
|
|
|
If we are willing to bypass the typechecker entirely, we can deserialize thusly,
|
|
|
|
|
|
|
|
```
|
|
- in the case of a tycon: that the tycon's kind is `Type` (as all kinds must be in the `TypeInType` scheme)
|
|
getTypeRepX::GetTypeRepXgetTypeRepX=do
|
|
- in the case of applications `f x`:
|
|
tag <- get ::GetWord8case tag of0->do
|
|
|
|
con <- get
|
|
|
|
TypeRepX rep_k <- getTypeRepX
|
|
|
|
pure $TypeRepX$ mkTyCon con (unsafeCoerce rep_k)1->doTypeRepX rep_f <- getTypeRepX
|
|
|
|
TypeRepX rep_x <- getTypeRepX
|
|
|
|
pure $TypeRepX$ mkTRApp (unsafeCoerce rep_f) rep_x
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
- that the type `f` is indeed an arrow
|
|
|
|
- that the type `f` is applied at the type `x` that it expects
|
|
|
|
|
|
The `unsafeCoerce`s here appear as though they draw the deserialization
|
|
|
|
implementation into the trusted codebase. That being said, the consequences for
|
|
|
|
a user being able to construct an ill-kinded representation inside of a
|
|
|
|
`TypeRepX` are not so significant; this is because most of the
|
|
|
|
type-safety-critical operations that we expose require a `TypeRep`, which the
|
|
|
|
type system will disallow us from producing from an ill-kinded `TypeRepX` (TODO
|
|
|
|
This requires more careful reasoning).
|
|
|
|
|
|
|
|
|
|
Given this we can easily implement `TypeRep a` given a representation of the expected `a`,
|
|
If this is indeed safe, then this fact should be factored out into something like,
|
|
|
|
|
|
|
|
```
|
|
```
|
|
mkTrConX::TyCon->TypeRepX->TypeRepXmkTrConX tc (TypeRepX kind)=TypeRepX$ mkTyCon tc (unsafeCoerce kind)mkTrAppX::TypeRepX->TypeRepX->TypeRepXmkTrAppX(TypeRepX f)(TypeRepX x)=TypeRepX$ mkTRApp (unsafeCoerce f) x
|
|
getTypeRep::Typeable a =>Get(TypeRep a)getTypeRep=doTypeRepX rep <- getTypeRepX
|
|
|
|
case rep `eqTypeRep`(typeRep ::TypeRep a)ofJustHRefl-> pure rep
|
|
|
|
Nothing-> fail "Binary: Type mismatch"
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
|
Admittedly, exposing these does feel a bit odd as they totally break the
|
|
|
|
assumption that a `TypeRepX` wraps a valid type, even in the absence of
|
|
|
|
deserialization.
|
|
|
|
|
|
|
|
### Through static data?
|
|
### Through static data?
|
|
|
|
|
|
|
|
|
|
On might have the idea that the solution here may be to avoid encoding
|
|
One might have the idea that the solution here may be to avoid encoding
|
|
representations at all: instead use GHC's existing support for static data, e.g.
|
|
representations at all: instead use GHC's existing support for static data, e.g.
|
|
add `TypeRep a` entries to the static pointer table for every known type. But of
|
|
add `TypeRep a` entries to the static pointer table for every known type. One will quickly realize, however, that
|
|
course, this is unrealistic: we have no way of enumerating the types that must
|
|
this is unrealistic: we have no way of enumerating the types that must
|
|
be considered and even if we did, there would be very many of them.
|
|
be considered and even if we did, there would be very many of them.
|
|
|
|
|
|
### Through an un-indexed representation?
|
|
## Type-indexed `TyCon`s
|
|
|
|
|
|
|
|
|
|
The "give up" approach is to simply project the type-indexed `TypeRep` onto
|
|
Under the above proposal `TyCon` is merely a record of static metadata; it has no
|
|
something that is totally untyped,
|
|
type information and consequently the user is quite limited in what they can do with it.
|
|
|
|
Another point in the design space would be to add a type index to `TyCon`,
|
|
|
|
|
|
```
|
|
```
|
|
-- | A serializable type representationdataTypeRepS=TypeConSTyCon|TypeAppSTypeRepSTypeRepStoTypeRep::TypeRepS->Maybe(TypeRep a)toTypeRepX::TypeRepS->TypeRepXfromTypeRep::TypeRep a ->TypeRepSfromTypeRepX::TypeRepX->TypeRepS
|
|
-- metadata describing a tycondataTyConMeta=TyConMeta{ tyConPackage ::String, tyConModule ::String, tyConName ::String}newtypeTyCon(a :: k)=TyConTyConMetapatternTRCon::TyCon a ->TypeRep a
|
|
|
|
|
|
|
|
-- which allows us to providemkTyCon::TyCon a ->TypeRep a
|
|
```
|
|
```
|
|
|
|
|
|
`TypeRepS` is now just plain old data, requiring nothing special for
|
|
|
|
serialization and deserialization. However, this gives us an awkward third
|
|
While this is something that we could do, I have yet to see a compelling reason
|
|
variety of type representation. Moreover, if you may use `TypeRepX` or must
|
|
why we **should** do it. The only way you can produce a `TyCon` is from a `TypeRep`,
|
|
use `TypeRepS` is solely determined by the rather incidental matter of whether
|
|
so ultimately you should be able to accomplish everything you can with type-index
|
|
you need serialization.
|
|
`TyCon`s by just not destructuring the `TypeRep` from which it arose.
|
|
|
|
|
|
## `Data.Dynamic`
|
|
## `Data.Dynamic`
|
|
|
|
|
... | | ... | |