... | ... | @@ -13,7 +13,7 @@ The TCB consists of `TyConT` and `Typeable` in the homogenous case, and just `Ty |
|
|
`TyConT`:
|
|
|
|
|
|
```
|
|
|
dataTyConT(a::k)-- abstracteqTyConT::TyConT(a :: k1)->TyConT(b :: k2)->BooleqTyConTHom::TyConT(a :: k)->TyConT(b :: k)->(a :~: b)-- this needs unsafeCoerce-- compiler support for generating (e.g.)tyConTBool::TyConTBooltyConTArr::TyConT(->)
|
|
|
dataTyConT(a::k)-- abstracteqTyConT::TyConT(a :: k1)->TyConT(b :: k2)->BooleqTyConTHom::TyConT(a :: k)->TyConT(b :: k)->Maybe(a :~: b)-- eqTyConTHom needs unsafeCoerce its implementation-- compiler support for generating (e.g.)tyConTBool::TyConTBooltyConTArr::TyConT(->)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -22,9 +22,14 @@ Note `eqTyConT` is not hugely useful as (if it returns True) we know that types |
|
|
`Typeable`:
|
|
|
|
|
|
```
|
|
|
dataTypeRetT(a::k)--abstractclassTypeable(a :: k)where
|
|
|
dataTypeRepT(a::k)-- Type-indexed type representation; abstractappT::TypeRepT a ->TypeRepT b ->TypeRepT(a b)tyConT::TyConT a ->TypeRepT a
|
|
|
|
|
|
classTypeable(a :: k)where
|
|
|
typeRepT ::TypeRepT a
|
|
|
instance(Typeable c,Typeable a)=>Typeable(c a)typeOf::Typeable a => a ->TypeRepT a -- for convenienceeqTT::TypeRepT(a::k1)->TypeRepT(b::k2)->BooleqTTHom::TypeRepT(a::k)->TypeRepT(b::k)->Maybe(a :~: b)dataGetApp(a::k)whereGA::TypeRepT a ->TypeRepT b ->GetApp(a b)getApp::TypeRepT(a::k)->Maybe(GetApp a)-- no unsafeCoerce neededdataG1 c a whereG1::TypeRepT a ->G1 c (c a)get1::TypeRepT(c :: k1->k)->TypeRepT(a::k)->Maybe(G1 c a)-- uses an unsafeCoercedataG2 c a whereG1::TypeRepT a ->TypeRepT b ->G2 c (c a b)get2::TypeRepT(c :: k2->k1->k)->TypeRepT(a::k)->Maybe(G1 c a)--uses an unsafeCoerce--TODO: how many of these should we provide?getFn::TypeRepT(a ::*)->Maybe(G2(->) a)-- convenience, specialise get2, don't need unsafeCoerce-- compiler support for generating (e.g.)instanceTypeableBoolinstanceTypeable(->)
|
|
|
|
|
|
withTypeRepT::TypeRepT a ->(Typeable a => b)-> b
|
|
|
-- c.f. Trac #2439typeOf::Typeable a => a ->TypeRepT a -- for convenienceeqTT::TypeRepT(a::k1)->TypeRepT(b::k2)->BooleqTTHom::TypeRepT(a::k)->TypeRepT(b::k)->Maybe(a :~: b)dataGetApp(a::k)whereGA::TypeRepT a ->TypeRepT b ->GetApp(a b)getAppT::TypeRepT(a::k)->Maybe(GetApp a)-- no unsafeCoerce neededdataG1 c a whereG1::TypeRepT a ->G1 c (c a)getT1::TypeRepT(c :: k1->k)->TypeRepT(a::k)->Maybe(G1 c a)-- Implementation uses an unsafeCoercedataG2 c a whereG2::TypeRepT a ->TypeRepT b ->G2 c (c a b)getT2::TypeRepT(c :: k2->k1->k)->TypeRepT(a::k)->Maybe(G1 c a)-- Implementation uses an unsafeCoerce--TODO: how many of these should we provide?getFnT::TypeRepT(a ::*)->Maybe(G2(->) a
|
|
|
getFnT= getT2 (tyConT tyConTFun)-- convenience, specialise get2, don't need unsafeCoerce-- GHC has magic built-in support for Typeable instances-- but the effect is similar to declarations like these:instance(Typeable c,Typeable a)=>Typeable(c a)instanceTypeableBoolinstanceTypeable(->)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -33,7 +38,8 @@ Similar notes to `eqTyConT` apply to `eqTT`. |
|
|
`Dynamic`
|
|
|
|
|
|
```
|
|
|
dataDynamicwhereDyn::TypeRepT a -> a ->DynamicmkDyn::Typeable a => a ->Dynamic-- for conveniencedynApply::Dynamic->Dynamic->MaybeDynamic-- type-safely apply a dynamic function to a dynamic argument
|
|
|
dataDynamicwhereDyn::TypeRepT a -> a ->DynamicmkDyn::Typeable a => a ->Dynamic-- for conveniencedynApply::Dynamic->Dynamic->MaybeDynamic-- type-safely apply a dynamic function to a dynamic argumentgetDynamic::TypeRepT a
|
|
|
->Dynamic-- ^ the dynamically-typed object->Maybe a -- ^ returns: @'Just' a@, if the dynamically-typed-- object has the correct type (and @a@ is its value), -- or 'Nothing' otherwise.
|
|
|
```
|
|
|
|
|
|
## Hetrogenous Case
|
... | ... | |