úÎ^ [6      !"#$%&'()*+,-./0123456 Alternative version of % where the universal quantification < over |s| is moved inside the quantification over |env2|. H Note that the type variables |a| and |b| are now labelled with |s|, # and hence have kind |(* -> *)|.  The type  is the type of the result of "running" a .  Because sH could be anything we have to hide it using existential quantification.  The type 5 is used to introduce an existential quantifier into  the definition of .  It can be seen that a / is a function taking as arguments: the input (a),  a $-transformer (T env2 s1) from the environment constructed in this step 1 to the final environment and the environment ( Env t s env1 ) where the D current transformation starts. The function returns: the output (b), a  $-transformer (T env1 s:) from the initial environment of this step to the final $ environment and the environment ( Env t s env2) constructed in this step.  The type H is the type of the transformation steps on a heterogeneous collection.  The argument m) stands for the type of the meta-data. Q A |Trafo| takes the meta-data on the current environment |env1| as input and E yields meta-data for the (possibly extended) environment |env2|.  The type t5 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.  The type  encodes a $!-transformer. It is usually used : to transform references from an actual environment to  the final one. When the types def and use of an  coincide, : we can be sure that the references in the terms do not 5 point to values outside the environment but point 6 to terms representing the right type. This kind of  environment is the final environment of a transformation.  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. !"The " type encodes type equality. #$The $- type for represents typed indices which are 5 labeled with both the type of value to which they 3 refer and the type of the environment (a nested 6 Cartesian product, growing to the right) in which  this value lives.  The constructor & expresses that the first 0 element of the environment has to be of type a.  The constructor % does not care about the type - of the first element in the environment, ! being polymorphic in the type b. %&' The function '' compares two references for equality. 8 If they refer to the same element in the environment  the value Just Eq' is returned, expressing the fact that 6 the types of the referred values are the same too. ( The function ($ returns the element indexed in the  environment parameter by the $ parameter. The types ' guarantee that the lookup succeeds. ) The function )! takes an additional function as 4 argument, which is used to update the value the  reference addresses. *+, The Trafo ,: takes a typed term as input, adds it to the environment 3 and yields a reference pointing to this value. : No meta-information on the environment is recorded by ,;  therefore we use the type  for the meta-data. - The function - returns a ' that extends the current environment. . The function . returns a  that casts the reference Y passed as parameter (in the constructed environment) to one in the final environment. / The function / returns a  that updates the value pointed F by the reference passed as parameter into the current environment. 0 The function 0 takes as arguments the # we want to run, meta-information 3 for the empty environment, and an input value.  The result of 0 (type ) 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 00 ensures that transformation steps cannot make 8 any assumptions about the type of final environment (s). 1The combinator 1 sequentially composes a list  of  s into a  that yields a list of outputs. * Its use is analogous to the combinator 6 combinator  for 7s. 2 The function 2 takes as arguments the # we want to run, meta-information 3 for the empty environment, and an input value.  The result of 2 (type ) 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 20 ensures that transformation steps cannot make 8 any assumptions about the type of final environment (s). # It is an alternative version of 0 which does not use  8. 3 The Trafo2 3: takes a typed term as input, adds it to the environment 3 and yields a reference pointing to this value. : No meta-information on the environment is recorded by 3;  therefore we use the type  for the meta-data. 45The combinator 5 sequentially composes a list  of  s into a  that yields a  of outputs. * Its use is analogous to the combinator 6 combinator  for 7s. 6  !"#$%&'()*+,-./0123456$&%"#'()! *+,-./0132   456   ! !"##$&%%&'()*+,-./0123459      !"#$%&'()*+,-./0120340567 TTTAS-0.2Language.TTTASList ArrowLoop2loop2Arrow2arr2first2second2****&&&& Category2id2.:.PairPTrafoE2Trafo2ResultUnitTrafoETrafoTunTFinalEnvEnvExtEmptyEqualEqRefSucZeromatchlookupupdate lookupEnv updateEnvnewSRefextEnvcastSRef updateSRefrunTrafo sequenceA runTrafo2newSRef2>>>> sequenceA2base Control.MonadsequenceGHC.BaseMonad Unsafe.Coerce unsafeCoerce