-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Typed Transformations of Typed Abstract Syntax -- -- Typed Transformations of Typed Abstract Syntax @package TTTAS @version 0.3.0 -- | 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. module Language.TTTAS -- | 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. data Ref a env Zero :: Ref a (env', a) Suc :: Ref a env' -> Ref a (env', b) -- | The Equal type encodes type equality. data Equal :: * -> * -> * Eq :: Equal a a -- | 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. match :: Ref a env -> Ref b env -> Maybe (Equal a b) -- | The function lookup returns the element indexed in the -- environment parameter by the Ref parameter. The types guarantee -- that the lookup succeeds. lookup :: Ref a env -> env -> a -- | The function update takes an additional function as argument, -- which is used to update the value the reference addresses. update :: (a -> a) -> Ref a env -> env -> env -- | 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. data Env term use def Empty :: Env t use () Ext :: Env t use def' -> t a use -> Env t use (def', a) -- | 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. type FinalEnv t usedef = Env t usedef usedef -- | The type T encodes a Ref-transformer. It is usually used -- to transform references from an actual environment to the final one. newtype T e s T :: (forall x. Ref x e -> Ref x s) -> T e s unT :: T e s -> forall x. Ref x e -> Ref x s 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 -- | The type Trafo is the type of the transformation steps on a -- heterogeneous collection. The argument m stands for the type -- of the meta-data. A |Trafo| takes the meta-data on the current -- environment |env1| as input and yields meta-data for the (possibly -- extended) environment |env2|. The type t is the type of the -- terms stored in the environment. The type variable s -- represents the type of the final result, which we do expose. Its role -- is similar to the s in the type ST s a. The -- arguments a and b are the Arrow's input and output, -- respectively. data Trafo m t s a b Trafo :: (forall env1. m env1 -> TrafoE m t s env1 a b) -> Trafo m t s a b -- | The type TrafoE is used to introduce an existential quantifier -- into the definition of Trafo. It can be seen that a -- Trafo is a function taking as arguments: the input -- (a), a Ref-transformer (T env2 s) from the -- environment constructed in this step to the final environment, the -- environment (Env t s env1) where the current transformation -- starts and a function (FinalEnv t s -> FinalEnv t s) to -- update (modify) the final environment. The function returns: the -- output (b), a Ref-transformer (T env1 s) from -- the initial environment of this step to the final environment, the -- environment (Env t s env2) constructed in this step and a -- function (FinalEnv t s -> FinalEnv t s) to update (modify) -- the final environment. NOTE: The function (FinalEnv t s -> -- FinalEnv t s) was introduced in version 0.3. It's carried throw -- the transformation steps and can be modified (composed to another -- function) using the function updateFinalEnv. data TrafoE m t s env1 a b TrafoE :: (m env2) -> (a -> T env2 s -> Env t s env1 -> (FinalEnv t s -> FinalEnv t s) -> (b, T env1 s, Env t s env2, FinalEnv t s -> FinalEnv t s)) -> TrafoE m t s env1 a b data Unit s Unit :: Unit s -- | The Trafo newSRef takes a typed term as input, adds it to the -- environment and yields a reference pointing to this value. No -- meta-information on the environment is recorded by newSRef; -- therefore we use the type Unit for the meta-data. newSRef :: Trafo Unit t s (t a s) (Ref a s) -- | The function extEnv returns a TrafoE that extends the -- current environment. extEnv :: m (e, a) -> TrafoE m t s e (t a s) (Ref a s) -- | The function castSRef returns a TrafoE that casts the -- reference passed as parameter (in the constructed environment) to one -- in the final environment. castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s) -- | The function updateSRef returns a TrafoE that updates -- the value pointed by the reference passed as parameter into the -- current environment. updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s) -- | The function updateFinalEnv returns a Trafo that -- introduces a function (FinalEnv t s -> FinalEnv t s) to -- update the final environment. updateFinalEnv :: Trafo m t s (FinalEnv t s -> FinalEnv t s) () -- | 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. data Result m t b Result :: (m s) -> (b s) -> (FinalEnv t s) -> Result m t b -- | The function runTrafo takes as arguments the Trafo we -- want to run, meta-information for the empty environment, and an input -- value. The result of runTrafo (type Result) is the final -- environment (Env t s s) together with the resulting meta-data -- (m s), and the output value (b s). The rank-2 type -- for runTrafo ensures that transformation steps cannot make any -- assumptions about the type of final environment (s). runTrafo :: (forall s. Trafo m t s a (b s)) -> m () -> a -> Result m t b -- | The combinator sequenceA sequentially composes a list of -- Trafos into a Trafo that yields a list of outputs. Its -- use is analogous to the combinator sequence combinator for -- Monads. sequenceA :: [Trafo m t s a b] -> Trafo m t s a [b] -- | Alternative version of Trafo where the universal quantification -- over |s| is moved inside the quantification over |env2|. Note that the -- type variables |a| and |b| are now labelled with |s|, and hence have -- kind |(* -> *)|. data Trafo2 m t a b Trafo2 :: (forall env1. m env1 -> TrafoE2 m t env1 a b) -> Trafo2 m t a b data TrafoE2 m t env1 a b TrafoE2 :: (m env2) -> (forall s. a s -> T env2 s -> Env t s env1 -> UpdFinalEnv t s -> (b s, T env1 s, Env t s env2, UpdFinalEnv t s)) -> TrafoE2 m t env1 a b -- | The Trafo2 newSRef2 takes a typed term as input, adds it to the -- environment and yields a reference pointing to this value. No -- meta-information on the environment is recorded by newSRef2; -- therefore we use the type Unit for the meta-data. newSRef2 :: Trafo2 Unit t (t a) (Ref a) newtype UpdFinalEnv t s Upd :: (FinalEnv t s -> FinalEnv t s) -> UpdFinalEnv t s -- | The function updateFinalEnv2 returns a Trafo2 that -- introduces a function ((UpdFinalEnv t)) to update the final -- environment. updateFinalEnv2 :: Trafo2 m t (UpdFinalEnv t) Unit -- | The function runTrafo2 takes as arguments the Trafo2 we -- want to run, meta-information for the empty environment, and an input -- value. The result of runTrafo2 (type Result) is the -- final environment (Env t s s) together with the resulting -- meta-data (m s), and the output value (b s). The -- rank-2 type for runTrafo2 ensures that transformation steps -- cannot make any assumptions about the type of final environment -- (s). It is an alternative version of runTrafo which -- does not use unsafeCoerce. runTrafo2 :: Trafo2 m t a b -> m () -> (forall s. a s) -> Result m t b newtype Pair a b s P :: (a s, b s) -> Pair a b s class (Category2 arr) => Arrow2 arr arr2 :: (Arrow2 arr) => (forall s. a s -> b s) -> arr a b first2 :: (Arrow2 arr) => arr a b -> arr (Pair a c) (Pair b c) second2 :: (Arrow2 arr) => arr a b -> arr (Pair c a) (Pair c b) (****) :: (Arrow2 arr) => arr a b -> arr a' b' -> arr (Pair a a') (Pair b b') (&&&&) :: (Arrow2 arr) => arr a b -> arr a b' -> arr a (Pair b b') class (Arrow2 arr) => ArrowLoop2 arr loop2 :: (ArrowLoop2 arr) => arr (Pair a c) (Pair b c) -> arr a b (>>>>) :: (Category2 cat) => cat a b -> cat b c -> cat a c newtype List a s List :: [a s] -> List a s -- | The combinator sequenceA2 sequentially composes a list of -- Trafo2s into a Trafo2 that yields a List of -- outputs. Its use is analogous to the combinator sequence -- combinator for Monads. sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b) instance ArrowLoop2 (Trafo2 m t) instance Arrow2 (Trafo2 m t) instance Category2 (Trafo2 m t) instance ArrowLoop (Trafo m t s) instance Arrow (Trafo m t s) instance Category (Trafo m t s) instance Functor (TrafoE m t s e a)