... | ... | @@ -43,13 +43,20 @@ These are issues that need to be addressed elsewhere in the compiler, |
|
|
|
|
|
## Immediate next steps
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Fix [\#11714](https://gitlab.haskell.org//ghc/ghc/issues/11714)
|
|
|
- Move things to a richer `TypeRep` representation to make user serialization implementations safer.
|
|
|
|
|
|
## Representing tycon kinds
|
|
|
|
|
|
|
|
|
In order to provide `typeRepKind` we must have some way of getting a kind from a `TrTyCon``TypeRep` node. There are two ways of doing this,
|
|
|
|
|
|
In order to provide `typeRepKind` we must have some way of getting a kind from a `TrTyCon` `TypeRep` node. There are two ways of doing this,
|
|
|
|
|
|
|
|
|
1. Making the `TrTyCon` carry its kind
|
|
|
1. Making the `TrTyCon` carry the instantiations of its kind variables and ensuring that we have a way of conjuring the final kind from these variables (e.g. encoding a representation of the type's uninstantiated kind in its `TyCon`)
|
... | ... | @@ -69,11 +76,15 @@ On the other hand, (2) lacks these disadvantages but presents a few challenges, |
|
|
### The need for kind representations
|
|
|
|
|
|
|
|
|
|
|
|
While `typeRepKind` may seem like a non-essential feature, it ends up being quite important in the presence of representationally polymorphic arrow lest we may produce ill-kinded type representations. Consider, for a moment, that we have a function, `mkApp`, which attempts to construct an application type from two `SomeTypeRep`s. It might look like,
|
|
|
|
|
|
|
|
|
```
|
|
|
mkApp::SomeTypeRep->SomeTypeRep->MaybeSomeTypeRepmkApp(SomeTypeRep f)(SomeTypeRep x)=doFunTy a b <- pure f
|
|
|
Refl<- a `eqTypeRep` typeRepKind x
|
|
|
mkApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
|
|
|
mkApp (SomeTypeRep f) (SomeTypeRep x) = do
|
|
|
FunTy a b <- pure f
|
|
|
Refl <- a `eqTypeRep` typeRepKind x
|
|
|
return (App f x)
|
|
|
```
|
|
|
|
... | ... | @@ -83,38 +94,78 @@ Note that before we can apply `x` to `f` we must prove to GHC that the kind of ` |
|
|
### Encoding kind instantiations
|
|
|
|
|
|
|
|
|
|
|
|
One approach would be,
|
|
|
|
|
|
|
|
|
```
|
|
|
typeKindBndr=IntdataKindRep=KindTyConTyCon|KindVar!KindBndr|KindAppKindRepKindRepdataTyCon=TyCon{ tyConName ::String,..., tyConKindRep ::KindRep}dataTypeRep(a :: k)whereTrCon::TyCon->[SomeTypeRep]->TypeRep a
|
|
|
TrApp::TypeRep a ->TypeRep b ->TypeRep(a b)dataSomeTypeRepwhereSomeTypeRep:: forall k (a :: k).TypeRep a ->SomeTypeRep
|
|
|
type KindBndr = Int
|
|
|
data KindRep = KindTyCon TyCon
|
|
|
| KindVar !KindBndr
|
|
|
| KindApp KindRep KindRep
|
|
|
|
|
|
data TyCon = TyCon { tyConName :: String, ...
|
|
|
, tyConKindRep :: KindRep
|
|
|
}
|
|
|
data TypeRep (a :: k) where
|
|
|
TrCon :: TyCon -> [SomeTypeRep] -> TypeRep a
|
|
|
TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
|
|
|
data SomeTypeRep where
|
|
|
SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
|
However this has the unfortunate side-effect of making the production of `TyCon`s (and hence all data types) significantly more expensive due to the need to produce `KindRep`.
|
|
|
|
|
|
|
|
|
|
|
|
An alternative to this would be to push the `KindRep` out of `TyCon` and into evidence generation,
|
|
|
|
|
|
|
|
|
```
|
|
|
typeKindBndr=IntdataKindRep=KindTyConTyCon|KindVar!KindBndr|KindAppKindRepKindRepdataTyCon=TyCon{ tyConName ::String,...}dataTypeRep(a :: k)whereTrCon::TyCon->KindRep->[SomeTypeRep]->TypeRep a
|
|
|
TrApp::TypeRep a ->TypeRep b ->TypeRep(a b)dataSomeTypeRepwhereSomeTypeRep:: forall k (a :: k).TypeRep a ->SomeTypeRep
|
|
|
type KindBndr = Int
|
|
|
data KindRep = KindTyCon TyCon
|
|
|
| KindVar !KindBndr
|
|
|
| KindApp KindRep KindRep
|
|
|
|
|
|
data TyCon = TyCon { tyConName :: String, ...
|
|
|
}
|
|
|
|
|
|
data TypeRep (a :: k) where
|
|
|
TrCon :: TyCon -> KindRep -> [SomeTypeRep] -> TypeRep a
|
|
|
TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
|
|
|
data SomeTypeRep where
|
|
|
SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
|
|
|
```
|
|
|
|
|
|
|
|
|
This has the advantage of only inflicting the cost of `KindRep` generation on users of `Typeable`. However, this means we lose sharing of `KindRep`s.
|
|
|
|
|
|
|
|
|
|
|
|
Another alternative would be to drop `KindRep` entirely and instead capture kinds through constraints,
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTyCon=TyCon{ tyConName ::String,...}dataTypeRep(a :: k)whereTrCon::TyCon->[SomeTypeRep]->TypeRep a
|
|
|
TrApp::TypeRep a ->TypeRep b ->TypeRep(a b)classTypeable k =>Typeable(a :: k)where
|
|
|
typeRep ::TypeRep a
|
|
|
data TyCon = TyCon { tyConName :: String, ...
|
|
|
}
|
|
|
|
|
|
data TypeRep (a :: k) where
|
|
|
TrCon :: TyCon -> [SomeTypeRep] -> TypeRep a
|
|
|
TrApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
|
|
|
-- Which has slight consequences on withTypeable,withTypeable::Typeable k =>TypeRep(a :: k)->(Typeable a => r)-> r
|
|
|
class Typeable k => Typeable (a :: k) where
|
|
|
typeRep :: TypeRep a
|
|
|
|
|
|
-- Which has slight consequences on withTypeable,
|
|
|
withTypeable :: Typeable k => TypeRep (a :: k) -> (Typeable a => r) -> r
|
|
|
|
|
|
-- and SomeTypeRep
|
|
|
data SomeTypeRep where
|
|
|
SomeTypeRep :: forall k (a :: k). Typeable k => TypeRep a -> SomeTypeRep
|
|
|
```
|
|
|
|
|
|
## Notes from meeting with Simon (5 Oct. 2016)
|
... | ... | @@ -139,8 +190,10 @@ Instead of encoding the kind of a constructor in `TrTyCon` let's encode its inst |
|
|
|
|
|
This slightly complicates the implementation of `typeRepKind`, however. We will need some way of moving from the list of kind variable instantiations to the resulting kind of a tycon. This will need to be encoded with the `TyCon` in a manner than can serialized. For instance,
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTyCon=TcString[String]TyConKindRepdataTyConKindRep=VarString|TyConAppTyCon[TyConKindRep]
|
|
|
data TyCon = Tc String [String] TyConKindRep
|
|
|
data TyConKindRep = Var String | TyConApp TyCon [TyConKindRep]
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -149,104 +202,112 @@ This unfortunately bloats the `TyCon` bindings produced by the compiler with eve |
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
Use Keyword = `Typeable` to ensure that a ticket ends up on these lists.
|
|
|
|
|
|
|
|
|
|
|
|
**Open Tickets:**
|
|
|
|
|
|
<table><tr><th>[\#10770](https://gitlab.haskell.org//ghc/ghc/issues/10770)</th>
|
|
|
<table><tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/10770">#10770</a></th>
|
|
|
<td>Typeable solver has strange effects</td></tr>
|
|
|
<tr><th>[\#11251](https://gitlab.haskell.org//ghc/ghc/issues/11251)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11251">#11251</a></th>
|
|
|
<td>isInstance does not work on Typeable with base-4.8 anymore</td></tr>
|
|
|
<tr><th>[\#11349](https://gitlab.haskell.org//ghc/ghc/issues/11349)</th>
|
|
|
<td>\[TypeApplications\] Create Proxy-free alternatives of functions in base</td></tr>
|
|
|
<tr><th>[\#11715](https://gitlab.haskell.org//ghc/ghc/issues/11715)</th>
|
|
|
<td>Constraint vs \*</td></tr>
|
|
|
<tr><th>[\#12451](https://gitlab.haskell.org//ghc/ghc/issues/12451)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11349">#11349</a></th>
|
|
|
<td>[TypeApplications] Create Proxy-free alternatives of functions in base</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11715">#11715</a></th>
|
|
|
<td>Constraint vs *</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12451">#12451</a></th>
|
|
|
<td>TemplateHaskell and Data.Typeable - tcIfaceGlobal (local): not found</td></tr>
|
|
|
<tr><th>[\#13261](https://gitlab.haskell.org//ghc/ghc/issues/13261)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13261">#13261</a></th>
|
|
|
<td>Consider moving Typeable evidence generation wholly back to solver</td></tr>
|
|
|
<tr><th>[\#13276](https://gitlab.haskell.org//ghc/ghc/issues/13276)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13276">#13276</a></th>
|
|
|
<td>Unboxed sums are not Typeable</td></tr>
|
|
|
<tr><th>[\#13647](https://gitlab.haskell.org//ghc/ghc/issues/13647)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13647">#13647</a></th>
|
|
|
<td>Tidy up TcTypeable</td></tr>
|
|
|
<tr><th>[\#13933](https://gitlab.haskell.org//ghc/ghc/issues/13933)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13933">#13933</a></th>
|
|
|
<td>Support Typeable instances for types with coercions</td></tr>
|
|
|
<tr><th>[\#14190](https://gitlab.haskell.org//ghc/ghc/issues/14190)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14190">#14190</a></th>
|
|
|
<td>Typeable imposes seemingly redundant constraints on polykinded instances</td></tr>
|
|
|
<tr><th>[\#14255](https://gitlab.haskell.org//ghc/ghc/issues/14255)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14255">#14255</a></th>
|
|
|
<td>Type-indexed type fingerprints</td></tr>
|
|
|
<tr><th>[\#14270](https://gitlab.haskell.org//ghc/ghc/issues/14270)</th>
|
|
|
<td>GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal</td></tr>
|
|
|
<tr><th>[\#14337](https://gitlab.haskell.org//ghc/ghc/issues/14337)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14270">#14270</a></th>
|
|
|
<td>GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14337">#14337</a></th>
|
|
|
<td>typeRepKind can perform substantial amounts of allocation</td></tr>
|
|
|
<tr><th>[\#14341](https://gitlab.haskell.org//ghc/ghc/issues/14341)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14341">#14341</a></th>
|
|
|
<td>Show instance for TypeReps is a bit broken</td></tr>
|
|
|
<tr><th>[\#14401](https://gitlab.haskell.org//ghc/ghc/issues/14401)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14401">#14401</a></th>
|
|
|
<td>Add a test ensuring that TypeReps can be stored in compact regions</td></tr>
|
|
|
<tr><th>[\#14480](https://gitlab.haskell.org//ghc/ghc/issues/14480)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14480">#14480</a></th>
|
|
|
<td>Clean up tyConTYPE</td></tr>
|
|
|
<tr><th>[\#14582](https://gitlab.haskell.org//ghc/ghc/issues/14582)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14582">#14582</a></th>
|
|
|
<td>Review and improve the Typeable API</td></tr>
|
|
|
<tr><th>[\#14663](https://gitlab.haskell.org//ghc/ghc/issues/14663)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14663">#14663</a></th>
|
|
|
<td>Deriving Typeable for enumerations seems expensive</td></tr>
|
|
|
<tr><th>[\#15322](https://gitlab.haskell.org//ghc/ghc/issues/15322)</th>
|
|
|
<td>\`KnownNat\` does not imply \`Typeable\` any more when used with plugin</td></tr>
|
|
|
<tr><th>[\#15862](https://gitlab.haskell.org//ghc/ghc/issues/15862)</th>
|
|
|
<td>Panic with promoted types that Typeable doesn't support</td></tr></table>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15322">#15322</a></th>
|
|
|
<td>`KnownNat` does not imply `Typeable` any more when used with plugin</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15862">#15862</a></th>
|
|
|
<td>Panic with promoted types that Typeable doesn't support</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
**Closed Tickets:**
|
|
|
|
|
|
<table><tr><th>[\#3480](https://gitlab.haskell.org//ghc/ghc/issues/3480)</th>
|
|
|
<table><tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/3480">#3480</a></th>
|
|
|
<td>Easily make Typeable keys pure, so that Typeable can be handled efficiently across communications</td></tr>
|
|
|
<tr><th>[\#8931](https://gitlab.haskell.org//ghc/ghc/issues/8931)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/8931">#8931</a></th>
|
|
|
<td>The type defaulting in GHCi with Typeable</td></tr>
|
|
|
<tr><th>[\#9639](https://gitlab.haskell.org//ghc/ghc/issues/9639)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9639">#9639</a></th>
|
|
|
<td>Remove OldTypeable</td></tr>
|
|
|
<tr><th>[\#9707](https://gitlab.haskell.org//ghc/ghc/issues/9707)</th>
|
|
|
<td>(Try to) restructure \`base\` to allow more use of \`AutoDeriveTypeable\`</td></tr>
|
|
|
<tr><th>[\#10163](https://gitlab.haskell.org//ghc/ghc/issues/10163)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/9707">#9707</a></th>
|
|
|
<td>(Try to) restructure `base` to allow more use of `AutoDeriveTypeable`</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/10163">#10163</a></th>
|
|
|
<td>Export typeRepKinds in Data.Typeable</td></tr>
|
|
|
<tr><th>[\#10343](https://gitlab.haskell.org//ghc/ghc/issues/10343)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/10343">#10343</a></th>
|
|
|
<td>Make Typeable track kind information better</td></tr>
|
|
|
<tr><th>[\#11011](https://gitlab.haskell.org//ghc/ghc/issues/11011)</th>
|
|
|
<td>Add type-indexed type representations (\`TypeRep a\`)</td></tr>
|
|
|
<tr><th>[\#11120](https://gitlab.haskell.org//ghc/ghc/issues/11120)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11011">#11011</a></th>
|
|
|
<td>Add type-indexed type representations (`TypeRep a`)</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11120">#11120</a></th>
|
|
|
<td>Missing type representations</td></tr>
|
|
|
<tr><th>[\#11714](https://gitlab.haskell.org//ghc/ghc/issues/11714)</th>
|
|
|
<td>Kind of (-\>) type constructor is overly constrained</td></tr>
|
|
|
<tr><th>[\#11722](https://gitlab.haskell.org//ghc/ghc/issues/11722)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11714">#11714</a></th>
|
|
|
<td>Kind of (->) type constructor is overly constrained</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11722">#11722</a></th>
|
|
|
<td>No TypeRep for unboxed tuples</td></tr>
|
|
|
<tr><th>[\#11736](https://gitlab.haskell.org//ghc/ghc/issues/11736)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/11736">#11736</a></th>
|
|
|
<td>Allow unsaturated uses of unlifted types in Core</td></tr>
|
|
|
<tr><th>[\#12082](https://gitlab.haskell.org//ghc/ghc/issues/12082)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12082">#12082</a></th>
|
|
|
<td>Typeable on RealWorld fails</td></tr>
|
|
|
<tr><th>[\#12123](https://gitlab.haskell.org//ghc/ghc/issues/12123)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12123">#12123</a></th>
|
|
|
<td>GHC crashes when calling typeRep on a promoted tuple</td></tr>
|
|
|
<tr><th>[\#12409](https://gitlab.haskell.org//ghc/ghc/issues/12409)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12409">#12409</a></th>
|
|
|
<td>Unboxed tuples have no type representations</td></tr>
|
|
|
<tr><th>[\#12670](https://gitlab.haskell.org//ghc/ghc/issues/12670)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12670">#12670</a></th>
|
|
|
<td>Representation polymorphism validity check is too strict</td></tr>
|
|
|
<tr><th>[\#12905](https://gitlab.haskell.org//ghc/ghc/issues/12905)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/12905">#12905</a></th>
|
|
|
<td>Core lint failure with pattern synonym and levity polymorphism</td></tr>
|
|
|
<tr><th>[\#13197](https://gitlab.haskell.org//ghc/ghc/issues/13197)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13197">#13197</a></th>
|
|
|
<td>Perplexing levity polymorphism issue</td></tr>
|
|
|
<tr><th>[\#13333](https://gitlab.haskell.org//ghc/ghc/issues/13333)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13333">#13333</a></th>
|
|
|
<td>Typeable regression in GHC HEAD</td></tr>
|
|
|
<tr><th>[\#13871](https://gitlab.haskell.org//ghc/ghc/issues/13871)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13871">#13871</a></th>
|
|
|
<td>GHC panic in 8.2 only: typeIsTypeable(Coercion)</td></tr>
|
|
|
<tr><th>[\#13872](https://gitlab.haskell.org//ghc/ghc/issues/13872)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13872">#13872</a></th>
|
|
|
<td>Strange Typeable error message involving TypeInType</td></tr>
|
|
|
<tr><th>[\#13915](https://gitlab.haskell.org//ghc/ghc/issues/13915)</th>
|
|
|
<td>GHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instance</td></tr>
|
|
|
<tr><th>[\#14199](https://gitlab.haskell.org//ghc/ghc/issues/14199)</th>
|
|
|
<td>Document Type.Reflection better (Fun and Con')</td></tr>
|
|
|
<tr><th>[\#14254](https://gitlab.haskell.org//ghc/ghc/issues/14254)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/13915">#13915</a></th>
|
|
|
<td>GHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instance</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14199">#14199</a></th>
|
|
|
<td>Document Type.Reflection better (Fun and Con')</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14254">#14254</a></th>
|
|
|
<td>The Binary instance for TypeRep smells a bit expensive</td></tr>
|
|
|
<tr><th>[\#14925](https://gitlab.haskell.org//ghc/ghc/issues/14925)</th>
|
|
|
<td>Non-ASCII type names get garbled when their \`TypeRep\` is shown</td></tr>
|
|
|
<tr><th>[\#15067](https://gitlab.haskell.org//ghc/ghc/issues/15067)</th>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/14925">#14925</a></th>
|
|
|
<td>Non-ASCII type names get garbled when their `TypeRep` is shown</td></tr>
|
|
|
<tr><th><a href="https://gitlab.haskell.org//ghc/ghc/issues/15067">#15067</a></th>
|
|
|
<td>When Typeable and unboxed sums collide, GHC panics</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
## `Type.Reflection`
|
|
|
|
|
|
|
... | ... | @@ -255,23 +316,89 @@ The new type-indexed typeable machinery will be exposed via a new module |
|
|
`Reflection` in particular has an unfortunate conflict with Edward Kmett's `reflection`
|
|
|
library). The user-visible interface of `Type.Reflection` will look like this,
|
|
|
|
|
|
|
|
|
```
|
|
|
-- The user-facing interfacemoduleType.ReflectionwhereclassTypeable(a :: k)-- This is how we get the representation for a typetypeRep:: forall (a :: k).Typeable a =>TypeRep a
|
|
|
-- The user-facing interface
|
|
|
module Type.Reflection where
|
|
|
|
|
|
class Typeable (a :: k)
|
|
|
|
|
|
-- This is how we get the representation for a type
|
|
|
typeRep :: 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 constructors
|
|
|
data TyCon
|
|
|
|
|
|
tyConPackage :: TyCon -> String
|
|
|
tyConModule :: TyCon -> String
|
|
|
tyConName :: TyCon -> String
|
|
|
|
|
|
-- A runtime type representation with O(1) access to a fingerprint.
|
|
|
data TypeRep (a :: k)
|
|
|
|
|
|
instance Show (TypeRep a)
|
|
|
|
|
|
-- Since TypeRep is indexed by its type and must be a singleton we can trivially
|
|
|
-- provide these
|
|
|
instance Eq (TypeRep a) where (==) _ _ = True
|
|
|
instance Ord (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).
|
|
|
pattern TRApp :: 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?
|
|
|
-- In practice you often need it when you need the TyCon
|
|
|
pattern TRCon :: forall k (a :: k). TyCon -> TypeRep a
|
|
|
|
|
|
-- Decompose functions, also bidirectional
|
|
|
pattern TRFun :: forall fun. ()
|
|
|
=> forall arg res. (fun ~ (arg -> res))
|
|
|
=> TypeRep arg
|
|
|
-> TypeRep res
|
|
|
-> 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
|
|
|
-- We can also request the kind of a type
|
|
|
typeRepKind :: TypeRep (a :: k) -> TypeRep k
|
|
|
|
|
|
-- 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
|
|
|
-- and compare types
|
|
|
eqTypeRep :: 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)
|
|
|
|
|
|
-- Decompose functions, also bidirectionalpatternTRFun:: forall fun.()=> forall arg res.(fun ~(arg -> res))=>TypeRep arg
|
|
|
->TypeRep res
|
|
|
->TypeRep fun
|
|
|
-- it can also be useful to quantify over the type such that we can, e.g.,
|
|
|
-- index a map on a type
|
|
|
data TypeRepX where
|
|
|
TypeRepX :: forall a. TypeRep a -> TypeRepX
|
|
|
|
|
|
-- We can also request the kind of a typetypeRepKind::TypeRep(a :: k)->TypeRep k
|
|
|
-- these have some useful instances
|
|
|
instance Eq TypeRepX
|
|
|
instance Ord TypeRepX
|
|
|
instance Show TypeRepX
|
|
|
|
|
|
-- 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
|
|
|
-- A `TypeRep a` gives rise to a `Typeable a` instance without loss of
|
|
|
-- confluence.
|
|
|
withTypeable :: TypeRep a -> (Typeable a => b) -> b
|
|
|
withTypeable = undefined
|
|
|
|
|
|
|
|
|
-- We can also allow the user to build up his own applications
|
|
|
mkTrApp :: 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`
|
... | ... | @@ -283,26 +410,60 @@ module. The goal of this is to preserve compatibility with the old |
|
|
`TypeRepX` under the new scheme. This gives us a very nice compatibility story
|
|
|
(thanks due to Richard Eisenberg for first proposing this),
|
|
|
|
|
|
|
|
|
```
|
|
|
moduleData.Typeable(-- We can use the same Typeable classI.Typeable,I.TyCon,I.tyConPackage,I.tyConModule,I.tyConName,(:~:)(Refl),moduleData.Typeable)whereimportType.Reflectionas I
|
|
|
importData.Type.Equality-- Merely expose TypeRepX opaquely under the old nametypeTypeRep=I.TypeRepXtypeOf:: forall a.Typeable a => a ->TypeReptypeOf_=I.typeRepX (Proxy::Proxy a)typeRep:: forall proxy a.Typeable a => proxy a ->TypeReptypeRep=I.typeRepX
|
|
|
module Data.Typeable
|
|
|
( -- We can use the same Typeable class
|
|
|
I.Typeable
|
|
|
, I.TyCon
|
|
|
, I.tyConPackage
|
|
|
, I.tyConModule
|
|
|
, I.tyConName
|
|
|
, (:~:)(Refl)
|
|
|
, module Data.Typeable
|
|
|
) where
|
|
|
|
|
|
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
|
|
|
import Type.Reflection as I
|
|
|
import Data.Type.Equality
|
|
|
|
|
|
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
|
|
|
-- Merely expose TypeRepX opaquely under the old name
|
|
|
type TypeRep = I.TypeRepX
|
|
|
|
|
|
funResultTy::TypeRep->TypeRep->MaybeTypeRepfunResultTy(I.TypeRepX f)(I.TypeRepX x)|JustHRefl<-(I.typeRep ::I.TypeRepType)`I.eqTypeRep`I.typeRepKind f
|
|
|
,I.TRFun arg res <- f
|
|
|
,JustHRefl<- arg `I.eqTypeRep` x
|
|
|
=Just(I.TypeRepX res)| otherwise
|
|
|
=NothingtypeRepTyCon::TypeRep->TyCon-- the old typeOfN exports from the pre-PolyKinds days can-- also be trivially provided.
|
|
|
typeOf :: forall a. Typeable a => a -> TypeRep
|
|
|
typeOf _ = I.typeRepX (Proxy :: Proxy a)
|
|
|
|
|
|
typeRep :: forall proxy a. Typeable a => proxy a -> TypeRep
|
|
|
typeRep = I.typeRepX
|
|
|
|
|
|
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
|
|
|
cast x
|
|
|
| Just HRefl <- ta `I.eqTypeRep` tb = Just x
|
|
|
| otherwise = Nothing
|
|
|
where
|
|
|
ta = I.typeRep :: I.TypeRep a
|
|
|
tb = I.typeRep :: I.TypeRep b
|
|
|
|
|
|
eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
|
|
|
eqT
|
|
|
| Just HRefl <- ta `I.eqTypeRep` tb = Just Refl
|
|
|
| otherwise = Nothing
|
|
|
where
|
|
|
ta = I.typeRep :: I.TypeRep a
|
|
|
tb = I.typeRep :: I.TypeRep b
|
|
|
|
|
|
funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep
|
|
|
funResultTy (I.TypeRepX f) (I.TypeRepX x)
|
|
|
| Just HRefl <- (I.typeRep :: I.TypeRep Type) `I.eqTypeRep` I.typeRepKind f
|
|
|
, I.TRFun arg res <- f
|
|
|
, Just HRefl <- arg `I.eqTypeRep` x
|
|
|
= Just (I.TypeRepX res)
|
|
|
| otherwise
|
|
|
= Nothing
|
|
|
|
|
|
typeRepTyCon :: TypeRep -> TyCon
|
|
|
|
|
|
-- the old typeOfN exports from the pre-PolyKinds days can
|
|
|
-- also be trivially provided.
|
|
|
```
|
|
|
|
|
|
## The representation serialization problem
|
... | ... | @@ -312,12 +473,15 @@ Serialization of type representations is a bit tricky in this new world. Let's |
|
|
say that we want to serialize (say, using the `binary` package), for instance, a
|
|
|
type-indexed map,
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTMap a
|
|
|
lookup::TypeRepX->TMap a ->Maybe a
|
|
|
insert::TypeRepX-> a ->TMap a ->TMap a
|
|
|
data TMap a
|
|
|
lookup :: TypeRepX -> TMap a -> Maybe a
|
|
|
insert :: TypeRepX -> a -> TMap a -> TMap a
|
|
|
|
|
|
-- we want to support these operations...getTMap::Binary a =>Get(TMap a)putTMap::Binary a =>TMap a ->Put
|
|
|
-- we want to support these operations...
|
|
|
getTMap :: Binary a => Get (TMap a)
|
|
|
putTMap :: Binary a => TMap a -> Put
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -330,14 +494,20 @@ Of course in order to provide `getTMap` and `putTMap` we need to be able to both |
|
|
serialize and deserialize `TypeRepX`s. Serialization poses no particular issue.
|
|
|
For instance, we might write,
|
|
|
|
|
|
|
|
|
```
|
|
|
instanceBinaryTyConputTypeRep::TypeRep a ->PutputTypeRep tr@(TRCon tc)=do put 0
|
|
|
instance Binary TyCon
|
|
|
|
|
|
putTypeRep :: TypeRep a -> Put
|
|
|
putTypeRep tr@(TRCon tc) = do put 0
|
|
|
put tc
|
|
|
putTypeRep (typeRepKind tr)putTypeRep(TRApp f x)=do put 1
|
|
|
putTypeRep (typeRepKind tr)
|
|
|
putTypeRep (TRApp f x) = do put 1
|
|
|
putTypeRep f
|
|
|
putTypeRep x
|
|
|
|
|
|
putTypeRepX::TypeRepX->PutputTypeRepX(TypeRepX rep)= putTypeRep rep
|
|
|
putTypeRepX :: TypeRepX -> Put
|
|
|
putTypeRepX (TypeRepX rep) = putTypeRep rep
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -349,10 +519,12 @@ Now let's try deserialization. |
|
|
### Deserialization
|
|
|
|
|
|
|
|
|
|
|
|
First, we need to define how deserialization should behave. For instance, defining
|
|
|
|
|
|
|
|
|
```
|
|
|
getTypeRep::Get(TypeRep a)
|
|
|
getTypeRep :: Get (TypeRep a)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -360,17 +532,28 @@ is a non-starter as we have no way to verify that the representation that we |
|
|
deserialize plausibly represents the type `a` that the user requests.
|
|
|
|
|
|
|
|
|
|
|
|
Instead, let's first consider `TypeRepX` (thanks to Adam Gundry for his guidance),
|
|
|
|
|
|
|
|
|
```
|
|
|
getTypeRepX::GetTypeRepXgetTypeRepX=do
|
|
|
tag <- get ::GetWord8case tag of0->do con <- get ::GetTyConTypeRepX rep_k <- getTypeRepX
|
|
|
case rep_k `eqTypeRep`(typeRep ::TypeRepType)ofJustHRefl-> pure $TypeRepX$ mkTrCon con rep_k
|
|
|
Nothing-> fail "getTypeRepX: Kind mismatch"1->doTypeRepX f <- getTypeRepX
|
|
|
getTypeRepX :: Get TypeRepX
|
|
|
getTypeRepX = do
|
|
|
tag <- get :: Get Word8
|
|
|
case tag of
|
|
|
0 -> do con <- get :: Get TyCon
|
|
|
TypeRepX rep_k <- getTypeRepX
|
|
|
case rep_k `eqTypeRep` (typeRep :: TypeRep Type) of
|
|
|
Just HRefl -> pure $ TypeRepX $ mkTrCon con rep_k
|
|
|
Nothing -> fail "getTypeRepX: Kind mismatch"
|
|
|
|
|
|
1 -> do TypeRepX f <- getTypeRepX
|
|
|
TypeRepX x <- getTypeRepX
|
|
|
case typeRepKind f ofTRFun arg _|JustHRefl<- arg `eqTypeRep` x ->
|
|
|
pure $TypeRepX$ mkTrApp f x
|
|
|
_-> fail "getTypeRepX: Kind mismatch"_-> fail "getTypeRepX: Invalid TypeRepX"
|
|
|
case typeRepKind f of
|
|
|
TRFun arg _ | Just HRefl <- arg `eqTypeRep` x ->
|
|
|
pure $ TypeRepX $ mkTrApp f x
|
|
|
_ -> fail "getTypeRepX: Kind mismatch"
|
|
|
_ -> fail "getTypeRepX: Invalid TypeRepX"
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -385,10 +568,14 @@ Note how we need to invoke type equality here to ensure, |
|
|
|
|
|
Given this we can easily implement `TypeRep a` given a representation of the expected `a`,
|
|
|
|
|
|
|
|
|
```
|
|
|
getTypeRep::Typeable a =>Get(TypeRep a)getTypeRep=doTypeRepX rep <- getTypeRepX
|
|
|
case rep `eqTypeRep`(typeRep ::TypeRep a)ofJustHRefl-> pure rep
|
|
|
Nothing-> fail "Binary: Type mismatch"
|
|
|
getTypeRep :: Typeable a => Get (TypeRep a)
|
|
|
getTypeRep = do
|
|
|
TypeRepX rep <- getTypeRepX
|
|
|
case rep `eqTypeRep` (typeRep :: TypeRep a) of
|
|
|
Just HRefl -> pure rep
|
|
|
Nothing -> fail "Binary: Type mismatch"
|
|
|
```
|
|
|
|
|
|
### Alternative: Through static data?
|
... | ... | @@ -407,10 +594,19 @@ Under the above proposal `TyCon` is merely a record of static metadata; it has n |
|
|
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`,
|
|
|
|
|
|
|
|
|
```
|
|
|
-- metadata describing a tycondataTyConMeta=TyConMeta{ tyConPackage ::String, tyConModule ::String, tyConName ::String}newtypeTyCon(a :: k)=TyConTyConMetapatternTRCon::TyCon a ->TypeRep a
|
|
|
-- metadata describing a tycon
|
|
|
data TyConMeta = TyConMeta { tyConPackage :: String
|
|
|
, tyConModule :: String
|
|
|
, tyConName :: String
|
|
|
}
|
|
|
newtype TyCon (a :: k) = TyCon TyConMeta
|
|
|
|
|
|
-- which allows us to providemkTyCon::TyCon a ->TypeRep a
|
|
|
pattern TRCon :: TyCon a -> TypeRep a
|
|
|
|
|
|
-- which allows us to provide
|
|
|
mkTyCon :: TyCon a -> TypeRep a
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -419,18 +615,37 @@ why we **should** do it. The only way you can produce a `TyCon` is from a `TypeR |
|
|
so ultimately you should be able to accomplish everything you can with type-index
|
|
|
`TyCon`s by just not destructuring the `TypeRep` from which it arose.
|
|
|
|
|
|
|
|
|
## `Data.Dynamic`
|
|
|
|
|
|
|
|
|
|
|
|
`Dynamic` doesn't really change,
|
|
|
|
|
|
|
|
|
```
|
|
|
moduleData.Dynamicwhere-- Dynamic itself no longer needs to be abstractdataDynamicwhereDynamic::TypeRep a -> a ->Dynamic-- ConstructiontoDynR::TypeRep a -> a ->DynamictoDyn::Typeable a => a ->Dynamic-- EliminationfromDynamicR::TypeRep a ->Dynamic->Maybe a
|
|
|
fromDynamic::Typeable a =>Dynamic->Maybe a
|
|
|
module Data.Dynamic where
|
|
|
|
|
|
-- fromDynR::TypeRep a ->Dynamic-> a -> a
|
|
|
fromDyn::Typeable a =>Dynamic-> a -> a
|
|
|
-- Dynamic itself no longer needs to be abstract
|
|
|
data Dynamic where
|
|
|
Dynamic :: TypeRep a -> a -> Dynamic
|
|
|
|
|
|
-- ApplicationdynApp::Dynamic->Dynamic->Dynamic-- Existing function; calls error on failure-- I think this should be deprecateddynApply::Dynamic->Dynamic->MaybeDynamic
|
|
|
-- Construction
|
|
|
toDynR :: TypeRep a -> a -> Dynamic
|
|
|
toDyn :: Typeable a => a -> Dynamic
|
|
|
|
|
|
-- Elimination
|
|
|
fromDynamicR :: TypeRep a -> Dynamic -> Maybe a
|
|
|
fromDynamic :: Typeable a => Dynamic -> Maybe a
|
|
|
|
|
|
--
|
|
|
fromDynR :: TypeRep a -> Dynamic -> a -> a
|
|
|
fromDyn :: Typeable a => Dynamic -> a -> a
|
|
|
|
|
|
-- Application
|
|
|
dynApp :: Dynamic -> Dynamic -> Dynamic -- Existing function; calls error on failure
|
|
|
-- I think this should be deprecated
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -439,13 +654,17 @@ Ben Pierce also |
|
|
variant of `Dynamic`, which models a value of dynamic type "inside" of a known
|
|
|
functor. He p
|
|
|
|
|
|
|
|
|
```
|
|
|
dataSDynamic s whereSDynamic::TypeRep a -> s a ->SDynamic s
|
|
|
data SDynamic s where
|
|
|
SDynamic :: TypeRep a -> s a -> SDynamic s
|
|
|
|
|
|
toSDynR::TypeRep a -> s a ->SDynamic s
|
|
|
toSDyn::Typeable a => s a ->SDynamic s
|
|
|
fromSDynamicR::TypeRep a ->SDynamic s ->Maybe(s a)fromSDynamic::Typeable a =>SDynamic s ->Maybe(s a)fromSDynR::TypeRep a ->SDynamic s -> s a -> s a
|
|
|
fromSDyn::Typeable a =>SDynamic s -> s a -> s a
|
|
|
toSDynR :: TypeRep a -> s a -> SDynamic s
|
|
|
toSDyn :: Typeable a => s a -> SDynamic s
|
|
|
fromSDynamicR :: TypeRep a -> SDynamic s -> Maybe (s a)
|
|
|
fromSDynamic :: Typeable a => SDynamic s -> Maybe (s a)
|
|
|
fromSDynR :: TypeRep a -> SDynamic s -> s a -> s a
|
|
|
fromSDyn :: Typeable a => SDynamic s -> s a -> s a
|
|
|
```
|
|
|
|
|
|
## Implementation notes
|
... | ... | @@ -471,12 +690,20 @@ generating representations for primitive types, which doesn't really change (see |
|
|
Step (2), however, changes slightly in that it needs to produce evidence for the
|
|
|
kind of type.
|
|
|
|
|
|
|
|
|
|
|
|
`Typeable` evidence is merely a `TypeRep`,
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTypeRep(a :: k)whereTrTyCon::!Fingerprint->!TyCon->TypeRep k ->TypeRep(a :: k)TrApp:: forall k1 k2 (a :: k1 -> k2)(b :: k1).!Fingerprint->TypeRep a
|
|
|
->TypeRep b
|
|
|
->TypeRep(a b)
|
|
|
data TypeRep (a :: k) where
|
|
|
TrTyCon :: !Fingerprint -> !TyCon -> TypeRep k -> TypeRep (a :: k)
|
|
|
|
|
|
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
|
|
|
!Fingerprint
|
|
|
-> TypeRep a
|
|
|
-> TypeRep b
|
|
|
-> TypeRep (a b)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -490,8 +717,13 @@ challenge (especially in the `TypeInType` world) as we now have to worry about |
|
|
recursive kind relationships during evidence generation. Thankfully there are
|
|
|
only a few types which we need to worry about,
|
|
|
|
|
|
|
|
|
```
|
|
|
TYPE::RuntimeRep->TYPE'PtrRepLiftedRuntimeRep::TYPE'PtrRepLifted'PtrRepLifted::RuntimeRep(->)::TYPE'PtrRepLifted->TYPE'PtrRepLifted->Type'PtrRepLiftedTYPE'PtrRepLifted::TYPE'PtrRepLifted
|
|
|
TYPE :: RuntimeRep -> TYPE 'PtrRepLifted
|
|
|
RuntimeRep :: TYPE 'PtrRepLifted
|
|
|
'PtrRepLifted :: RuntimeRep
|
|
|
(->) :: TYPE 'PtrRepLifted -> TYPE 'PtrRepLifted -> Type 'PtrRepLifted
|
|
|
TYPE 'PtrRepLifted :: TYPE 'PtrRepLifted
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -507,48 +739,90 @@ Instead, the implementation manually defines representations for these types in |
|
|
Another approach would be to to encode these special cases in the `TypeRep`
|
|
|
type itself
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTypeRep(a :: k)whereTrTyCon::!Fingerprint->!TyCon->TypeRep k ->TypeRep(a :: k)TrApp:: forall k1 k2 (a :: k1 -> k2)(b :: k1).!Fingerprint->TypeRep a
|
|
|
->TypeRep b
|
|
|
->TypeRep(a b)TrArrow:: forall k1 k2.!Fingerprint->TypeRep k1
|
|
|
->TypeRep k2
|
|
|
->TypeRep((->):: k1 -> k2 ->*)TrTYPE::TypeRepTYPETrType::TypeRep(TYPE'PtrRepLifted)TrRuntimeRep::TypeRepRuntimeRepTr'PtrRepLifted::TypeRep'PtrRepLifted
|
|
|
data TypeRep (a :: k) where
|
|
|
TrTyCon :: !Fingerprint -> !TyCon -> TypeRep k -> TypeRep (a :: k)
|
|
|
|
|
|
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
|
|
|
!Fingerprint
|
|
|
-> TypeRep a
|
|
|
-> TypeRep b
|
|
|
-> TypeRep (a b)
|
|
|
|
|
|
TrArrow :: forall k1 k2.
|
|
|
!Fingerprint
|
|
|
-> TypeRep k1
|
|
|
-> TypeRep k2
|
|
|
-> TypeRep ((->) :: k1 -> k2 -> *)
|
|
|
|
|
|
TrTYPE :: TypeRep TYPE
|
|
|
TrType :: TypeRep (TYPE 'PtrRepLifted)
|
|
|
|
|
|
TrRuntimeRep :: TypeRep RuntimeRep
|
|
|
Tr'PtrRepLifted :: TypeRep 'PtrRepLifted
|
|
|
```
|
|
|
|
|
|
|
|
|
(although `TrArrow` won't quite work yet due to [\#11714](https://gitlab.haskell.org//ghc/ghc/issues/11714))
|
|
|
|
|
|
|
|
|
|
|
|
With this we can easily write `typeRepKind`,
|
|
|
|
|
|
|
|
|
```
|
|
|
typeRepKind:: forall k (a :: k).TypeRep a ->TypeRep k
|
|
|
-- these cases are unchanged...typeRepKind(TrTyCon__ k)= k
|
|
|
typeRepKind(TrApp_ f _)=case typeRepKind f ofTRFun _arg res -> res
|
|
|
typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
|
|
|
-- these cases are unchanged...
|
|
|
typeRepKind (TrTyCon _ _ k) = k
|
|
|
typeRepKind (TrApp _ f _) = case typeRepKind f of TRFun _arg res -> res
|
|
|
|
|
|
-- these are new...typeRepKind(TrArrow x y)= mkTrApp (mkTrApp (TrArrowTrTypeTrType) x) y
|
|
|
typeRepKindTrTYPE= mkTrApp TrRuntimeRepTrTypetypeRepKindTrType=TrTypetypeRepKindTrRuntimeRep=TrTypetypeRepKindTr'PtrRepLifted=TrRuntimeRep
|
|
|
-- these are new...
|
|
|
typeRepKind (TrArrow x y) = mkTrApp (mkTrApp (TrArrow TrType TrType) x) y
|
|
|
typeRepKind TrTYPE = mkTrApp TrRuntimeRep TrType
|
|
|
typeRepKind TrType = TrType
|
|
|
typeRepKind TrRuntimeRep = TrType
|
|
|
typeRepKind Tr'PtrRepLifted = TrRuntimeRep
|
|
|
```
|
|
|
|
|
|
|
|
|
Although providing pattern synonyms to allow decomposition of, e.g.,
|
|
|
`TYPE 'PtrTypeLifted` becomes a bit trickier,
|
|
|
|
|
|
|
|
|
```
|
|
|
-- Just as above, we can decompose applications but we-- now need to define it in terms of the splitApp helper,patternTRApp:: forall k2 (t :: k2).()=> forall k1 (a :: k1 -> k2)(b :: k1).(t ~ a b)=>TypeRep a ->TypeRep b ->TypeRep t
|
|
|
patternTRApp x y =(splitApp ->Just(App x y))dataAppResult(t :: k)whereApp::TypeRep a ->TypeRep b ->AppResult(a b)splitApp::TypeRep a ->Maybe(AppResult a)splitApp(TrTyCon___)=NothingsplitApp(TrApp_ f x)=Just$App f x
|
|
|
splitApp(TrArrow_ x y)=Just$App(mkTrApp (TrArrow(typeRepKind x)(typeRepKind y)) x) y
|
|
|
splitAppTrTYPE=NothingsplitAppTrType=Just$AppTrTYPETr'PtrRepLiftedsplitAppTrRuntimeRep=NothingsplitAppTr'PtrRepLifted=Nothing
|
|
|
-- Just as above, we can decompose applications but we
|
|
|
-- now need to define it in terms of the splitApp helper,
|
|
|
pattern TRApp :: forall k2 (t :: k2). ()
|
|
|
=> forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
|
|
|
=> TypeRep a -> TypeRep b -> TypeRep t
|
|
|
pattern TRApp x y = (splitApp -> Just (App x y))
|
|
|
|
|
|
data AppResult (t :: k) where
|
|
|
App :: TypeRep a -> TypeRep b -> AppResult (a b)
|
|
|
|
|
|
splitApp :: TypeRep a -> Maybe (AppResult a)
|
|
|
splitApp (TrTyCon _ _ _) = Nothing
|
|
|
splitApp (TrApp _ f x) = Just $ App f x
|
|
|
splitApp (TrArrow _ x y) = Just $ App (mkTrApp (TrArrow (typeRepKind x) (typeRepKind y)) x) y
|
|
|
splitApp TrTYPE = Nothing
|
|
|
splitApp TrType = Just $ App TrTYPE Tr'PtrRepLifted
|
|
|
splitApp TrRuntimeRep = Nothing
|
|
|
splitApp Tr'PtrRepLifted = Nothing
|
|
|
```
|
|
|
|
|
|
|
|
|
Pretty much everything else follows from this. For instance `TRFun`,
|
|
|
|
|
|
|
|
|
```
|
|
|
patternTRFun:: forall fun.()=> forall arg res.(fun ~(arg -> res))=>TypeRep arg
|
|
|
->TypeRep res
|
|
|
->TypeRep fun
|
|
|
patternTRFun arg res <-TRApp_(TRApp_(TrArrow__) arg) res whereTRFun arg res = mkTrApp (mkTrApp trArrow arg) res
|
|
|
pattern TRFun :: forall fun. ()
|
|
|
=> forall arg res. (fun ~ (arg -> res))
|
|
|
=> TypeRep arg
|
|
|
-> TypeRep res
|
|
|
-> TypeRep fun
|
|
|
pattern TRFun arg res <- TRApp _ (TRApp _ (TrArrow _ _) arg) res where
|
|
|
TRFun arg res = mkTrApp (mkTrApp trArrow arg) res
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -559,6 +833,9 @@ needs to take care to normalize representations that it builds (e.g. prefer |
|
|
`TrType` to `TrApp TrTYPE Tr'PtrRepLifted`). That being said, it may be a bit
|
|
|
more efficient for the compiler to produce dictionaries in this form.
|
|
|
|
|
|
|
|
|
```
|
|
|
mkApp::TypeRep a ->TypeRep b ->TypeRep(a b)mkAppTrTYPETr'PtrRepLifted=TrTypemkAppTrTYPE
|
|
|
mkApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
|
|
|
mkApp TrTYPE Tr'PtrRepLifted = TrType
|
|
|
mkApp TrTYPE
|
|
|
``` |
|
|
\ No newline at end of file |