... | ... | @@ -28,134 +28,150 @@ The names of functions and type constructors is totally up for grabs. |
|
|
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>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
## Goal
|
|
|
|
|
|
|
|
|
|
|
|
Consider `Dynamic`:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataDynamicwhereDyn::TypeRep-> a ->Dynamic
|
|
|
data Dynamic where
|
|
|
Dyn :: TypeRep -> a -> Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
We'd like to write `dynApply`:
|
|
|
|
|
|
|
|
|
```
|
|
|
dynApply::Dynamic->Dynamic->MaybeDynamic
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
which succeeds only when the application is type correct. But how? Let's try
|
|
|
|
|
|
|
|
|
```
|
|
|
dynApply(Dyn tf f)(Dyn tx x)=???
|
|
|
dynApply (Dyn tf f) (Dyn tx x) = ???
|
|
|
```
|
|
|
|
|
|
|
|
|
We need some way to decompose `tf` (the type representation for `f`), ask if it is an arrow type, and if so extract the type representation for the argument and result type. Then we need to compare the argument type with `xt`'s representation. If so, we are good to go.
|
|
|
|
|
|
|
|
|
|
|
|
But at the moment we don't have any *type-safe* way to decompose `TypeRep`. Indeed `dynApply` is defined like this right now:
|
|
|
|
|
|
|
|
|
```
|
|
|
dynApply(Dyn tf f)(Dyn tx x)=case funResultTy tf tx ofJust tr ->Just(Dyn tr (unsafeCoerce f x))
|
|
|
dynApply (Dyn tf f) (Dyn tx x)
|
|
|
= case funResultTy tf tx of
|
|
|
Just tr -> Just (Dyn tr (unsafeCoerce f x))
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -172,21 +188,33 @@ So **our main goal is to be able to write `dynApply` in a type-safe way** so tha |
|
|
## Step 1: Type-indexed type representations
|
|
|
|
|
|
|
|
|
|
|
|
The first obvious thing is that we must make a connection between the type-rep arg of `Dyn` and the value itself. Something like this:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataDynamicwhereDyn::TTypeRep a -> a ->Dynamic
|
|
|
data Dynamic where
|
|
|
Dyn :: TTypeRep a -> a -> Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
Here we are using a *type-indexed* type representation, `TTypeRep`. Now the connection betweeen the two is visible to the type system.
|
|
|
|
|
|
|
|
|
|
|
|
We can re-define the `Typeable` class and `TypeRep` thus:
|
|
|
|
|
|
|
|
|
```
|
|
|
classTypeable a where
|
|
|
tTypeRep ::TTypeRep a -- No need for a proxy argument!dataTypeRepwhereTypeRep::TTypeRep a ->TypeReptypeRep::Typeable a => proxy a ->TypeRep-- The current typeRep functiontypeRep(p :: proxy a)=TypeRep(tTypeRep ::TTypeRep a)
|
|
|
class Typeable a where
|
|
|
tTypeRep :: TTypeRep a -- No need for a proxy argument!
|
|
|
|
|
|
data TypeRep where
|
|
|
TypeRep :: TTypeRep a -> TypeRep
|
|
|
|
|
|
typeRep :: Typeable a => proxy a -> TypeRep
|
|
|
-- The current typeRep function
|
|
|
typeRep (p :: proxy a) = TypeRep (tTypeRep :: TTypeRep a)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -199,18 +227,25 @@ It is helpful to have both `Typeable a` (the class) and `TTypeRep a` (the value) |
|
|
We can get from `Typeable a` to `TTypeRep` by using the class method `tTypeRep`. But what about the other way round?
|
|
|
We need to add the following primitive:
|
|
|
|
|
|
|
|
|
```
|
|
|
withTypeable::TTypeRep a ->(Typeable a => b)-> b
|
|
|
withTypeable :: TTypeRep a -> (Typeable a => b) -> b
|
|
|
```
|
|
|
|
|
|
|
|
|
(This seems both simpler and more useful than making the Typeable class recursive through TypeRep data declaration.) See more on the [sub-page](typeable/with-typeable).
|
|
|
|
|
|
|
|
|
|
|
|
We can also compare two `TTypeReps` to give a statically-usable proof of equality:
|
|
|
|
|
|
|
|
|
```
|
|
|
eqTT::TTypeRep a ->TTypeRep b ->Maybe(a :~: b)eqT::(Typeable a,Typeable b)=>Maybe(a :~: b)data a :~: b where-- Defined in Data.Typeable.EqualityRefl:: a :~: a
|
|
|
eqTT :: TTypeRep a -> TTypeRep b -> Maybe (a :~: b)
|
|
|
eqT :: (Typeable a, Typeable b) => Maybe (a :~: b)
|
|
|
|
|
|
data a :~: b where -- Defined in Data.Typeable.Equality
|
|
|
Refl :: a :~: a
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -221,38 +256,60 @@ eqTT::TTypeRep a ->TTypeRep b ->Maybe(a :~: b)eqT::(Typeable a,Typeable b)=>Mayb |
|
|
## Step 2: Decomposing functions
|
|
|
|
|
|
|
|
|
|
|
|
If we want to decompose `TTypable`, at least in the function arrow case, we need a function like this:
|
|
|
|
|
|
|
|
|
```
|
|
|
decomposeFun::TTypeRep fun
|
|
|
decomposeFun :: TTypeRep fun
|
|
|
-> r
|
|
|
-> (forall arg res. (fun ~ (arg->res))
|
|
|
=> TTypeRep arg -> TTypeRep res -> r)
|
|
|
-> r
|
|
|
->(forall arg res.(fun ~(arg->res))=>TTypeRep arg ->TTypeRep res -> r)-> r
|
|
|
-- (decomposeFun tf def k) sees if 'tf' is a function type-- If so, it applies 'k' to the argument and result type-- representations; if not, it returns 'def'
|
|
|
-- (decomposeFun tf def k) sees if 'tf' is a function type
|
|
|
-- If so, it applies 'k' to the argument and result type
|
|
|
-- representations; if not, it returns 'def'
|
|
|
```
|
|
|
|
|
|
|
|
|
This function is part of `Typeable`, and replaces `funResultTy`.
|
|
|
|
|
|
|
|
|
|
|
|
Now we can write `dynApply`, in a completely type-safe way, outside the TCB:
|
|
|
|
|
|
|
|
|
```
|
|
|
dynApply::Dynamic->Dynamic->MaybeDynamicdynApply(Dyn tf f)(Dyn tx x)= decomposeFun tf Nothing$\ ta tr ->case eqTT ta tx ofNothing->NothingJustRefl->Just(Dyn tr (f x))
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
dynApply (Dyn tf f) (Dyn tx x)
|
|
|
= decomposeFun tf Nothing $ \ ta tr ->
|
|
|
case eqTT ta tx of
|
|
|
Nothing -> Nothing
|
|
|
Just Refl -> Just (Dyn tr (f x))
|
|
|
```
|
|
|
|
|
|
|
|
|
**Pattern synonyms**. An alternative, rather nicer interface for `decomoposeFun` would use a [pattern synonym](pattern-synonyms) instead of continuation-passing style. Here is the signature for the pattern synonym:
|
|
|
|
|
|
|
|
|
```
|
|
|
patternTRFun:: fun ~(arg -> res)=>TTypeRep arg
|
|
|
->TTypeRep res
|
|
|
->TTypeRep fun
|
|
|
pattern TRFun :: fun ~ (arg -> res)
|
|
|
=> TTypeRep arg
|
|
|
-> TTypeRep res
|
|
|
-> TTypeRep fun
|
|
|
```
|
|
|
|
|
|
|
|
|
which looks (by design) very like the signature for a GADT data constructor. Now we can use `TRFun` in a pattern, thus:
|
|
|
|
|
|
|
|
|
```
|
|
|
dynApply::Dynamic->Dynamic->MaybeDynamicdynApply(Dyn(TRFun ta tr) f)(Dyn tx x)=case eqTT ta tx ofNothing->NothingJustRefl->Just(Dyn tr (f x))dynApply__=Nothing
|
|
|
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
|
|
|
dynApply (Dyn (TRFun ta tr) f) (Dyn tx x)
|
|
|
= case eqTT ta tx of
|
|
|
Nothing -> Nothing
|
|
|
Just Refl -> Just (Dyn tr (f x))
|
|
|
dynApply _ _ = Nothing
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -266,18 +323,21 @@ Is that not beautiful? The second equation for `dynApply` is needed in case the |
|
|
Suppose we have a `TTypeRep (a :: k)`. It might be nice to get a `TTypeRep (k :: *)`
|
|
|
out of it. (Here, we assume `* :: *`, but the idea actually works without that assumption.) An example is an attempt to typecheck the *expression*
|
|
|
|
|
|
|
|
|
```
|
|
|
typeOf::Typeable(a :: k)=>Proxy a ->TypeRep
|
|
|
typeOf :: Typeable (a :: k) => Proxy a -> TypeRep
|
|
|
```
|
|
|
|
|
|
|
|
|
where `typeOf :: Typeable a => a -> TypeRep` is a long-standing part of the `Typeable` API. To typecheck that expression, we need a `Typeable (Proxy a)` dictionary. Of course, to build such a thing, we need `Typeable k`, which we have no way of getting.
|
|
|
|
|
|
|
|
|
|
|
|
So, we now include
|
|
|
|
|
|
|
|
|
```
|
|
|
kindRep::TTypeRep(a :: k)->TTypeRep k
|
|
|
kindRep :: TTypeRep (a :: k) -> TTypeRep k
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -291,78 +351,106 @@ in the API. I (Richard) conjecture that this is all possible without kind equali |
|
|
It is all very well being able to decompose functions, but what about decomposing other types, like `Maybe Int`?
|
|
|
|
|
|
|
|
|
|
|
|
To do this it is natural to regard types as built from type constructors and binary application, like this:
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTTypeRep(a :: k)::*whereTRApp::TTypeRep a ->TTypeRep b ->TTypeRep(a b)TRCon::TTyCon a ->TTypeRep a
|
|
|
data TTypeRep (a :: k) :: * where
|
|
|
TRApp :: TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
TRCon :: TTyCon a -> TTypeRep a
|
|
|
|
|
|
-- TTyCon must be polykinded, so that we can have-- (TTyCon Maybe), (TTyCon Either), (TTyCon Int) etc-- TTyCon :: forall k. k -> *
|
|
|
-- TTyCon must be polykinded, so that we can have
|
|
|
-- (TTyCon Maybe), (TTyCon Either), (TTyCon Int) etc
|
|
|
-- TTyCon :: forall k. k -> *
|
|
|
```
|
|
|
|
|
|
|
|
|
(We could, and ultimately should, use pattern synonyms again, but it's more concrete to use a GADT for now. Perhaps surprisingly, it is actually fine to expose `TTypeRep` concretely, with its constructors; we can't construct ill-formed `TTypeRep`s.)
|
|
|
|
|
|
|
|
|
|
|
|
While this GADT is expressible in GHC now (note the existential kind in TRApp), **it is not very useful without kind equalities**. (GHC does not currently support kind equalities, but Richard Eisenberg is working that very question.) Why? Here is the type of `TRApp` in its full glory, with normally-invisible kind args in angle brackets:
|
|
|
|
|
|
|
|
|
```
|
|
|
TRApp:: forall k1 k2. forall (a :: k1 -> k2)(b :: k1).TTypeRep<k1->k2> a ->TTypeRep<k1> b ->TTypeRep<k2>(a b)
|
|
|
TRApp :: forall k1 k2. forall (a :: k1 -> k2) (b :: k1).
|
|
|
TTypeRep <k1->k2> a -> TTypeRep <k1> b -> TTypeRep <k2> (a b)
|
|
|
```
|
|
|
|
|
|
|
|
|
Or, to be really explicit about the existentials:
|
|
|
|
|
|
|
|
|
```
|
|
|
TRApp:: forall k2 (c:k2).-- Universal
|
|
|
forall k1 (a :: k1 -> k2)(b :: k1).-- Existential(c ~ a b)=>TTypeRep<k1->k2> a
|
|
|
->TTypeRep<k2> b
|
|
|
->TTypeRep<k2> c
|
|
|
TRApp :: forall k2 (c:k2). -- Universal
|
|
|
forall k1 (a :: k1 -> k2) (b :: k1). -- Existential
|
|
|
(c ~ a b)
|
|
|
=> TTypeRep <k1->k2> a
|
|
|
-> TTypeRep <k2> b
|
|
|
-> TTypeRep <k2> c
|
|
|
```
|
|
|
|
|
|
|
|
|
Now suppose we want to implement `decomposeFun`. We should be able to do this outside the TCB, i.e. without `unsafeCoerce`:
|
|
|
|
|
|
|
|
|
```
|
|
|
arrowCon::TTyCon(->)-- The type rep for (->)decomposeFun::TTypeRep fun
|
|
|
arrowCon :: TTyCon (->) -- The type rep for (->)
|
|
|
|
|
|
decomposeFun :: TTypeRep fun
|
|
|
-> r
|
|
|
-> (forall arg res. (fun ~ (arg->res))
|
|
|
=> TypeRep arg -> TTypeRep res -> r)
|
|
|
-> r
|
|
|
->(forall arg res.(fun ~(arg->res))=>TypeRep arg ->TTypeRep res -> r)-> r
|
|
|
decomposeFun tr def kont
|
|
|
=case tr ofTRApp(TRApp(TRCon c) r1) r2 ->case eqTyCon arrowCon c ofJustHRefl-> kont r1 r2
|
|
|
Nothing-> def
|
|
|
_->default
|
|
|
= case tr of
|
|
|
TRApp (TRApp (TRCon c) r1) r2 -> case eqTyCon arrowCon c of
|
|
|
Just HRefl -> kont r1 r2
|
|
|
Nothing -> def
|
|
|
_ -> default
|
|
|
```
|
|
|
|
|
|
|
|
|
But look at the arguments of `eqTyCon`:
|
|
|
|
|
|
|
|
|
```
|
|
|
arrowCon ::TTyCon<*->*->*>(->)
|
|
|
c ::TTyCon<k1->k2->*> tc
|
|
|
arrowCon :: TTyCon <*->*->*> (->)
|
|
|
c :: TTyCon <k1->k2->*> tc
|
|
|
```
|
|
|
|
|
|
|
|
|
where `k1` and `k2` are existential kinds bound by the two nested `TRApp` constructors, and `tc` the existential bound by the inner `TRApp`. But `kont` is expecting `arg` and `res` to have kind `*`! So we need proofs that `k1 ~ *` and `k2 ~ *`.
|
|
|
|
|
|
|
|
|
|
|
|
The real work is done by `eqTyCon`:
|
|
|
|
|
|
|
|
|
```
|
|
|
eqTyCon:: forall (k1 k2 ::*).
|
|
|
forall (a :: k1)(b :: k2).TTyCon<k1> a ->TTyCon<k2> b ->Maybe(a :~~: b)
|
|
|
eqTyCon :: forall (k1 k2 :: *).
|
|
|
forall (a :: k1) (b :: k2).
|
|
|
TTyCon <k1> a -> TTyCon <k2> b -> Maybe (a :~~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
where `:~~:` is a *kind-heterogeneous* version of `:~:`:
|
|
|
|
|
|
|
|
|
```
|
|
|
data(a::k1):~~:(b::k2)whereHRefl:: forall (a::k). a :~~: a
|
|
|
data (a::k1) :~~: (b::k2) where
|
|
|
HRefl :: forall (a::k). a :~~: a
|
|
|
```
|
|
|
|
|
|
|
|
|
Or, to write the type of `HRefl` with its constraints explicit:
|
|
|
|
|
|
|
|
|
```
|
|
|
HRefl:: forall k1 k2. forall (a::k1)(b::k2).(k1 ~ k2, a ~ b)=> a :~~: b
|
|
|
HRefl :: forall k1 k2. forall (a::k1) (b::k2).
|
|
|
(k1 ~ k2, a ~ b)
|
|
|
=> a :~~: b
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -386,19 +474,27 @@ Conclusion: make `TypeRep` abstract. But then how can we pattern-match on it? |
|
|
### Trusted computing base
|
|
|
|
|
|
|
|
|
|
|
|
With all of this, what is left in the TCB? The `TTyCon` type is a new abstract type, and the comparison (based on fingerprints) must be in the TCB.
|
|
|
|
|
|
|
|
|
```
|
|
|
TTyCon a --- abstract typeeqTyCon:: forall k1 k2. forall (a :: k1)(b :: k2).TTyCon a ->TTyCon b ->Maybe(a :~~: b)tyConKind::TTyCon(a :: k)->TTypeRep(k ::*)
|
|
|
TTyCon a --- abstract type
|
|
|
eqTyCon :: forall k1 k2. forall (a :: k1) (b :: k2).
|
|
|
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
|
|
|
tyConKind :: TTyCon (a :: k) -> TTypeRep (k :: *)
|
|
|
```
|
|
|
|
|
|
|
|
|
Note that `TTyCon` represents type constructors already applied to any kind arguments. Even with kind equalities, we have no way of creating a representation for `Proxy :: forall k. k -> *`, as that would require an impredicative kind for the implicit kind argument to `TTyCon`.
|
|
|
|
|
|
|
|
|
|
|
|
`withTypeable` could be written in core (and perhaps could be generalized to other constraints) but not in source Haskell:
|
|
|
|
|
|
|
|
|
```
|
|
|
withTypeable::TypeRep a ->(Typeable a => b)-> b
|
|
|
withTypeable :: TypeRep a -> (Typeable a => b) -> b
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -423,34 +519,81 @@ implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the |
|
|
## Proposed API
|
|
|
|
|
|
|
|
|
|
|
|
This version assumes homoegeneous equality (as GHC is today, July 2, 2015). Below is the version with heterogeneous equality.
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTTypeRep(a :: k)-- abstractdataTTyCon(a :: k)-- abstract-- CostructorstrCon:: forall k (a :: k).TTyCon a ->TTypeRep a -- in TCBtrApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- in TCB-- DestructorspatterntypeTRCon:: forall k (a :: k).TyCon a ->TTypeRep a
|
|
|
patterntypeTRApp:: forall k. exists k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)patterntypeTRFun::TTypeRep arg
|
|
|
->TTypeRep res
|
|
|
->TypeRep(TTypeRep(arg->res))-- For now, homogeneous equalitieseqTyCon:: forall k (a :: k)(b :: k).TTyCon a ->TTyCon b ->Maybe(a :~: b)eqTT:: forall k (a :: k)(b :: k).TTypeRep a ->TTypeRep b ->Maybe(a :~: b)
|
|
|
data TTypeRep (a :: k) -- abstract
|
|
|
data TTyCon (a :: k) -- abstract
|
|
|
|
|
|
-- Costructors
|
|
|
trCon :: forall k (a :: k). TTyCon a -> TTypeRep a -- in TCB
|
|
|
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
|
|
|
TTypeRep a -> TTypeRep b -> TTypeRep (a b) -- in TCB
|
|
|
|
|
|
-- Destructors
|
|
|
pattern type TRCon :: forall k (a :: k). TyCon a -> TTypeRep a
|
|
|
pattern type TRApp :: forall k. exists k1 (a :: k1 -> k) (b :: k1).
|
|
|
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
pattern type TRFun :: TTypeRep arg
|
|
|
-> TTypeRep res
|
|
|
-> TypeRep (TTypeRep (arg->res))
|
|
|
|
|
|
|
|
|
-- For now, homogeneous equalities
|
|
|
eqTyCon :: forall k (a :: k) (b :: k).
|
|
|
TTyCon a -> TTyCon b -> Maybe (a :~: b)
|
|
|
eqTT :: forall k (a :: k) (b :: k).
|
|
|
TTypeRep a ->T TypeRep b -> Maybe (a :~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
This assumes heterogeneous equality (that is, with kind equalities).
|
|
|
|
|
|
|
|
|
```
|
|
|
dataTTypeRep(a :: k)-- abstractdataTTyCon(a :: k)-- abstracttyConKind:: forall k (a :: k).TTyCon a ->TTypeRep k
|
|
|
data TTypeRep (a :: k) -- abstract
|
|
|
data TTyCon (a :: k) -- abstract
|
|
|
|
|
|
tyConKind :: forall k (a :: k). TTyCon a -> TTypeRep k
|
|
|
|
|
|
-- Costructors
|
|
|
trCon :: forall k (a :: k). TTyCon a -> TTypeRep a
|
|
|
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
|
|
|
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
|
|
|
-- CostructorstrCon:: forall k (a :: k).TTyCon a ->TTypeRep a
|
|
|
trApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- DestructorspatterntypeTRCon:: forall k (a :: k).TyCon a ->TTypeRep a
|
|
|
patterntypeTRApp:: forall k. exists k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)-- this definition to go into Data.Type.Equalitydata(a :: k1):~~:(b :: k2)whereHRefl:: a :~~: a
|
|
|
-- Destructors
|
|
|
pattern type TRCon :: forall k (a :: k). TyCon a -> TTypeRep a
|
|
|
pattern type TRApp :: forall k. exists k1 (a :: k1 -> k) (b :: k1).
|
|
|
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
|
|
|
eqTyCon:: forall k1 k2 (a :: k1)(b :: k2).TTyCon a ->TTyCon b ->Maybe(a :~~: b)-- the following definitions can be defined on top of the interface-- above, but would be included for conveniencepatterntypeTRFun::TTypeRep arg ->TTypeRep res
|
|
|
->TTypeRep(arg -> res)eqTT:: forall k1 k2 (a :: k1)(b :: k2).TTypeRep a ->TTypeRep b ->Maybe(a :~~: b)typeRepKind:: forall k (a :: k).TTypeRep a ->TTypeRep k
|
|
|
-- this definition to go into Data.Type.Equality
|
|
|
data (a :: k1) :~~: (b :: k2) where
|
|
|
HRefl :: a :~~: a
|
|
|
|
|
|
class forall k (a :: k).Typeable k =>Typeable a where
|
|
|
tTypeRep ::TTypeRep a
|
|
|
eqTyCon :: forall k1 k2 (a :: k1) (b :: k2).
|
|
|
TTyCon a -> TTyCon b -> Maybe (a :~~: b)
|
|
|
|
|
|
-- the following definitions can be defined on top of the interface
|
|
|
-- above, but would be included for convenience
|
|
|
pattern type TRFun :: TTypeRep arg -> TTypeRep res
|
|
|
-> TTypeRep (arg -> res)
|
|
|
|
|
|
eqTT :: forall k1 k2 (a :: k1) (b :: k2).
|
|
|
TTypeRep a -> TTypeRep b -> Maybe (a :~~: b)
|
|
|
|
|
|
typeRepKind :: forall k (a :: k). TTypeRep a -> TTypeRep k
|
|
|
|
|
|
class forall k (a :: k). Typeable k => Typeable a where
|
|
|
tTypeRep :: TTypeRep a
|
|
|
```
|
|
|
|
|
|
|
|
|
**SLPJ**: Do we need both `:~:` and `:~~:`?
|
|
|
|
|
|
|
|
|
|
|
|
**RAE**: I don't think it's strictly necessary, but keeping the distinction might be useful. `:~:` will unify the kinds of its arguments during type inference, and that might be what the programmer wants. I don't feel strongly here.
|
|
|
|
|
|
|
... | ... | @@ -474,36 +617,42 @@ The class declaration for `Typeable` is highly suspect, as it is manifestly cycl |
|
|
As painfully demonstrated (painful in the conclusion, not the demonstration!) in [comment:16:ticket:9858](https://gitlab.haskell.org//ghc/ghc/issues/9858), `Typeable` can now (7.10.1 RC1) be abused to write `unsafeCoerce`. The problem is that today's `TypeRep`s ignore kind parameters.
|
|
|
|
|
|
|
|
|
|
|
|
Drawing this out somewhat: we allow only `Typeable` instances for unapplied constructors. That is, we have
|
|
|
|
|
|
|
|
|
```
|
|
|
derivinginstanceTypeableMaybe
|
|
|
deriving instance Typeable Maybe
|
|
|
```
|
|
|
|
|
|
|
|
|
never
|
|
|
|
|
|
|
|
|
```
|
|
|
derivinginstanceTypeable(MaybeInt)
|
|
|
deriving instance Typeable (Maybe Int)
|
|
|
```
|
|
|
|
|
|
|
|
|
However, what if we have
|
|
|
|
|
|
|
|
|
```
|
|
|
dataPK(a :: k)
|
|
|
data PK (a :: k)
|
|
|
```
|
|
|
|
|
|
|
|
|
? `PK` properly has *two* parameters: the kind `k` and the type `a :: k`. However, whenever we write `PK` in source code, the `k` parameter is implicitly provided. Thus,
|
|
|
when we write
|
|
|
|
|
|
|
|
|
```
|
|
|
derivinginstanceTypeablePK
|
|
|
deriving instance Typeable PK
|
|
|
```
|
|
|
|
|
|
|
|
|
we actually supply a kind parameter `k0`. GHC tries to find a value for `k0`, fails, and leaves it as a skolem variable. We get an instance `forall k. Typeable (PK k)`. But, of course, `PK *` and `PK (* -> *)` should have *different*`TypeRep`s. Disaster!
|
|
|
we actually supply a kind parameter `k0`. GHC tries to find a value for `k0`, fails, and leaves it as a skolem variable. We get an instance `forall k. Typeable (PK k)`. But, of course, `PK *` and `PK (* -> *)` should have *different* `TypeRep`s. Disaster!
|
|
|
|
|
|
|
|
|
### A stop-gap solution
|
|
|
|
... | ... | @@ -515,10 +664,13 @@ we actually supply a kind parameter `k0`. GHC tries to find a value for `k0`, fa |
|
|
The "obvious" answer -- don't supply the `k` here -- doesn't work. The instance for `PK` would become `Typeable <forall k. k -> *> PK`, where a normally-implicit kind parameter is supplied in angle brackets. This is an **impredicative kind**, certainly beyond GHC's type system's abilities at the moment, especially in a type-class argument.
|
|
|
|
|
|
|
|
|
|
|
|
One (somewhat unpleasant) way forward is to allow kind parameters to be supplied in `Typeable` instances, but still restrict type parameters. So, we would have
|
|
|
|
|
|
|
|
|
```
|
|
|
derivinginstanceTypeable(PK::*->*)derivinginstanceTypeable(PK::(*->*)->*)
|
|
|
deriving instance Typeable (PK :: * -> *)
|
|
|
deriving instance Typeable (PK :: (* -> *) -> *)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -550,25 +702,33 @@ Some drawbacks: |
|
|
### Long-term solution
|
|
|
|
|
|
|
|
|
|
|
|
We actually don't have a good long-term solution available. We thought that `* :: *` and kind equalities would fix this, but they don't. To see why, let's examine the type of `trApp`:
|
|
|
|
|
|
|
|
|
```
|
|
|
trApp:: forall k k1 (a :: k1 -> k)(b :: k1).TTypeRep a ->TTypeRep b ->TTypeRep(a b)
|
|
|
trApp :: forall k k1 (a :: k1 -> k) (b :: k1).
|
|
|
TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
```
|
|
|
|
|
|
|
|
|
In the `* :: *` world, it would be reasonable to have `TTypeRep`s for kinds, assuming we have `TTypeRep`s always take explicit kind parameters. So, we might imagine having a `TTypeRep` for `PK` (call it `pkRep`) and a `TTypeRep` for `Bool` (call it `boolRep`). Does `pkRep `trApp` boolRep`` type-check? Unfortunately, no. We have
|
|
|
|
|
|
|
|
|
```
|
|
|
pkRep::TTypeRep<forall k. k ->*>PKboolRep::TTypeRep<*>Bool
|
|
|
pkRep :: TTypeRep <forall k. k -> *> PK
|
|
|
boolRep :: TTypeRep <*> Bool
|
|
|
```
|
|
|
|
|
|
|
|
|
but `trApp` says that `a` must have type `k1 -> k` for some `k1` and `k`. Here `PK` would be the value for `a`, but `PK`'s kind is `forall k. k -> *`, which doesn't fit `k1 -> k` at all! We would need to generalize `trApp` to
|
|
|
|
|
|
|
|
|
```
|
|
|
trApp2:: forall (k1 ::*)(k :: k1 ->*)(a :: pi (b :: k1). k b)(b :: k1).TTypeRep<pi (b :: k1). k b> a ->TTypeRep<k1> b
|
|
|
->TTypeRep<k b>(a b)
|
|
|
trApp2 :: forall (k1 :: *) (k :: k1 -> *)
|
|
|
(a :: pi (b :: k1). k b) (b :: k1).
|
|
|
TTypeRep <pi (b :: k1). k b> a -> TTypeRep <k1> b
|
|
|
-> TTypeRep <k b> (a b)
|
|
|
```
|
|
|
|
|
|
|
... | ... | |