liboleg-2010.1.5: An evolving collection of Oleg Kiselyov's Haskell modules

Language.Typ

Contents

Description

  • Type representation, equality and the safe typecast: * the above-the-board version of Data.Typeable

Synopsis

Documentation

class TSYM trepr whereSource

  • 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

Methods

tint :: trepr IntSource

tarr :: trepr a -> trepr b -> trepr (a -> b)Source

Instances

TSYM SafeCast 
TSYM AsArrow 
TSYM AsInt 
TSYM ShowAs 
TSYM TQ

TQ is itself an interpreter, the trivial one

TSYM ShowT 
(TSYM trep1, TSYM trep2) => TSYM (TCOPY trep1 trep2) 

newtype ShowT a Source

  • The view interpreter The first interpreter is to view the types

Constructors

ShowT String 

Instances

Quantifying over the TSYM interpreter

newtype TQ t Source

Constructors

TQ 

Fields

unTQ :: forall trepr. TSYM trepr => trepr t
 

Instances

TSYM TQ

TQ is itself an interpreter, the trivial one

Show Typ-able expressions

No Show type class constraint!

show_as :: TQ a -> a -> StringSource

data ShowAs a Source

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.

Constructors

ShowAs (TQ a) (a -> String) 

Instances

Type representation

Compare with Dyta.Typeable.TypeRep

data Typ Source

Constructors

forall t . Typ (TQ t) 

Alternative to quantification: copying

data TCOPY trep1 trep2 a Source

Constructors

TCOPY (trep1 a) (trep2 a) 

Instances

(TSYM trep1, TSYM trep2) => TSYM (TCOPY trep1 trep2) 

Equality and safe type cast

c is NOT necessarily a functor or injective!

newtype EQU a b Source

Constructors

EQU 

Fields

equ_cast :: forall c. c a -> c b
 

Leibniz equality is reflexive, symmetric and transitive

An Unusual functor

tran :: EQU a u -> EQU u b -> EQU a bSource

newtype FS b a Source

Constructors

FS 

Fields

unFS :: EQU a b
 

symm :: EQU a b -> EQU b aSource

newtype F1 t b a Source

Constructors

F1 

Fields

unF1 :: EQU t (a -> b)
 

newtype F2 t a b Source

Constructors

F2 

Fields

unF2 :: EQU t (a -> b)
 

eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1 -> b1) (a2 -> b2)Source

Decide if (trepr a) represents a type that is equal to some type b

A constructive deconstructor

data AsInt a Source

Constructors

AsInt (Maybe (EQU a Int)) 

Instances

as_int :: AsInt a -> c a -> Maybe (c Int)Source

Another constructive deconstructor

data AsArrow a Source

Constructors

forall b1 b2 . AsArrow (TQ a) (Maybe (TQ b1, TQ b2, EQU a (b1 -> b2))) 

Instances

newtype SafeCast a Source

Constructors

SafeCast (forall b. TQ b -> Maybe (EQU a b)) 

Instances

Cf. Data.Typeable.gcast

safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)Source

Our own version of Data.Dynamic

data Dynamic Source

Constructors

forall t . Dynamic (TQ t) t 

newtype Id a Source

Constructors

Id a