... | @@ -24,7 +24,7 @@ Note `eqTyConT` is not hugely useful as (if it returns True) we know that types |
... | @@ -24,7 +24,7 @@ Note `eqTyConT` is not hugely useful as (if it returns True) we know that types |
|
```
|
|
```
|
|
dataTypeRetT(a::k)--abstractclassTypeable(a :: k)where
|
|
dataTypeRetT(a::k)--abstractclassTypeable(a :: k)where
|
|
typeRepT ::TypeRepT a
|
|
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 neededdataGetFn(a ::*)where-- must have a :: * as GF cannot be GADT-like in its *kind* argumentsGF::TypeRepT a ->TypeRepT b ->GetFn(a -> b)getFn::TypeRepT(a ::*)->Maybe(GetFn a)-- this needs unsafeCoerce-- compiler support for generating (e.g.)instanceTypeableBoolinstanceTypeable(->)
|
|
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(->)
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
... | | ... | |