TTTAS-0.6.0: Typed Transformations of Typed Abstract Syntax

Safe HaskellSafe-Inferred




Library for Typed Transformations of Typed Abstract Syntax.

The library is documented in the paper: Typed Transformations of Typed Abstract Syntax

Bibtex entry:;filename=TTTAS.bib

For more documentation see the TTTAS webpage:


Typed References and Environments

Typed References

data Ref a env where Source

The Ref type for represents typed indices which are labeled with both the type of value to which they refer and the type of the environment (a nested Cartesian product, growing to the right) in which this value lives. The constructor Zero expresses that the first element of the environment has to be of type a. The constructor Suc does not care about the type of the first element in the environment, being polymorphic in the type b.


Zero :: Ref a (env', a) 
Suc :: Ref a env' -> Ref a (env', b) 

data Equal :: * -> * -> * where Source

The Equal type encodes type equality.


Eq :: Equal a a 

match :: Ref a env -> Ref b env -> Maybe (Equal a b) Source

The function match compares two references for equality. If they refer to the same element in the environment the value Just Eq is returned, expressing the fact that the types of the referred values are the same too.

lookup :: Ref a env -> env -> a Source

The function lookup returns the element indexed in the environment parameter by the Ref parameter. The types guarantee that the lookup succeeds.

update :: (a -> a) -> Ref a env -> env -> env Source

The function update takes an additional function as argument, which is used to update the value the reference addresses.


data Env term use def where Source

The type Env term use def represents a sequence of instantiations of type forall a. term a use, where all the instances of a are stored in the type parameter def. The type use is a sequence containing the types to which may be referred from within terms of type term a use.


Empty :: Env t use () 
Ext :: Env t use def' -> t a use -> Env t use (def', a) 

type FinalEnv t usedef = Env t usedef usedef Source

When the types def and use of an Env coincide, we can be sure that the references in the terms do not point to values outside the environment but point to terms representing the right type. This kind of environment is the final environment of a transformation.

newtype T e s Source

The type T encodes a Ref-transformer. It is usually used to transform references from an actual environment to the final one.




unT :: forall x. Ref x e -> Ref x s

lookupEnv :: Ref a env -> Env t s env -> t a s Source

updateEnv :: (t a s -> t a s) -> Ref a env -> Env t s env -> Env t s env Source

data Unit s Source



data Result m t b Source

The type Result is the type of the result of "running" a Trafo. Because s could be anything we have to hide it using existential quantification.


forall s . Result (m s) (b s) (FinalEnv t s)