Language.Typ
Contents
- Quantifying over the TSYM interpreter
- Show Typ-able expressions
- No Show type class constraint!
- Type representation
- Compare with Dyta.Typeable.TypeRep
- Alternative to quantification: copying
- Equality and safe type cast
- c is NOT necessarily a functor or injective!
- Leibniz equality is reflexive, symmetric and transitive
- An Unusual
functor - Decide if (trepr a) represents a type that is equal to some type b
- A constructive
deconstructor - Another constructive
deconstructor - Cf. Data.Typeable.gcast
- Our own version of Data.Dynamic
Description
- Type representation, equality and the safe typecast: * the above-the-board version of Data.Typeable
- class TSYM trepr where
- newtype ShowT a = ShowT String
- view_t :: ShowT a -> String
- newtype TQ t = TQ {}
- show_as :: TQ a -> a -> String
- data ShowAs a = ShowAs (TQ a) (a -> String)
- data Typ = forall t . Typ (TQ t)
- data TCOPY trep1 trep2 a = TCOPY (trep1 a) (trep2 a)
- newtype EQU a b = EQU {
- equ_cast :: forall c. c a -> c b
- refl :: EQU a a
- tran :: EQU a u -> EQU u b -> EQU a b
- newtype FS b a = FS {}
- symm :: EQU a b -> EQU b a
- newtype F1 t b a = F1 {}
- newtype F2 t a b = F2 {}
- eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1 -> b1) (a2 -> b2)
- data AsInt a = AsInt (Maybe (EQU a Int))
- as_int :: AsInt a -> c a -> Maybe (c Int)
- data AsArrow a = forall b1 b2 . AsArrow (TQ a) (Maybe (TQ b1, TQ b2, EQU a (b1 -> b2)))
- as_arrow :: AsArrow a -> AsArrow a
- newtype SafeCast a = SafeCast (forall b. TQ b -> Maybe (EQU a b))
- safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)
- data Dynamic = forall t . Dynamic (TQ t) t
- newtype Id a = Id a
Documentation
- The language of type representations: first-order and typed It is quite like the language of intnegadd we have seen before, but it is now typed. It is first order: the language of simple types is first order
- The view interpreter The first interpreter is to view the types
Quantifying over the TSYM interpreter
Show Typ-able expressions
No Show type class constraint!
The implementation of the interpreter ShowAs shows off the technique of accumulating new TQ as we traverse the old one. We shall see more examples later. One is again reminded of attribute grammars.
Type representation
Compare with Dyta.Typeable.TypeRep
Alternative to quantification: copying
Equality and safe type cast
c is NOT necessarily a functor or injective!
Leibniz equality is reflexive, symmetric and transitive
An Unusual functor
Decide if (trepr a) represents a type that is equal to some type b
A constructive deconstructor
Another constructive deconstructor
Cf. Data.Typeable.gcast
safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)Source