... | ... | @@ -17,22 +17,21 @@ See also |
|
|
|
|
|
Consider `Dynamic`:
|
|
|
|
|
|
```wiki
|
|
|
data Dynamic where
|
|
|
Dyn :: TypeRep -> a -> Dynamic
|
|
|
```
|
|
|
dataDynamicwhereDyn::TypeRep-> a ->Dynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
We'd like to write `dynApply`:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
dynApply::Dynamic->Dynamic->MaybeDynamic
|
|
|
```
|
|
|
|
|
|
|
|
|
which succeeds only when the application is type correct. But how? Let's try
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
dynApply(Dyn tf f)(Dyn tx x)=???
|
|
|
```
|
|
|
|
... | ... | @@ -42,10 +41,8 @@ We need some way to decompose `tf` (the type representation for `f`), ask if it |
|
|
|
|
|
But at the moment we don't have any *type-safe* way to decompose `TypeRep`. Indeed `dynApply` is defined like this right now:
|
|
|
|
|
|
```wiki
|
|
|
dynApply (Dyn tf f) (Dyn tx x)
|
|
|
= case funResultTy tf tx of
|
|
|
Just tr -> Just (Dyn tr (unsafeCoerce f x))
|
|
|
```
|
|
|
dynApply(Dyn tf f)(Dyn tx x)=case funResultTy tf tx ofJust tr ->Just(Dyn tr (unsafeCoerce f x))
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -64,9 +61,8 @@ So **our main goal is to be able to write `dynApply` in a type-safe way** so tha |
|
|
|
|
|
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:
|
|
|
|
|
|
```wiki
|
|
|
data Dynamic where
|
|
|
Dyn :: TTypeRep a -> a -> Dynamic
|
|
|
```
|
|
|
dataDynamicwhereDyn::TTypeRep a -> a ->Dynamic
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -75,16 +71,9 @@ Here we are using a *type-indexed* type representation, `TTypeRep`. Now the con |
|
|
|
|
|
We can re-define the `Typeable` class and `TypeRep` thus:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
classTypeable 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)
|
|
|
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)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -97,7 +86,7 @@ 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:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
withTypeable::TTypeRep a ->(Typeable a => b)-> b
|
|
|
```
|
|
|
|
... | ... | @@ -107,12 +96,8 @@ withTypeable :: TTypeRep a -> (Typeable a => b) -> b |
|
|
|
|
|
We can also compare two `TTypeReps` to give a statically-usable proof of equality:
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
```
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -125,15 +110,11 @@ data a :~: b where -- Defined in Data.Typeable.Equality |
|
|
|
|
|
If we want to decompose `TTypable`, at least in the function arrow case, we need a function like this:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
decomposeFun::TTypeRep fun
|
|
|
-> 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'
|
|
|
->(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'
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -142,20 +123,14 @@ This function is part of `Typeable`, and replaces `funResultTy`. |
|
|
|
|
|
Now we can write `dynApply`, in a completely type-safe way, outside the TCB:
|
|
|
|
|
|
```wiki
|
|
|
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))
|
|
|
```
|
|
|
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))
|
|
|
```
|
|
|
|
|
|
**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:
|
|
|
|
|
|
```wiki
|
|
|
pattern TRFun :: fun ~ (arg -> res)
|
|
|
=> TTypeRep arg
|
|
|
```
|
|
|
patternTRFun:: fun ~(arg -> res)=>TTypeRep arg
|
|
|
->TTypeRep res
|
|
|
->TTypeRep fun
|
|
|
```
|
... | ... | @@ -163,13 +138,8 @@ pattern TRFun :: fun ~ (arg -> res) |
|
|
|
|
|
which looks (by design) very like the signature for a GADT data constructor. Now we can use `TRFun` in a pattern, thus:
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
```
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -183,7 +153,7 @@ 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*
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
typeOf::Typeable(a :: k)=>Proxy a ->TypeRep
|
|
|
```
|
|
|
|
... | ... | @@ -193,7 +163,7 @@ where `typeOf :: Typeable a => a -> TypeRep` is a long-standing part of the `Typ |
|
|
|
|
|
So, we now include
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
kindRep::TTypeRep(a :: k)->TTypeRep k
|
|
|
```
|
|
|
|
... | ... | @@ -210,14 +180,10 @@ It is all very well being able to decompose functions, but what about decomposin |
|
|
|
|
|
To do this it is natural to regard types as built from type constructors and binary application, like this:
|
|
|
|
|
|
```wiki
|
|
|
data TTypeRep (a :: k) :: * where
|
|
|
TRApp :: TTypeRep a -> TTypeRep b -> TTypeRep (a b)
|
|
|
TRCon :: TTyCon a -> TTypeRep a
|
|
|
```
|
|
|
dataTTypeRep(a :: k)::*whereTRApp::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 -> *
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -226,19 +192,16 @@ data TTypeRep (a :: k) :: * where |
|
|
|
|
|
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:
|
|
|
|
|
|
```wiki
|
|
|
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:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
TRApp:: forall k2 (c:k2).-- Universal
|
|
|
forall k1 (a :: k1 -> k2) (b :: k1). -- Existential
|
|
|
(c ~ a b)
|
|
|
=> TTypeRep <k1->k2> a
|
|
|
forall k1 (a :: k1 -> k2)(b :: k1).-- Existential(c ~ a b)=>TTypeRep<k1->k2> a
|
|
|
->TTypeRep<k2> b
|
|
|
->TTypeRep<k2> c
|
|
|
```
|
... | ... | @@ -246,18 +209,12 @@ TRApp :: forall k2 (c:k2). -- Universal |
|
|
|
|
|
Now suppose we want to implement `decomposeFun`. We should be able to do this outside the TCB, i.e. without `unsafeCoerce`:
|
|
|
|
|
|
```wiki
|
|
|
arrowCon :: TTyCon (->) -- The type rep for (->)
|
|
|
|
|
|
decomposeFun :: TTypeRep fun
|
|
|
-> r
|
|
|
-> (forall arg res. (fun ~ (arg->res))
|
|
|
=> TypeRep arg -> TTypeRep res -> r)
|
|
|
```
|
|
|
arrowCon::TTyCon(->)-- The type rep for (->)decomposeFun::TTypeRep fun
|
|
|
-> r
|
|
|
->(forall arg res.(fun ~(arg->res))=>TypeRep arg ->TTypeRep res -> r)-> r
|
|
|
decomposeFun tr def kont
|
|
|
= case tr of
|
|
|
TRApp (TRApp (TRCon c) r1) r2 -> case eqTyCon arrowCon c of
|
|
|
Just HRefl -> kont r1 r2
|
|
|
=case tr ofTRApp(TRApp(TRCon c) r1) r2 ->case eqTyCon arrowCon c ofJustHRefl-> kont r1 r2
|
|
|
Nothing-> def
|
|
|
_->default
|
|
|
```
|
... | ... | @@ -265,7 +222,7 @@ decomposeFun tr def kont |
|
|
|
|
|
But look at the arguments of `eqTyCon`:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
arrowCon ::TTyCon<*->*->*>(->)
|
|
|
c ::TTyCon<k1->k2->*> tc
|
|
|
```
|
... | ... | @@ -276,27 +233,23 @@ where `k1` and `k2` are existential kinds bound by the two nested `TRApp` constr |
|
|
|
|
|
The real work is done by `eqTyCon`:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
eqTyCon:: forall (k1 k2 ::*).
|
|
|
forall (a :: k1) (b :: k2).
|
|
|
TTyCon <k1> a -> TTyCon <k2> b -> Maybe (a :~~: b)
|
|
|
forall (a :: k1)(b :: k2).TTyCon<k1> a ->TTyCon<k2> b ->Maybe(a :~~: b)
|
|
|
```
|
|
|
|
|
|
|
|
|
where `:~~:` is a *kind-heterogeneous* version of `:~:`:
|
|
|
|
|
|
```wiki
|
|
|
data (a::k1) :~~: (b::k2) where
|
|
|
HRefl :: forall (a::k). a :~~: a
|
|
|
```
|
|
|
data(a::k1):~~:(b::k2)whereHRefl:: forall (a::k). a :~~: a
|
|
|
```
|
|
|
|
|
|
|
|
|
Or, to write the type of `HRefl` with its constraints explicit:
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -322,11 +275,8 @@ Conclusion: make `TypeRep` abstract. But then how can we pattern-match on it? |
|
|
|
|
|
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.
|
|
|
|
|
|
```wiki
|
|
|
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 :: *)
|
|
|
```
|
|
|
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 ::*)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -334,7 +284,7 @@ Note that `TTyCon` represents type constructors already applied to any kind argu |
|
|
|
|
|
`withTypeable` could be written in core (and perhaps could be generalized to other constraints) but not in source Haskell:
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
withTypeable::TypeRep a ->(Typeable a => b)-> b
|
|
|
```
|
|
|
|
... | ... | @@ -362,66 +312,25 @@ implementation of `decomposeFun` will use `unsafeCoerce` and will be part of the |
|
|
|
|
|
This version assumes homoegeneous equality (as GHC is today, July 2, 2015). Below is the version with heterogeneous equality.
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
```
|
|
|
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 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)
|
|
|
->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)
|
|
|
```
|
|
|
|
|
|
|
|
|
This assumes heterogeneous equality (that is, with kind equalities).
|
|
|
|
|
|
```wiki
|
|
|
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)
|
|
|
|
|
|
-- 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)
|
|
|
|
|
|
-- this definition to go into Data.Type.Equality
|
|
|
data (a :: k1) :~~: (b :: k2) where
|
|
|
HRefl :: a :~~: 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)
|
|
|
```
|
|
|
dataTTypeRep(a :: k)-- abstractdataTTyCon(a :: k)-- abstracttyConKind:: forall k (a :: k).TTyCon a ->TTypeRep k
|
|
|
|
|
|
eqTT :: forall k1 k2 (a :: k1) (b :: k2).
|
|
|
TTypeRep a -> TTypeRep b -> Maybe (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
|
|
|
|
|
|
typeRepKind :: forall k (a :: k). TTypeRep a -> TTypeRep k
|
|
|
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
|
|
|
|
|
|
class forall k (a :: k).Typeable k =>Typeable a where
|
|
|
tTypeRep ::TTypeRep a
|
... | ... | @@ -452,21 +361,21 @@ As painfully demonstrated (painful in the conclusion, not the demonstration!) in |
|
|
|
|
|
Drawing this out somewhat: we allow only `Typeable` instances for unapplied constructors. That is, we have
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
derivinginstanceTypeableMaybe
|
|
|
```
|
|
|
|
|
|
|
|
|
never
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
derivinginstanceTypeable(MaybeInt)
|
|
|
```
|
|
|
|
|
|
|
|
|
However, what if we have
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
dataPK(a :: k)
|
|
|
```
|
|
|
|
... | ... | @@ -474,7 +383,7 @@ 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
|
|
|
|
|
|
```wiki
|
|
|
```
|
|
|
derivinginstanceTypeablePK
|
|
|
```
|
|
|
|
... | ... | @@ -493,9 +402,8 @@ The "obvious" answer -- don't supply the `k` here -- doesn't work. The instance |
|
|
|
|
|
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
|
|
|
|
|
|
```wiki
|
|
|
deriving instance Typeable (PK :: * -> *)
|
|
|
deriving instance Typeable (PK :: (* -> *) -> *)
|
|
|
```
|
|
|
derivinginstanceTypeable(PK::*->*)derivinginstanceTypeable(PK::(*->*)->*)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -529,26 +437,22 @@ Some drawbacks: |
|
|
|
|
|
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`:
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
|
|
|
```wiki
|
|
|
pkRep :: TTypeRep <forall k. k -> *> PK
|
|
|
boolRep :: TTypeRep <*> Bool
|
|
|
```
|
|
|
pkRep::TTypeRep<forall k. k ->*>PKboolRep::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
|
|
|
|
|
|
```wiki
|
|
|
trApp2 :: forall (k1 :: *) (k :: k1 -> *)
|
|
|
(a :: pi (b :: k1). k b) (b :: k1).
|
|
|
TTypeRep <pi (b :: k1). k b> a -> TTypeRep <k1> 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)
|
|
|
```
|
|
|
|
... | ... | |