Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell98 |

Library for Typed Transformations of Typed Abstract Syntax.

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

Bibtex entry: http://www.cs.uu.nl/wiki/bin/viewfile/Center/TTTAS?rev=1;filename=TTTAS.bib

For more documentation see the TTTAS webpage: http://www.cs.uu.nl/wiki/bin/view/Center/TTTAS.

- data Ref a env where
- data Equal :: * -> * -> * where
- match :: Ref a env -> Ref b env -> Maybe (Equal a b)
- lookup :: Ref a env -> env -> a
- update :: (a -> a) -> Ref a env -> env -> env
- data Env term use def where
- type FinalEnv t usedef = Env t usedef usedef
- newtype T e s = T {}
- lookupEnv :: Ref a env -> Env t s env -> t a s
- updateEnv :: (t a s -> t a s) -> Ref a env -> Env t s env -> Env t s env
- data Unit s = Unit
- data Result m t b = forall s . Result (m s) (b s) (FinalEnv t s)

# Typed References and Environments

## Typed References

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`

.

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.

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.

## Declarations

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`

.

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.