text:
# A Framework for Datatype Transformation

## 1 Introduction

We study operators for the transformation of the datatype declarations in a program. The presentation will be biased towards the algebraic datatypes in Haskell, but the concepts are of relevance for many typed declarative languages, e.g., Mercury and SML, as well as frameworks for algebraic specification or rewriting like ASF+SDF, CASL, Elan, and Maude. Our transformations are rather syntactical in nature as opposed to more semantical concepts such as data refinement. Our transformations contribute to the more general notion of *functional program refactoring* \[TR01\].

The following introductory example is about extracting a new datatype from constructor components of an existing datatype. This is illustrated with datatypes that represent the syntax of an imperative language. The following extraction identifies a piece of syntax to enable its reuse in later syntax extensions:

\- - Datatypes with focus on two constructor components

|  | $`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝑃𝑟𝑜𝑔}`$ | $`=`$ | $`\mathrm{𝑃𝑟𝑜𝑔}\mathrm{𝑃𝑟𝑜𝑔𝑁𝑎𝑚𝑒}\underset{¯}{\left[\mathrm{𝐷𝑒𝑐}\right]\left[\mathrm{𝑆𝑡𝑎𝑡}\right]}`$ |
| --- | --- | --- | --- |
| $`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝐷𝑒𝑐}`$ | $`=`$ | $`\mathrm{𝑉𝐷𝑒𝑐}\mathrm{𝐼𝑑}\mathrm{𝑇𝑦𝑝𝑒}`$ |
| $`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝑆𝑡𝑎𝑡}`$ | $`=`$ | $`\mathrm{𝐴𝑠𝑠𝑖𝑔𝑛}\mathrm{𝐼𝑑}\mathrm{𝐸𝑥𝑝𝑟}\mathrm{𝐼𝑓}\mathrm{𝐸𝑥𝑝𝑟}\mathrm{𝑆𝑡𝑎𝑡}\mathrm{𝑆𝑡𝑎𝑡}`$ |

\- - After extraction of $`[\mathrm{𝐷𝑒𝑐}][\mathrm{𝑆𝑡𝑎𝑡}]`$ to constitute a new datatype $`\mathrm{𝐵𝑙𝑜𝑐𝑘}`$

|  |  | $`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝑃𝑟𝑜𝑔}`$ | $`=`$ | $`\mathrm{𝑃𝑟𝑜𝑔}\mathrm{𝑃𝑟𝑜𝑔𝑁𝑎𝑚𝑒}\mathrm{𝐵𝑙𝑜𝑐𝑘}`$ |
| --- | --- | --- | --- | --- |
| $`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝐵𝑙𝑜𝑐𝑘}`$ | $`=`$ | $`\mathrm{𝐵𝑙𝑜𝑐𝑘}\left[\mathrm{𝐷𝑒𝑐}\right]\left[\mathrm{𝑆𝑡𝑎𝑡}\right]`$ |

In the present paper, we describe the design of a framework for datatype transformations including the operators for the above extraction. In Sec. 2, we identify all the concerns addressed by the framework. In Sec. 3, we describe all the basic operators for datatype transformations. In Sec. 4, these operators are lifted from datatypes to complete programs. Related work is discussed in Sec. 5. The paper is concluded in Sec. 6.

## 2 Concerns in datatype transformation

The central contribution of the present paper is a simple, well-defined, and ‘editing-complete’ suite of operators for datatype transformations. Before we embark on this suite, we identify the concerns addressed by our approach:

* Datatype transformations via scripting or interactive tool support.
* Well-defined primitives for datatype transformations.
* Generic meta-programming for conciseness of datatype transformations.
* Flexible means of referring to fragments of interest in datatype transformations.

We will now discuss these concerns in some depth.

### 2.1 Scripting vs. interactive tool support

From the point of view of a programmer, datatype transformations should be founded on intuitive scenarios for adaptation. To actually perform (datatype) transformations, there are two modes of operation. The first mode is *scripting*: the programmer encodes the desired transformation as an expression over basic or higher-level operators. The second mode is *interactive* transformation based on a corresponding GUI. The benefits of an interactive tool are rather obvious. Such a tool is useful to issue a transformation on the basis of an operator-specific dialogue, and to provide a tailored list of options for transformations that make sense in a given context. A crucial benefit of interactive transformation is that the GUI can be used to provide feedback to the programmer: Which locations were changed? Where is the programmer’s attention needed to complete the issued transformation scenario? The apparent benefits of scripting such as the opportunities to revise transformations and to replay them can be also integrated into an interactive setting.

In Fig. 1, we illustrate the interactive treatment of the introductory example using our prototypical tool *TH* — *T*ransform *H*askell. As the snapshot indicates, we use a designated *fold* dialogue to perform the extraction of the piece of syntax. (Folding is the basic transformation underlying extraction.) This dialogue combines several transformation steps and side conditions in a convenient way. The figure shows the following situation. The user has selected two consecutive types “\[Dec\] \[Stat\]” and initiated the *fold* dialogue. The user has also typed in “Block” in the “type name” field. The introduction check-box is marked automatically since the given type name does not yet exist. The user has also selected the “kind” radio-button to be “data” and filled in “Block” in the “cons name” field. After this, the user would press “Replace” to make the change. If there had been more than one occurrence, the user could replace them all with “Replace All”, or step through all occurrences with “Next”, and replace only specific ones with “Replace” as with ordinary *find and replace* in text editors.

Here is an open-ended list of further common transformation scenarios:

* Renaming type and constructor names.
* Permuting type arguments and constructor components.
* The dual of extracting datatypes, i.e., inlining datatypes.
* Including a constructor declaration together with associated functionality.
* Excluding a constructor declaration together with associated functionality.
* Inserting a constructor component together with associated functionality.
* Deleting a constructor component together with associated functionality.

### 2.2 Well-defined transformation primitives

The core asset of our framework is a suite of *basic* operators, which can be either used as is, or they can be completed into more complex, *compound* transformations. In the design of this suite, we reuse design experience from a related effort on grammar adaptation \[Läm01\]. Indeed, there is an obvious affinity of grammar transformations and datatype transformations. A challenging problem that we did not need to address in this previous work, is the completion of datatype transformations to apply to entire (functional) programs in which evolving datatypes reside.

We list the required properties of our basic transformation operators:

Mostly, we insist on ‘structure preservation’, that is, the resulting datatype is of the same shape as the original datatype. This is enforced by the pre- and postconditions of the operators.

The operators are ‘editing-complete’, that is, they capture all scenarios of datatype evolution that are otherwise performed by plain text editors. Semantics-preserving adaptations are defined in terms of disciplined primitives.

The operators inhabit well-defined, non-overlapping roles. Higher-level scenarios for interactive transformation are derivable. Operators for datatype transformations are complementary to expression-level transformations.

The basic operators operate on small code locations as opposed to ‘global’ or ‘exhaustive’ operators, which iterate over the entire program. Note that some operators are necessarily exhaustive, e.g., an operator to rename a type name.

The operators are implemented as syntactical transformations that are constrained by simple analyses to check for pre- and postconditions, but which otherwise do not necessitate any offline reasoning.

While the present paper focuses on datatype transformations, the principles that are embodied by our operators are universal in the sense that they also apply to other abstractions than datatypes, e.g., functions or modules.

We do not list these properties to announce a formal treatment. This would be very challenging as we opt for the complex language setup of Haskell. The above properties provide merely a design rationale. A formal approach is an important subject for future work, but it does not contribute anything to the narrow goal of the present paper: to compile an inventory of the basic roles in datatype transformation.

### 2.3 Generic meta-programming

We implement transformation operators and compound meta-programs in Haskell. We reuse a publicly available abstract syntax for Haskell.111The used abstract syntax is part of the Haskell Core Libraries — in the haskell-src package. We rely on generic programming techniques to perform meta-programming on the non-trivial Haskell syntax in Haskell. We use the Strafunski-style222http://www.cs.vu.nl/Strafunski/ of generic programming that allows us to complete functions on specific syntactical sorts into generic traversals that process subterms of the specific sorts accordingly. This style of meta-programming is known to be very concise because one only provides functionality for the types and constructors that are immediately relevant for the given problem.

All our datatype transformations are of type *Trafo* which is defined as follows:

That is, a datatype transformation is a partial function on *HsModule* — the abstract syntactical domain for Haskell modules. Partiality is expressed by means of the $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ type constructor that wraps the result type. Partially is needed to model side conditions.

In Fig. 2, we illustrate generic meta-programming by giving the definition of a simple operator for replacing type names. The specification formalises the fact that type names can occur in two kinds of locations: either on a declaration site, when we declare the type, or on a using site, when we refer to the type in a type expression. So we need to synthesise a transformation which pays special attention to the syntactical domains for declaring and using sites. Indeed, in the figure, there are *two* type-specific ‘ad-hoc’ cases which customise the identity function *idTP*. In the given context, we choose the traversal scheme *full\_tdTP* for ‘*full* *t*op-*d*own traversal in *T*ype-*P*reserving manner’. This way, we will reach each node in the input tree to transform type names on declaring and using sites. The operator *replaceTypeId*, by itself, is a total function. (So the *Maybe* in its type is not really needed here.) Partiality would be an issue if we derived an operator for renaming type names. This necessitates adding a side condition to insist on a fresh new name.

### 2.4 Means of referring to fragments of interest

Both the basic operators for datatype transformation but also actual transformation scenarios in scripts or in interactive sessions need to refer to program fragments of interest. Recall our introductory example. Extracting a type necessitates referring to the constructor components that are meant to constitute the new type. In our framework, we use three ways to refer to fragments of interest:

This approach is particularly suited for interactive transformations. Here, relevant fragments can be directly marked. In Fig. 3, we extend Haskell’s abstract syntax to include term constructors for focusing on relevant fragments in datatype transformations. That is, we are prepared to focus on names of types, on type expressions, and on lists of constructor components.

This approach is particularly suited for scripting transformations. Selectors for Haskell’s type expressions are defined in Fig. 4. The three forms of *TypeSel* represent the three kinds of declarations that involve types. The helper $`\mathrm{𝑇𝑦𝑝𝑒𝑆𝑒𝑙}^{}`$ allows to select any part of a given type expression.

Such predicates typically constrain the type of a term or the top-level pattern. This approach is particularly suited for the repeated application of a transformation to different focuses that match a given predicate.

There are ways to mediate between these different ways of referring to subterms. For example. given a term with a focus marker on a type expression, one can compute the selector that refers to the focused subterm. Given a predicate on type expressions, one can compute the list of all selectors so that an operator that is defined on selectors can be used with predicates as well. Finally, given a selector, one can also add the corresponding focus marker in the input at hand.

## 3 Basic operators for datatype transformation

We will now describe the themes that constitute our operator suite:

* Renaming type and constructor names.
* Permutation of type parameters and constructor components.
* Swapping types on use sites.
* Introduction vs. elimination of type declarations.
* Folding vs. unfolding of type declarations.
* Wrapping vs. unwrapping of constructor components.
* Inclusion vs. exclusion of entire constructor declarations.
* Insertion vs. deletion of constructor components.

As this list makes clear, we group an operator with its inverse such as in “folding vs. unfolding”, unless the operator can be used to inverse itself. This is the case for renaming, permutation, and swapping. The operators from the first six groups are (almost) *structure-preserving*. The last two groups deal with *structure-extending* and *-reducing transformations*. We will now explain the operators in detail including illustrative examples. We will only explain the effect of the operators on datatype declarations while we postpone lifting the operators to the level of complete programs until Sec. 4.

### 3.1 Renaming and permutation

Let us start with the simplest datatype refactorings one can think of. These are transformations to consistently rename type or constructor names, and to permute parameters of type and constructor declarations. In Fig. 5, a simple example is illustrated. We rename the type name $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$, the constructor names *Nil* and *Cons*, and we permute the two parameter positions of *Cons*. The resulting datatype specifies a $`\mathrm{𝑆𝑛𝑜𝑐𝐿𝑖𝑠𝑡}`$ as opposed to the $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$ before.

In Fig. 6, we declare the operators for renaming names and permuting parameter lists. In Fig. 7, we include the script that encodes the $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$-to-$`\mathrm{𝑆𝑛𝑜𝑐𝐿𝑖𝑠𝑡}`$ sample as a sequence of basic renaming and permuting transformations. To this end, we assume a sequential composition operator *seqTrafo* for datatype transformations. (In the script, *seqTrafo* is used as an infix operator ‘*seqTrafo*‘.)

### 3.2 Introduction vs. elimination

The next group of operators deals with the introduction and elimination of type declarations (see Fig. 8). Introduction means that the supplied types are added while their names must not be in use in the given program. Elimination means that the referenced types are removed while their names must not be referred to anymore in the resulting program. The two operators take *lists* of types as opposed to single ones because types can often only be introduced and eliminated in groups, say mutually recursive systems of datatypes. All kinds of type declarations make sense in this context: aliases, newtypes, and proper datatypes. The operators for introduction and elimination are often essential in compound transformations. This will be illustrated below when we reconstruct the introductory example in full detail (see Sec. 3.4).

### 3.3 Folding vs. unfolding

Instantiating the folklore notions of unfolding and folding for datatypes basically means to replace a type name by its definition and vice versa. Extra provisions are needed for parameterised datatypes. The prime usage scenarios for the two operators are the following:

* *extraction* = *introduction* of a type followed by its *folding*.
* *inlining* = *unfolding* a type followed by its *elimination*.

To give an example, the introductory example basically *extracts* the structure of imperative program blocks. To actually reconstruct this example, we need a few more operators. So we postpone scripting the example (see Sec. 3.4).

The operators for folding and unfolding are declared in Fig. 9, The operators make a strict assumption: the type which is subject to folding or unfolding is necessarily a type alias as opposed to a proper datatype. This assumption simplifies the treatment of the operators considerably since type aliases and their definitions are equivalent by definition. Extra operators for so-called wrapping and unwrapping allow us to use proper datatypes during folding and unfolding as well. This will be addressed below. In the type of the *foldAlias* operator, we do not just provide a type name but also a list of type variables (cf. helper type *TypeHdr*). This is needed for parameterised datatypes, where we want to specify how the free type variables in the selected type expression map to the argument positions of the type alias.

The preconditions for the operators are as follows. In the case of *foldAlias*, we need to check if the referenced type expression and the right-hand side of the given alias declaration coincide. In the case of unfolding, we need to check that the referenced type expression corresponds to an application of a type alias.

### 3.4 Wrapping vs. unwrapping

We will now consider operators that facilitate certain forms of wrapping and unwrapping of datatype constructors (see Fig. 10). There are operators for grouping and ungrouping, that is, to turn consecutive constructor components into a single component that is of a product type, and vice versa. There are also operators to mediate between the different kinds of type declarations, namely type aliases, newtypes and datatypes. This will allow us to toggle the representation of datatypes in basic ways. As a result, the normal forms assumed by other operators can be established; recall, for example, the use of type aliases in folding and unfolding. This separation of concerns serves orthogonality.

In Fig. 11, we show the steps that implement the introductory example. As one can see, we basically implement extraction, but extra steps deal with grouping and ungrouping the two components subject to extraction. Also, the extracted type should be a proper datatype as opposed to a type alias (see transition from 3. to 4.). For completeness’ sake, the transformation script is shown in Fig. 12. The script precisely captures the steps that underly the interactive transformation in Fig. 1.

Some of the operators are not completely structure-preserving, that is, strictly speaking, the structures of the datatypes before and after transformation are not fully equivalent. For example, a newtype and a datatype are semantically distinguished, even if the defining constructor declaration is the very same. (This is because a constructor of a datatype involves an extra lifting step in the semantical domain, i.e., there is an extra ‘bottom’ element.) The operators for grouping and ungrouping also deviate from full structure preservation.

### 3.5 Swapping types on use sites

We will now deal with transformations that eliminate or establish type distinctions by what we call *swapping* types on use sites. In Fig. 13, we illustrate a typical application of swapping. In the example, we want to generalise the standard datatype $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ to allow for lists instead. In fact, we do not want to change the general definition of the library datatype $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$, but we only want to change it on one use site (not shown in the figure). This is where swapping helps: as an intermediate step, we can replace $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ on the use site by a newly introduced datatype $`\mathrm{𝑀𝑎𝑦𝑏𝑒}^{}`$ with equivalent structure. The figure illustrates how subsequent adaptations derive the *ConsList* datatype from the clone of the *Maybe* datatype. In particular, we add the boxed constructor component.

The swapping operators are declared in Fig. 14. There is one operator for type aliases and another for datatype declarations. In the case of proper datatypes, one needs to match the constructors in addition to just the names of the types. This is modelled by the helper datatype *DataUnifier*. The type of the operator *swapData* clarifies that we are prepared to process a list of *DataUnifier*s. This is necessary if we want to swap mutually recursive systems of datatypes.

### 3.6 Inclusion vs. exclusion

We now leave the ground of structure-preserving transformations. That is, we will consider transformations where input and output datatypes are not structurally equivalent. In fact, we consider certain ways to extend or reduce the structure of the datatype. The first couple of structure-extending and -reducing transformations is about inclusion and exclusion of constructor declarations (see Fig. 15). These operators are only feasible for proper datatypes and not for type aliases or newtypes. (This is because a type alias involves no constructor at all, and a newtype is defined in terms of precisely one constructor declaration.)

In Fig. 16, we show an example for constructor inclusion. In fact, we just continue the introductory example to make use of the extracted block structure in a language extension for statement blocks. That is, we include a constructor application for *Stat* to capture *Block* as another statement form. This continuation of the introductory example amplifies the intended use of our operator suite: for program evolution in the sense of datatype refactoring and adaptation.

### 3.7 Insertion vs. deletion

Inclusion and exclusion of constructor declarations is about the *branching* structure of datatypes. We will now discuss operators that serve for the insertion or deletion of constructor *components* (see Fig. 17). Insertion of a component $`c`$ into a constructor declaration $`Cc_1\mathrm{}c_n`$ proceeds as follows. Given the target position for the new component, be it $`in+1`$, the new constructor declaration is simply of the form $`Cc_1\mathrm{}c_{i1}cc_i\mathrm{}c_n`$. In general, $`c`$ might need to refer to type parameters of the affected datatype. Deletion of a constructor declaration relies on the identification of the obsolete component.

In Fig. 18, we elaborate on the earlier example for generalising ‘maybies’ to lists (recall Fig. 13). At the top of Fig. 18, we see three datatypes $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$, $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$, and $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$. The idea is indeed to replace $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ by $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$ in the using occurrence in $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$. (That is, we want to allow for a function from $`a`$ to a list of $`a`$s instead of a partial function from $`a`$ to $`a`$.) We call this adaptation a generalisation because a list is more general than an optional. In the initial phase of the generalisation of $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$, we disconnect the relevant occurrence of $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ in $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$ from other possible occurrences in the program. So we introduce a copy $`\mathrm{𝑀𝑎𝑦𝑏𝑒}^{}`$ of $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$, and we perform type swapping so that $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$ refers to $`\mathrm{𝑀𝑎𝑦𝑏𝑒}^{}`$ instead of the ‘read-only’ $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$. Now we need to make $`\mathrm{𝑀𝑎𝑦𝑏𝑒}^{}`$ structurally equivalent to $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$. This amounts to adding a recursive component to the second constructor $`\mathrm{𝐽𝑢𝑠𝑡}^{}`$. Then, we can again swap types to refer to $`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$ in the co-domain of $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$.

## 4 Datatype transformation meets program transformation

We will now re-iterate over the groups of operators to investigate their impact on functional programs. It would be utterly complex to formalise the link between datatype and program transformation. The mere specification of the transformations is already intractable for a publication because of its size, and the number of details. So we will describe the implied program transformations informally while omitting less interesting details.

### 4.1 Renaming

Type names only occur inside type declarations and type annotations. So there is no need to adapt expressions or function declarations except for their signatures, or the type annotations of expressions. Constructor names can very well occur inside patterns and expressions that contribute to function declarations. Renaming these occurrences is completely straightforward.

### 4.2 Permutation

The permutation of type parameters does not necessitate any completion at the level of function declarations. The permutation of constructor components, however, needs to be realized in patterns and expressions as well. This is particularly simple for pattern-match cases because all components are matched by definition. Hence, we can directly permute the sub-patterns in an affected constructor pattern. Witnessing permutations of constructor components in expression forms is slightly complicated by currying and higher-order style. Instead of permuting components in possibly incomplete constructor applications, we could first get access to all components by ‘$`\lambda `$-pumping’: given a constructor $`C`$ with say $`n`$ potential components according to its declaration, we first replace $`C`$ by $`\lambda x_1\mathrm{}x_n.Cx_1\mathrm{}x_n`$ as justified by $`\eta `$-conversion. Then, we witness the permutation by permuting the arguments $`x_1`$, …, $`x_n`$ in the pumped-up expression. In the presence of a non-strict language with an evaluation order on patterns, the permutation of constructor components might actually change the behaviour of the program regarding termination. We neglect this problem. We should also mention that it is debatable if the described kind of $`\eta `$-conversion is really what the programmer wants because it obscures the code.

### 4.3 Introduction vs. elimination

Introduction does not place any obligations on the functions defined in the same program. In the case of elimination, we have to ensure that the relevant types are not used by any function. If we assume that all function declarations are annotated by programmer-supplied or inferred signatures, then the precondition for elimination can be checked by looking at these signatures. There is an alternative approach that does not rely on complete type annotations: we check that no constructor of the relevant types is used.

### 4.4 Folding vs. unfolding

The restriction of folding and unfolding to type aliases guarantees that these operators do not necessitate any adaptation of the function declarations. This is simply because interchanging a type alias and its definition is completely structure- and semantics-preserving, by definition. This is extremely convenient: despite the crucial role of the operators for folding and unfolding, they do not raise any issue at the level of function declarations.

### 4.5 Wrapping vs. unwrapping

*Grouping and ungrouping* These operators are handled using the same overall approach as advocated for the permutation of constructor components. That is, in patterns we witness grouping or ungrouping by inserting or removing the enclosing “( … )”; in expressions, we perform $`\eta `$-conversion to access the relevant components, and then we group or ungroup them in the pumped-up constructor application.

*Mediation between newtypes and datatypes* These datatype transformations do not imply any adaptations of the functions that involve the datatype in question. (As we indicated earlier, the extra bottom value of a datatype, when compared to a newtype, allows a program to be ‘undefined’ in one more way.)

*Newtype to alias migration* We simply remove all occurrences of the associated constructor both in pattern and expression forms. We require that the relevant newtype is not covered by any instance declaration of some type class or constructor class. Otherwise, we had to inline these members in a non-obvious way prior to the removal of the constructor. If we neglected this issue, the resulting program either becomes untypeable, or a different instance is applied accidentally, which would be hazardous regarding semantics preservation.

*Alias to newtype migration* This operator requires a non-trivial treatment for function declarations. The crucial issue is how to know the following:

* What expressions have to be wrapped with the newtype constructor?
* In what patterns does the newtype constructor need to be stripped?

Our approach is as simple as possible. We observe that the new newtype might be used in the declarations of other datatypes. The corresponding patterns and expressions can be easily located and adapted as in the case of permutation, grouping, and ungrouping (recall $`\eta `$-conversion etc.). We also need to adapt function declarations if their argument or result types are known to refer to the relevant alias. This basically means that we need to access the affected arguments and result expressions in all relevant equations to unwrap the arguments and wrap the result expressions. These adaptations are slightly complicated by the fact that the affected type alias can occur in arbitrarily nested locations.

In Fig. 19, we illustrate the effect of the *alias2newtype* operator in the introductory example. We show the top-level interpreter function that maps over the statements of the program. (The program name and the declarations do not carry any semantics here.) The type of the function *run* exhibits that the meaning of a program is a computation that involves a *State* for the program variables. The adapted version of *run* refers to the extra constructor *Block*, which resulted from extraction.

### 4.6 Swapping types on use sites

This operator relies on the same techniques as *alias2newtype*. However, instead of wrapping and unwrapping a constructor. We invoke conversion functions that mediate between the two structurally equivalent types. These mediators merely map old to new constructors and vice versa, and hence they are immediately induced by the datatype transformation itself, namely by the *DataUnifier*s passed to the swap operator. This approach implies that we only perform very local changes. The program code will still work on the old datatypes thanks to the mediators.

The impact of swapping types at the function level is illustrated in Fig. 20. We deal with the initial steps of the $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$-to-$`\mathrm{𝐶𝑜𝑛𝑠𝐿𝑖𝑠𝑡}`$ migration in Fig. 18, where we replace the occurrence of $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ within $`\mathrm{𝑇𝑟𝑎𝑛𝑠𝑅𝑒𝑙}`$ by a structurally equivalent $`\mathrm{𝑀𝑎𝑦𝑏𝑒}^{}`$. We show an illustrative function $`\mathrm{𝑑𝑒𝑎𝑑𝐸𝑛𝑑}`$ which performs a test if the given transition relation allows for a transition in the presence of a given state $`a`$. The adapted function $`\mathrm{𝑑𝑒𝑎𝑑𝐸𝑛𝑑}`$ refers to the conversion function $`\mathrm{𝑡𝑜𝑀𝑎𝑦𝑏𝑒}`$ prior to performing pattern matching on the obsolete $`\mathrm{𝑀𝑎𝑦𝑏𝑒}`$ type.

### 4.7 Inclusion vs. exclusion

Intuitively, the inclusion of a constructor should be complemented by the extension of all relevant case discriminations. This normally means to add a pattern-match equation (or a case to a case expression) for the new constructor. Dually, exclusion of a constructor should be complemented by the removal of all pattern-match equations (or cases) that refer to this constructor. In the case of added pattern-match equations, we view the right-hand sides of these equations as a kind of ‘hot spot’ to be resolved by subsequent expression-level transformations. To this end, we use “undefined”, i.e., “$``$”, as a kind of to-do marker. Dually, in the case of removed constructors, we also need to replace occurrences of the constructor within expressions by “$``$”. When using interactive tool support, these to-do markers are useful to control further steps in a transformation scenario.

In Fig. 21, we progress with our running example of an interpreter for an imperative language. We illustrate the step where blocks are turned into another form of statements. Hence, the shown output program involves a new pattern-match equation that interprets statement blocks. This added equation reflects that the meaning of such blocks is as yet undefined, subject to subsequent adaptations.

### 4.8 Insertion vs. deletion

Inserting a component into a declaration for a constructor $`C`$ means that all patterns with $`C`$ as outermost constructor must be adapted to neglect the added component, and all applications of $`C`$ must be completed to include “$``$” for the added component. Dually, deletion of a component from $`C`$ means that all applications of $`C`$ and all patterns with $`C`$ as outermost constructor need to be cleaned up to project away the obsolete component. Any reference to a pattern variable for the obsolete component is replaced by “$``$”. As in the case of permutation and others, $`\eta `$-conversion is needed to actually get access to constructor components in expressions.

In Fig. 22, the insertion of a constructor component is illustrated by continuing the scenario from Fig. 20. The adapted equation of $`\mathrm{𝑡𝑜𝑀𝑎𝑦𝑏𝑒}`$ involves an extended pattern. As the don’t care pattern “\_” indicates, the definition of *toMaybe* does not make use of the added component. In fact, the definition of the function *deadEnd* does not need to be adapted; it only tests for the availability of a transition step. Normally, other functions will start to rely on the richer pattern.

## 5 Related work

*Transformational program development* Formal program transformation \[BD77\] separates two concerns: the development of an initial, maybe inefficient program the correctness of which can easily be shown, and the stepwise derivation of a better implementation in a semantics-preserving manner. Partsch’s textbook \[Par90\] describes the formal approach to this kind of software development. Pettorossi and Proietti study typical transformation rules (for functional and logic) programs in \[PP96\]. Formal program transformation, in part, also addresses datatype transformation \[dRE98\], say data refinement. Here, one gives different axiomatisations or implementations of an abstract datatype which are then related by well-founded transformation steps. This typically involves some amount of mathematical program calculation. By contrast, we deliberately focus on the more syntactical transformations that a programmer uses anyway to adapt evolving programs.

*Database schema evolution* There is a large body of research addressing the related problem of database schema evolution \[BKKK87\] as relevant, for example, in database re- and reverse engineering \[HTJC93\]. The schema transformations themselves can be compared with our datatype transformations only at a superficial level because of the different formalisms involved. There exist formal frameworks for the definition of schema transformations and various formalisms have been investigated \[MP97\]. An interesting aspect of database schema evolution is that schema evolution necessitates a database instance mapping \[BCN92\]. Compare this with the evolution of the datatypes in a functional program. Here, the main concern is to update the function declarations for compliance with the new datatypes. It seems that the instance mapping problem is a special case of the program update problem.

*Refactoring* The transformational approach to program evolution is nowadays called refactoring \[Opd92, Fow99\], but the idea is not new \[ABFP86, GN90\]. Refactoring means to improve the structure of code so that it becomes more comprehensible, maintainable, and adaptable. Interactive refactoring tools are being studied and used extensively in the object-oriented programming context \[Moo96, RBJ97\]. Typical examples of *functional* program refactorings are described in \[Läm00\], e.g., the introduction of a monad in a non-monadic program. The precise inhabitation of the refactoring notion for functional programming is being addressed in a project at the University of Kent by Thompson and Reinke; see \[TR01\]. There is also related work on type-safe meta-programming in a functional context, e.g., by Erwig \[ER02\]. Previous work did not specifically address datatype transformations. The refactorings for object-oriented class structures are not directly applicable because of the different structure and semantics of classes vs. algebraic datatypes.

*Structure editing* Support for interactive transformations can be seen as a sophistication of structure editing \[RT88, Koo94, KS98\]. This link between transformation and editing is particularly appealing for our “syntactical” transformations. Not surprisingly, concepts that were developed for structure editing are related to our work. For example, in \[SdM99\], primitives of structure editing are identified based on the notion of focus to select subtrees, and on navigation primitives left, right, up and down. Trees, subtrees and paths are here defined as follows:
$`\mathrm{𝐝𝐚𝐭𝐚}\mathrm{𝑇𝑟𝑒𝑒}`$ $`=`$ $`\mathrm{𝐹𝑜𝑟𝑘}\mathrm{𝐿𝑎𝑏𝑒𝑙}\left[\mathrm{𝑇𝑟𝑒𝑒}\right]`$  $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑆𝑢𝑏𝑇𝑟𝑒𝑒}`$ $`=`$ $`(\mathrm{𝑃𝑎𝑡ℎ},\mathrm{𝑇𝑟𝑒𝑒})`$  $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝑃𝑎𝑡ℎ}`$ $`=`$ $`\left[\mathrm{𝐿𝑎𝑦𝑒𝑟}\right]`$  $`\mathrm{𝐭𝐲𝐩𝐞}\mathrm{𝐿𝑎𝑦𝑒𝑟}`$ $`=`$ $`(\mathrm{𝐿𝑎𝑏𝑒𝑙},\left[\mathrm{𝑇𝑟𝑒𝑒}\right],\left[\mathrm{𝑇𝑟𝑒𝑒}\right])`$

The $`t`$ in a subtree $`(p,t)`$ is the currently selected tree and it is between the left and right trees in the top layer (the head of the $`p`$). This approach does not account for the heterogeneous character of language syntaxes, but it shows that the fact if a focus resides in a term can be encoded in types.

## 6 Concluding remarks

*Contribution* We identified the fundamental primitives for datatype transformation. These operators are meant to support common scenarios of program adaptation in functional programming, or other settings where algebraic datatypes play a role. In fact, all the identified operators are universal in the sense, that they are also meaningful for other program abstractions than just datatypes, e.g., function declarations. We deliberately focused on adaptations of datatypes because a vast body of previous work addressed fold/unfold transformations for recursive functions. Despite the focus on datatype transformations, we had to consider program transformations that are necessitated by the modification of datatypes. Regarding the executable specification of the operator suite, we adhered to the formula: meta-programs = object-programs = Haskell programs. We employed generic functional programming in the interest of conciseness. We also employed designated means of referring to fragments of interest, e.g., a focus concept.

*Partial project failure* We are confident that the identified operators are sufficient and appropriate for actual datatype transformations. We have attempted to complement this framework development by actual interactive tool support. We initially thought that using Haskell for this interactive tooling as well would be a good idea. Since the actual transformation operators are implemented in Haskell anyway, and the interactive dialogues need to cooperate with the operator framework to perform analyses, Haskell indeed seems to be the obvious choice. To make a long story short, there are many GUI libraries for Haskell, but none of them is suitable for developing a sophisticated GUI for interactive program transformation at the moment. It seems that environments for interactive language tools would provide a better starting point, e.g., environments based on attribute grammars \[RT88, KS98\].

*Perspective* To cover full Haskell, a few further operators would have to be added to our suite, in particular, operators that support type and constructor classes. We should also pay full attention to some idiosyncrasies of Haskell; cf. refutable vs. irrefutable patterns. Then, there are also transformation techniques that seem to go beyond our notion of program evolution but it is interesting to cover them anyway. We think of techniques like turning a system of datatypes into functorial style, or threading a parameter through a system of datatypes. The ultimate perspective for the presented work is to integrate the datatype transformations into a complete, well-founded, and user-friendly refactoring tool for functional programming along the lines of Thompson’s and Reinke’s research project \[TR01\]. Another perspective for our research is to further pursue the intertwined character of datatype and program transformations in the context of XML format and API evolution.


format: text

text:
# European accelerator-based neutrino projects

## 1 Introduction

Traditionally, accelerator-based neutrino physics in Europe has been centred around CERN. Also for the future, this laboratory is expected to play a leading role in neutrino physics, despite the heavy commitment in the construction of LHC.

Due to the small atmospheric neutrino mass difference squared, the attention of the neutrino community is presently shifted towards long-baseline project. The CERN neutrino beam to Gran Sasso is higher in energy with respect to the Japanese $`^\mathrm{?}`$ or American $`^\mathrm{?}`$ projects, and will have the unique feature of being well above threshold for $`\tau `$ lepton production, in order to confirm the $`\nu _\mu \nu _\tau `$ nature of the atmospheric oscillations.

The OPERA detector is a dedicated experiment to search for $`\tau `$ appearance using topological informations, while ICARUS is a more versatile apparatus, that could reach similar $`\tau `$ identification capabilities, provided a sufficient number of modules is built.

On the longer term, the European projects are focused towards the possibility of building a super-beam based on a Superconducting Proton Linac (SPL), that also would be the first building block of a CERN-based neutrino factory. To estimate the flux of neutrinos produced in a super-beam, or the number of muons accelerated in a neutrino factory, a dedicated experiment (HARP) is presently under way. The Harp detector, built in a very short time, has taken data in summer 2001 and will have a second run in summer 2002 at the CERN PS. The goal is to measure total and differential cross sections for proton interactions with a large variety of targets, with energy in the range 3-15 GeV.

## 2 The Neutrino beam from CERN to Gran Sasso

As stated in the introduction, the CERN beam to Gran Sasso has the unique characteristic of being at a sufficiently high energy to produce a detectable number of $`\tau `$ leptons in charged current $`\nu _\tau `$ interactions. This is a natural consequence of using a high-energy proton driver (400 GeV from the CERN SPS), having as a natural target the Gran Sasso lab near Rome (distant 732 km from CERN) and of the practical difficulties of building a near station, that makes hard to conceive disappearance measurements.

Civil engineering construction started on Oct 12, 2000; they will consist of 3 km of new tunnels and caverns: 700 m for the proton line to the target, 1 km of decay tube, plus various connections. Overall it will mean 45000 $`m^3`$ of rock removal, and 12000 $`m^3`$ of concrete added to reinforce the walls. The main properties of the CNGS beam are listed in table 1.

The beam target will be 2 meters long, made of 10 cm long graphite (pure carbon) rods, interspaced to minimise absorption of pions with small transverse momentum with respect to the beam direction. Due to the strong thermical shocks, the whole system is cooled with helium. Secondaries produced in interactions with the target are focalised by a horn/reflector system. The horn will be 6.5 m long, with a diameter of 70 cm, and able to sustain a current of 150 kA for 1 ms, with a tolerance rate of 95% survival probability after $`5\times 10^7`$ pulses. A horn prototype has already been built and tested, and survived 1.5 million pulses.

The beam transverse profile will be checked using two muon detectors at the end of the decay tunnel; the beam width at the far location is more than one kilometre, and approximately flat for a radius of about 500 m, much larger than the expected width of the detectors. Systematic uncertainties on the beam can arise from misalignment of the various components. As a reference, a 3% variation in the number of $`\nu _\mu `$ in Gran Sasso could result from:

* the horn being off-axis by 6 mm
* the reflector being off-axis by 30 mm
* the beam being off-axis by 1 mm on the target
* an overall misalignment of 0.5 mrad

Beam alignment can be further checked in the Gran Sasso site, looking for the muons produced by neutrino interactions in the upstream rock. However, we have to bear in mind that flux systematics is not that relevant when doing an appearance experiment with few candidate events.

Possible upgrade schemes for the PS/SPS complex, in order to increase the neutrino flux, have been extensively studied $`^\mathrm{?}`$. It was found out that most of the components are at their limits. A gain of a factor 1.5 seems feasible; however, a factor 3 seems the absolute maximum, even if large investments are made.

The Gran Sasso laboratory from INFN (Laboratori Nazionali del Gran Sasso, LNGS) is operational since 1987, and offers an easy access from a motorway tunnel, and 1500 meters of rock overburden. The completion of the first generation of experiments (e.g. MACRO) leaves space in two large underground hall (B and C), oriented towards CERN, to perform long-baseline neutrino experiments. The two experiments foreseen for the long-baseline project are OPERA $`^\mathrm{?}`$, already fully approved as CNGS1, a dedicated experiment to look for $`\tau `$ kink in a hybrid emulsion system, and ICARUS $`^\mathrm{?}`$, of which the first module has already been built and successfully tested, a general-purpose detector based on a liquid Argon TPC.

## 3 OPERA

The requirement to have a large mass and a space resolution of the order of 1 $`\mu `$ m has lead to the choice of hybrid emulsions as basic detector component. A basic cell is composed of 1 mm lead planes, separated by an emulsion layer made of two 50 mm emulsion sheets separated by 100 $`\mu `$m plastic base. 56 such lead-emulsion cells constitute a brick, 3000 bricks, together with an extruded scintillator plane for quasi-online identification of interesting interactions are a module, 24 modules, completed with a muon spectrometer, form a supermodule. The experiment will be made of 3 such supermodules, for a total mass of about 2 ktons. The emulsion surface will be 176000 $`m^2`$; as a comparison, that of CHORUS was about 500 $`m^2`$. Given the very large amount of emulsion surface, finding few $`\tau `$ events, for an average $`\tau `$ decay length of half a millimetre, is an extremely challenging task. The first step will be the use of the scintillator tracker plane behind the bricks to identify where neutrino interactions take place. These bricks are removed from the wall, with a rate of about 40 bricks per day. They are exposed for a short period to cosmic rays in a shallower location, always in Gran Sasso, to provide a reference for the alignment, and then the emulsions are developed. Then, a search for a neutrino vertex and a decay candidate is performed quasi-online by various scanning stations. The goal is to understand if the brick extracted is sufficient for $`\tau `$ search, or additional nearby bricks have to be extracted. Finally, about 500 squared meters of emulsions (a factor 100 more than at CHORUS) are sent to the scanning labs.

The scanning speed is a fundamental factor to ensure the success of the experiment. A factor 20 improvement with respect to the present speed is expected from the use of the S-UTS technology presently under development in the Japanese laboratory of Nagoya University. This system is based on a fast CCD camera (3000 frames per second) connected to microscopes, with continuous movement on the x-y plane. The z position is determined by the focusing plane of the microscopes, controlled by pizo-attenuators. The scanning speed envisaged is 20 sqcm per hour, and the amount of data reduction from pixel to track of the order of $`10^5`$.

The strategy for $`\tau `$ search is based first on finding a vertex, i.e. a common starting point for tracks with $`\mathrm{tan}\theta <0.4`$, that are followed back until not any more found in two successive layers. Including geometrical losses, a vertex finding efficiency of 80% is expected. Then the search is split in two, depending on weather the $`\tau `$ decays in the same lead layer (short decays) or in the next. In the first case, the requirement is to have the momentum of the primary track above 1 GeV, and an impact parameter larger than a value, dependent on the z position, between 5 and 20 $`\mu `$m. In case of long decays, the requirement is to have a kink angle of 20 mrad with respect to the initial track (the kink angle resolution is about 3 mrad). The signal efficiency for several event categories is shown in table 2, and the number of expected backgrounds in table 3.

In absence of signal, OPERA can exclude at 90% C.L. $`\nu _\mu \nu _\tau `$ oscillations for $`\mathrm{\Delta }m^2<1.2\times 10^3eV^2`$ at full mixing, and $`\mathrm{sin}^22\theta <5.7\times 10^3`$ at large $`\mathrm{\Delta }m^2`$. The number of expected events for signal and background for various values of $`\mathrm{\Delta }m^2`$ and maximal mixing are shown in table 4

## 4 ICARUS

The ICARUS detector is composed of a large liquid Argon TPC, that combines big mass and a granularity of the order of 1 mm, being a veritable electronic bubble chamber. Its resolution and particle identification capabilities allow this kind of detector to contribute to a vast and versatile physics program, that includes study of atmospheric neutrinos, solar neutrinos, nucleon decay and of course neutrinos from the long baseline beam.

Drifting electrons for distances of the order of 1 meter, needed to achieve a sufficient detector mass, requires an extreme purity of the liquid Argon: the tolerance is a concentration of electronegative impurities at the level of 0.1 parts per billion, that was finally achieved after 10 years of R&D.

A 600 ton module has been built during the last years in Pavia, and successfully tested this summer with cosmic ray data. Many long ( 20 meters) muon events were observed, as well as other interesting events such as electromagnetic showers, stopping muons and strange particles.

This 600 ton detector will be transported to Gran Sasso at the beginning of 2003. The ICARUS technology is very well-suited for $`\tau `$ search, using a kinematic approach, complementary to the topological one of OPERA. However, 600 tons are not sufficient to produce enough events when the tight cuts necessary for large background suppression are applied. The ICARUS collaboration has recently proposed $`^\mathrm{?}`$ an upgrade to 5 modules, for a total fiducial mass of 2.35 kton. Golden $`\tau e`$ events can be identified cutting on fiducial volume, electron momentum, visible energy, electron $`P_t`$ and $`Q_t`$ and missing momentum. The best sensitivity is obtained combining several variables in a common likelihood, and efficiencies and backgrounds for a 3 kton ICARUS (table 5) is similar to that of OPERA.

Due to its good electron identification, ICARUS will also be able to perform a search for $`\nu _\mu \nu _e`$ oscillations, improving by some factors the present limit on $`\mathrm{sin}^22\theta _{13}`$.

## 5 The CERN-Frejus Super-Beam

In the next 15-20 years the main commitment of CERN will be the construction and operation of LHC and its detectors. However, the European neutrino community is very active in trying to shape a next-generation neutrino program, in the context of a future CERN-based neutrino factory. The first brick of such a machine would be a low energy (2.2 GeV) high power (4 MW) proton linac$`^\mathrm{?}`$.

Independently of the neutrino factory, this machine would be a considerable improvement to the CERN accelerator complex, since it will increase PS beam intensity, triple the brilliance of the LHC beam, supply the present ISOLDE facility with 5 times more current (or up to 100 times for Super-ISOLDE), and allow the construction of a low-energy superbeam.

Focusing the pions in the energy range of their maximal production, the resulting mean neutrino energy is about 250 MeV, an ideal energy for a water Cerenkhov detector. At this energy, the maximum of the oscillation occurs for a baseline of about 130 Km, the distance between CERN and the Frejus tunnel. Due to the civil engineering work foreseen to build a second motorway gallery, it is conceivable to propose building there a large Cerenkhov detector, to be used for proton decay, supernova and beam neutrinos, like that proposed by the UNO collaboration $`^\mathrm{?}`$. Considering 400 kton of fiducial mass, a $`\pi ^0`$/e separation with 0.1 % confusion and efficiency around 70%, the 90% C.L. sensitivity to $`\mathrm{sin}^22\theta _{13}`$ would be in the range of $`5\times 10^4`$ after 5 years for the current values of $`\mathrm{\Delta }m^2`$. A ten times smaller exposure would already allow measuring $`\mathrm{sin}^2\theta _{23}`$ at 1% level and $`\mathrm{\Delta }m_{23}^2`$ with a precision of $`10^4`$. For CP violation studies, even in the case of a favourable choice of parameters, 400 kton are needed, for 2 years of running with neutrinos and 10 years with antineutrinos.

## 6 The beta-beam

A recent interesting possibility$`^\mathrm{?}`$ is producing a neutrino beam from the decay of radioactive ions collected in a storage ring. Antineutrinos would be for instance produced by the decay $`{}_{}{}^{6}He^{++}^6Li^{+++}\overline{\nu }_ee^{}`$, and neutrinos from similar decays of $`{}_{}{}^{18}Ne`$. The advantage of this approach with respect to the “traditional” Neutrino factory is that despite the lower intensities of the stored beam, the much larger quality factor $`\mathrm{\Gamma }/E_0`$ for ions produces a very collimated neutrino beam, leading to fluxes in the far detector similar to those of a super-beam, for comparable energies. The produced beam will be extremely clean and well-known, and of only the electron neutrino flavour. Moreover, it is possible to think of an experiment combining the beta-beam and the super-beam, that would produce an almost pure $`\nu _\mu `$ beam, separated from the $`\nu _e`$ beta-beam using timing information. Such a system would have the two-beam feature of the neutrino factory, but it will not need a magnetic detector to distinguish oscillated and beam events. Therefore, larger detector with lower threshold can be used (like a water Cerenkov), putting them at shorter distance to minimise matter effect. A high-intensity combination of super-beam and beta-beam could search for T-violation in an extremely convincing way.

## 7 Other experiments

The HARP detector, presently running at CERN, is not strictly speaking a neutrino experiment, but it will provide measurement of hadron production at small and large angles for a variety of target material of interest for neutrino beams. In particular large angle pion production is important in the design of the focusing system of a Neutrino Factory and a Super-Beam. It will also use cryogenic targets made of liquefied gases for hadronic production in the atmosphere in the region of interest of atmospheric neutrinos, as well as the measurement of replicas of existing neutrino targets (K2K, MiniBOONE). Several million of events have been collected in summer 2001, and a similar statistics will be collected this year. Since several sources of data-taking inefficiency have been removed, the number of useful events is expected to increase by a factor of approximately 5.

The possibility of using the existing AD ring as a muon accumulator for a “baby” neutrino factory to measure low-energy neutrino cross section was studied $`^\mathrm{?}`$. The interesting result was that these muons are already accumulated in the present antiproton running mode, and thus a neutrino beam is already existing there. Unfortunately, quantitative estimate showed that obtaining a sufficient number of stored muons in parasitic mode is incompatible with the present setup of the running AD experiments.

## 8 Conclusions

In the next years, CERN will focus on building and operating LHC. However, a large community is eager to maintain an active neutrino physics program. The CNGS long-baseline beam will start operation in spring 2005; the OPERA detector is already fully approved and under construction; a first 600 ton ICARUS module has already bee built and tested, and a proposal for a factor 5 mass increase is under approval. For the future, HARP is studying hadron production in the region of interest of present and future neutrino beams, neutrino factories and atmospheric neutrinos; there is an active group studying the possibility of a second-generation super-beam (possibly in conjunction with a beta-beam), and trying to make the first step towards a European neutrino factory for the post-LHC period.

## References


text:
# Néel order in doped quasi one-dimensional antiferromagnets

On leave from \]Canadian Institute for Advanced Research and Department of Physics and Astronomy, University of British Columbia, Vancouver, BC, Canada, V6T 1Z1

(March 29, 2002. Last change: )

## Abstract

We study the Néel temperature of quasi one-dimensional S=1/2 antiferromagnets containing non-magnetic impurities. We first consider the temperature dependence of the staggered susceptibility of finite chains with open boundary conditions, which shows an interesting difference for even and odd length chains. We then use a mean field theory treatment to incorporate the three dimensional inter-chain couplings. The resulting Néel temperature shows a pronounced drop as a function of doping by up to a factor of 5.

The study of doped low-dimensional antiferromagnets has been a very active field since the discovery of high-Tc superconductivity. A particularly simple form of doping results from replacing some magnetic Cu ions by non-magnetic ions like Zn. In this case the system is well described by the Heisenberg model with some spins removed from a regular lattice. This problem has been quite extensively studied both theoretically and experimentally in the quasi-two-dimensional case. Recent Monte Carlo simulations have shown convincingly that the zero temperature 2 dimensional system remains Néel ordered for impurity concentrations, $`p`$ up to the classical percolation threshold, ($`p_c.407`$, on the square lattice) Kato ; Sandvik . An analytic approach has been developed based on spin-wave theory and the T-matrix approximation, valid at impurity concentrations well below percolation, and extended to include weak inter-plane couplings Chernyshev . Recent experiments on La2Cu1-x(Zn,Mg)xO4 Vajik  are consistent with the $`T=0`$ critical concentration corresponding to classical percolation, and agree in detail, at lower impurity concentrations, with the analytic theory.

Here we study the effect of doping on three dimensional ordering in spin-1/2 chain compounds where the exchange interaction along the chains $`J`$ is much stronger than the inter-chain coupling $`J^{}`$. Before doping, the Hamiltonian is

$$H=\underset{j,\stackrel{}{y}}{}\left(J\stackrel{}{S}_{j,\stackrel{}{y}}\stackrel{}{S}_{j+1,\stackrel{}{y}}+\underset{\stackrel{}{\delta }}{}J^{}\stackrel{}{S}_{j,\stackrel{}{y}}\stackrel{}{S}_{j,\stackrel{}{y}+\stackrel{}{\delta }}\right),$$
(1)
where $`J`$ is the site-index along the chains and $`\stackrel{}{\delta }`$ are the vectors to neighboring chains. The chain lattice spacing has been set to unity. Randomly removing some of the spins breaks the chains up into finite segments with open boundary conditions, which are still weakly coupled to neighboring chains. This model describes Zn doped Sr2CuO3, for example. For the pure system a standard method to study the Néel temperature for weakly coupled chains is to first determine the staggered susceptibility of the one-dimensional chains, $`\chi _1(T)`$. If we then treat the inter-chain couplings in mean field theory MFT  we obtain the condition which determines the Néel temperature

$$zJ^{}\chi _1(T_N)=1,$$
(2)
where $`z`$ is the number of neighboring chains from the sum over $`\stackrel{}{\delta }`$ in Eq. (1). Since at low $`T`$, $`\chi _1(T)`$ diverges as $`1/T`$, this predicts $`T_NJ^{}`$, so that Néel order is predicted to occur for arbitrarily weak inter-chain coupling.

In this paper we extend this approach to the doped system by calculating the staggered susceptibility of chains with arbitrary length $`L`$ to find an average value of $`\chi _1`$ as a function of temperature $`T`$. This type of mean field treatment of inter-plane couplings in doped samples was used to study the Néel temperature of quasi-two-dimensional antiferromagnets in Chernyshev . This method can be carried out much more accurately in the quasi-one-dimensional case studied here because an analytic expression for the staggered susceptibility of finite chains can be found, which by itself yields rather interesting results, exhibiting very different behavior for even and odd length chains. Eq. (2) corresponds to approximating the interchain interactions as simply providing a staggered field of fixed magnitude, acting on a given chain. This approximation results from averaging over both quantum fluctuations and impurity locations on neighboring chains. We expect it to become more reliable when the average chain length $`\overline{L}`$ and $`z`$ (i.e. the lattice dimension) increases. Clearly this approximation must break down at large impurity doping $`p=1/\overline{L}`$, before the percolation threshold is reached ($`p_c69.8\%`$ for a three dimensional simple cubic lattice). In lower dimensions this approach becomes more questionable since the percolation threshold is reached earlier and the number of neighbors is lower, while in higher dimensions this method may become exact as $`z\mathrm{}`$ and valid for all doping levels since $`p_c1`$.

The staggered susceptibility per unit length of a finite chain of length $`L`$ with open boundary conditions at finite temperature $`T=1/\beta `$ is

$$\chi _1(L,T)\frac{1}{L}_0^\beta 𝑑\tau \underset{j,k=1}{\overset{L}{}}(1)^{jk}S_j^z(\tau )S_k^z(0).$$
(3)
In order to find a reliable average we need to determine $`\chi _1`$ for a large range of temperatures and lengths for which we use both bosonization techniques and numerical Monte Carlo simulations. Note that here we measure the staggered response to a staggered field, not to be confused with the staggered response to a uniform field impurity .

In order to calculate $`\chi _1`$ as a function of temperature we now go to the continuum limit and use the field theory treatment which is correct in the asymptotic low $`T`$, large $`L`$ limit review . The spin operators are then described in terms of a boson field, $`\varphi `$,

$$S_j^z\frac{_x\varphi }{\sqrt{2\pi }}+C(1)^j\mathrm{cos}\sqrt{2\pi }\varphi ,$$
(4)
where $`C`$ is a parameter which will be discussed in more detail below. The boson field $`\varphi `$ is described by a free massless relativistic Hamiltonian review  up to a marginally irrelevant interaction which gives rise to logarithmic corrections as we will see later. We normalize the operator $`\mathrm{cos}\sqrt{2\pi }\varphi `$ so that its $`T=0`$, $`L=\mathrm{}`$, equal time correlation function decays with distance as $`1/2|r|`$. In the sum of Eq. (3) we can neglect all rapidly oscillating parts so that only the second term in Eq. (4) will be kept in the alternating spin-spin correlation function

$$G(x,y,\tau )=C^2\mathrm{cos}\sqrt{2\pi }\varphi (x,i\tau )\mathrm{cos}\sqrt{2\pi }\varphi (y,0),$$
(5)
so that Eq. (3) becomes

$$\chi _1\frac{1}{L}_0^\beta 𝑑\tau _0^L𝑑x_0^L𝑑yG(x,y,\tau ).$$
(6)
To calculate the correlation function we use the mode expansion of the boson for a finite chain with open boundary conditions ourPRB

$$\varphi (x,t)=\sqrt{\frac{\pi }{8}}+\sqrt{2\pi }S^z\frac{x}{L}+\varphi _>(x,t),$$
(7)
where

$$\varphi _>(x,t)\underset{n=1}{\overset{\mathrm{}}{}}\frac{1}{\sqrt{\pi n}}\mathrm{sin}\frac{\pi nx}{L}(e^{i\pi nvt/L}a_n+h.c.)$$
(8)
contains the ordinary boson modes $`a_n`$ and the “zero mode” eigenvalue $`S^z`$ corresponds to the z-component of the total spin of the chain, which takes integer values for even lengths $`L`$ and half-integer values for odd $`L`$. The spin wave velocity is given by $`v=\pi J/2`$.

Before considering the case of arbitrary $`T`$ and $`L`$, it is interesting to consider the limit $`T0`$ with $`L`$ held fixed. In this limit, upon inserting a complete set of states, $`\chi _1\frac{1}{LT}|0|S_{\mathrm{alt}}^z|0|^2`$ will be dominated by the groundstate $`|0`$, where $`S_{\mathrm{alt}}^z_{j=1}^L(1)^{j+1}S_j^z`$. Using Eq. (7) we can directly find the local staggered magnetization of the lowest energy state in any sector with a given $`S^z`$

$`S^z(x)`$ $``$ $`C(1)^x\mathrm{cos}\sqrt{2\pi }\varphi (x)`$ (9)
$`=`$ $`C(1)^x{\displaystyle \frac{\mathrm{sin}(2\pi S^zx/L)}{\sqrt{(2L/\pi )\mathrm{sin}(\pi x/L)}}}.`$
For $`L`$ even $`S^z=0`$ in the groundstate so this gives zero $`LT\chi _10`$. However, for $`L`$ odd $`S^z=\pm 1/2`$ in the groundstates, giving

$$\pm |S^z(x)|\pm \pm C(1)^x\sqrt{\frac{\pi }{2L}\mathrm{sin}\frac{\pi x}{L}},$$
(10)
which upon integrating over $`x`$ gives $`S_{\mathrm{alt}}^z\sqrt{L}`$ and therefore $`\chi _11/T`$. This divergence is in sharp contrast to the even case. Interestingly Eq. (10) indicates a maximum response in the center of the chain which agrees with numerical results laukamp ; long  and is reminiscent of the square-root increase of the staggered response to a uniform field with the distance from the open ends impurity . It is interesting to note that our finding $`S_{\mathrm{alt}}^z\sqrt{L}`$ for a spin chain corresponds to an intermediate result between a Néel state with $`S_{\mathrm{alt}}^z=\pm L/2`$ and a nearest neighbor dimer state with one unpaired spin $`S_{\mathrm{alt}}^z=\pm 1/2`$.

We now consider the case of general $`L`$ and $`T`$ using the field theory approach. The correlation function can then be written as

$`G(x,y,\tau )={\displaystyle \frac{C^2}{2}}(e^{i2\pi S^z(xy)/L}e^{i\sqrt{2\pi }(\varphi _>(x,i\tau )\varphi _>(y,0))}`$
$`e^{i2\pi S^z(x+y)/L}e^{i\sqrt{2\pi }(\varphi _>(x,i\tau )+\varphi _>(y,0))}).`$ (11)
Upon using the cumulant theorem for boson modes $`e^A=e^{A^2/2}`$ we can determine the correlation function at any finite temperature and length by following the analogous calculations in Refs. mattsson  and EMK . Using the shorthand notation $`u=\pi \frac{xyiv\tau }{2L}`$, $`\overline{u}=\pi \frac{xy+iv\tau }{2L}`$, $`w=\pi \frac{x+y+iv\tau }{2L}`$, and $`\overline{w}=\pi \frac{x+yiv\tau }{2L}`$ we find

$`G(x,y,\tau )={\displaystyle \frac{\pi C^2}{4L}}{\displaystyle \frac{_x\theta _1(0,e^\gamma )}{\sqrt{\theta _1(w+u,e^\gamma )\theta _1(w\overline{u},e^\gamma )}}}`$
$`\times [B(u+\overline{u},e^{2\gamma })\sqrt{{\displaystyle \frac{\theta _1(w,e^\gamma )\theta _1(\overline{w},e^\gamma )}{\theta _1(u,e^\gamma )\theta _1(\overline{u},e^\gamma )}}}`$ (12)
$`B(w+\overline{w},e^{2\gamma })\sqrt{{\displaystyle \frac{\theta _1(u,e^\gamma )\theta _1(\overline{u},e^\gamma )}{\theta _1(w,e^\gamma )\theta _1(\overline{w},e^\gamma )}}}],`$
where $`\theta _1`$ is the elliptic theta function of the first kind GR . The parameter $`\gamma =\frac{v\pi }{2LT}`$ gives the spacing in the finite size energy spectrum in relation to the temperature. The contribution $`B(x)`$ from the zero modes is given by

$$B(z,e^{2\gamma })\frac{\underset{S^z}{}e^{2\gamma (S^z)^2+2iS^zz}}{_{S^z}e^{2\gamma (S^z)^2}}=\frac{\theta (z,e^{2\gamma )}}{\theta (0,e^{2\gamma })},$$
(13)
where $`\theta `$ is the elliptic theta function of the second kind for odd chains $`\theta =\theta _2`$, while it is the elliptic theta function of the third kind for even chains $`\theta =\theta _3`$. Remarkably, the correlation functions in the continuum limit in Eq. (12) therefore retain information about the underlying lattice and explicitly depend on the parity of $`L`$. This result requires the explicit use of the zero modes in the mode expansion mattsson ; EMK . The difference arises because of the different set of eigenvalues of $`S^z`$: integer and half-integer for even and odd length chains, respectively.

At this point we may rescale all the variables of integration in Eq. (6) by $`L`$ (or alternatively $`T`$) to express $`\chi _1`$ in terms of a universal function of the dimensionless variable $`LT/v`$.

$$\chi _1=C^2f(LT/v)/T$$
(14)
In the thermodynamic limit $`LT/v\mathrm{}`$, we can use the asymptotic behavior of the $`\theta `$ functions GR  as was done in a related calculation in mattsson ; EMK  for $`e^\gamma 1`$. In this case we can combine the two terms of $`G(x,y,\tau )`$ in Eq. (12) into one, giving the known finite temperature correlation functions impurity . This results in the well-known $`1/T`$ behavior benzoate

$$\chi _1\stackrel{\gamma 0}{}\frac{C^2}{4T}\frac{\mathrm{\Gamma }^2(1/4)}{\mathrm{\Gamma }^2(3/4)}2.18844C^2/T$$
(15)
As expected there is no difference between even and odd length chains in the limit of $`LT/v\mathrm{}`$ in Eq. (15).

In the opposite limit of zero temperature and finite length $`LT/v0`$, however, we find a qualitative difference for even and odd chains. Again using asymptotic limits of $`\theta `$ functions as $`e^\gamma 0`$, we now find

$$G(x,y,\tau )\frac{\pi C^2}{4L}\sqrt{\frac{\mathrm{sin}(w+u)\mathrm{sin}(w\overline{u})}{\mathrm{sin}(u)\mathrm{sin}(\overline{u})\mathrm{sin}(w)\mathrm{sin}(\overline{w})}}\times \{\begin{array}{ccc}1,\hfill & & \text{L even}\hfill \\ & & \\ \mathrm{cosh}(\frac{\pi v\tau }{L}),\hfill & & \text{L odd}\hfill \end{array}$$
(16)
Since for odd $`L`$ the correlation function $`G(x,y,\tau )`$ approaches a constant as $`\tau \mathrm{}`$ we get a divergence of $`\chi _1`$ in Eq. (6) with $`1/T`$ for low temperatures, while for even $`L`$ the integral is proportional to $`L`$ resulting in

$$\chi _1\stackrel{\gamma \mathrm{}}{}\{\begin{array}{ccc}0.92905C^2L/J,\hfill & & \text{L even}\hfill \\ & & \\ \frac{8C^2}{\pi T}E^2(\frac{\pi }{4},\sqrt{2})0.913893C^2/T,\hfill & & \text{L odd}\hfill \end{array}$$
(17)
where $`E`$ is the elliptic integral of the second kind GR , which can also be derived from Eq. (10). Note that the scaling behavior with $`1/T`$ in the two limits $`LT/v1`$ for odd $`L`$ in Eq. (17) and $`LT/v1`$ in Eq. (15) is the same, up to a factor of about 2. This is of crucial significance for the behavior of the Néel temperature of the doped quasi-one-dimensional system as we shall see.

So far we have ignored the marginally irrelevant interaction mentioned earlier. Its effect on the staggered susceptibility at finite $`T`$ but $`L\mathrm{}`$ is well-known. It corresponds to replacing the constant $`C^2`$ by a slowly varying function of $`T`$

$$C^2=2\sqrt{\mathrm{ln}(aJ/T)/(2\pi )^3},$$
(18)
where $`a`$ is a dimensionless constant exact ; benzoate . From fitting our susceptibility data, we find $`a23`$, which gives $`C^20.33\pm 0.07`$ for $`0.001T/J0.2`$. A finite length $`L`$ together with open boundary conditions leads to more complicated logarithmic corrections which may in general involve a different exponent near the boundary Qin . Hence, the general expression of the logarithmic correction at finite $`L`$ is not known, but we expect that $`C^20.33\pm 0.07`$ remains approximately correct for the relevant length scales studied here.

The full behavior of $`\chi _1`$ as a function of the scaling variable $`LT`$ is shown in Fig. (1) compared to numerical Monte Carlo data after dividing by the logarithmic factor in Eq. (18). There are no adjustable parameters for this fitting except for the constant inside the logarithm $`a23`$ and all numerical points from the Monte Carlo simulations fall close to this universal line for larger values of $`LT`$ as well (not shown). The errors are less than the size of the symbols in the figure so that the deviations are due to higher order corrections. For the simulations we chose different values of $`20L120`$ and $`0.025T/J0.2`$. For $`LT4J`$ the even and odd cases are virtually indistinguishable, but as $`LT0`$ there is a clear difference in the behavior.

We now want to determine the Néel temperature by using the mean field treatment of inter-chain couplings in Eq. (2), where $`\chi _1`$ now represents the one-dimensional susceptibility averaged over chain lengths with the probability distribution, $`P(L)=e^{L/\overline{L}}/\overline{L}`$, where $`\overline{L}`$ is the average chain length, corresponding to an impurity concentration of $`p=1/\overline{L}`$. Because of the scaling form in Eq. (14) it is straightforward to show that the mean field condition in Eq. (2) can be written as

$$T_N=C^2zJ^{}g(T_N\overline{L})$$
(19)
where $`g(T_N\overline{L})=𝑑yye^yf(T_N\overline{L}y)`$ is the average of the scaling function $`f`$ in Fig. (1) and Eq. (14) and $`C^2`$ is given in Eq. (18) with $`T=T_N`$. We see that the solutions for the Néel temperature $`T_N/J^{}`$ in Eq. (19) are functions of the scaling variable $`\overline{L}J^{}`$ as shown in Fig. (2) for $`z=4`$ compared to the results from Monte Carlo simulations. The marginal operator leads to weak logarithmic corrections to this scaling behavior, which leaves the shape of the curve largely unchanged for different $`J^{}`$, and only shifts it up by a few percent as $`J^{}`$ is lowered. Therefore we can make a nearly universal quantitative prediction for all doping levels and coupling strengths.

The Néel temperature is strongly affected by doping when the impurity concentration, $`1/\overline{L}J^{}/J`$ and may drop by as much as a factor of 5, although it remains finite. This is because the scaled average staggered susceptibility $`g(T_N\overline{L})`$ of odd chains is finite as $`\overline{L}0`$ so that Eq. (19) can always be fulfilled for a positive $`T_N`$. If, however, only even chains were allowed in the system, no non-zero solution would exist for $`\overline{L}0.6J/zJ^{}`$. As mentioned above, we expect this result to break down at larger impurity doping as the percolation threshold is approached and Néel order disappears.

###### Acknowledgements.

I.A. would like to thank Antonio Castro-Neto and Anders Sandvik for very helpful conversations and Kenji Kojima for interesting him in this subject. This research was supported in part by the Swedish Research Council (SE) and NSERC of Canada (IA and MDPH).


text:
# Monte Carlo Simulations of Vector Spin Glasses at Low Temperatures

## Results

Figures 1 and 2 show data222I present data for $`\left|q\right|`$ since for the gauge glass $`q`$. for $`P(\left|q\right|)`$ and $`P(q_l)`$ at $`T=0.050`$, well below $`T_c0.45`$  for the 3D gauge glass.

There is a clear peak in $`P(\left|q\right|)`$ for large $`\left|q\right|`$ as well as a tail at small $`\left|q\right|`$. The weight in the tail does not decrease with increasing $`L`$, as is expected in the standard interpretations of the droplet theory. If anything, the weight increases for larger sizes. There is some evidence that $`P(\left|q\right|)`$ stays flat down to smaller $`\left|q\right|`$ for larger $`L`$, although the range of sizes is too small to make a reliable extrapolation.

As with the distribution of $`\left|q\right|`$, there is a pronounced peak at large $`q_l`$-values in the distribution of $`P(q_l)`$ for the 3D gauge glass. Note also the appearance of a smaller peak at smaller $`q_l`$ for larger system sizes, as predicted by RSB.

The width of the distribution decreases with increasing system size. This can be seen in Figure 3 where I plot the variance of the link overlap as a function of system size $`L`$. The data is consistent with a power law decrease ($`a=0`$ in Eq. 1) where the (presumably effective) exponent varies slightly with $`T`$. Extrapolating to $`T=0`$ gives $`\mu _l\theta ^{}+2(dd_s)=0.501\pm 0.04`$. Assuming $`\theta ^{}0`$ I find $`dd_s=0.25\pm 0.02`$, implying that for the 3D gauge glass system-size excitations have a fractal surface in the thermodynamic limit as predicted by the droplet picture.

Figures 4 and 5 show data for $`P(q)`$ and $`P(q_l)`$ for $`T=0.20`$ (to be compared with $`T_c0.95`$ ) for the 4D $`XY`$ spin glass. Again one sees a large peak for large $`q`$ and $`q_l`$ values. The data for $`P(q_l)`$ exhibits a hint of a shoulder for smaller values of $`q_l`$.

The width of the distribution decreases with increasing system size. This is demonstrated in Fig. 6 where I show the variance of $`q_l`$ against system size $`L`$ for several low temperatures. There is some curvature in the data for $`\mathrm{Var}(q_l)`$ so first I attempt a three-parameter fit to Eq. 1. As there are the same number of data points as variables, I cannot assign fitting probabilities to the fits but from the data I find $`a=0.00100`$, $`0.00087`$, $`0.00073`$ and $`0.00036`$ for $`T=0.200`$, $`0.247`$, $`0.305`$ and $`0.420`$, respectively.

I also attempt a power law fit to Eq. 1 setting $`a=0`$. The quality of the fits is poor with probabilities $`Q=5.0\times 10^2`$, $`3.6\times 10^3`$, $`2.9\times 10^6`$ and $`6.0\times 10^8`$ for $`T=0.200`$, $`0.247`$, $`0.305`$ and $`0.42`$, respectively333The complete set of fitting parameters for both fitting functions presented in Eq. 1 can be found in Ref. .. The effective exponent $`\mu _l`$ is found to vary with temperature. Extrapolating to $`T=0`$, I obtain $`\mu _l\theta ^{}+2(dd_s)=0.294\pm 0.073`$. Assuming $`\theta ^{}0`$, one obtains $`dd_s=0.147\pm 0.036`$.

## Conclusions

To conclude, I have studied the properties of the 3D gauge glass and the 4D $`XY`$ spin glass at low temperatures. For both models, the order parameter distribution $`P(q)`$ has, in addition to a peak, a tail that seems to extend for smaller values of $`q`$ and whose height seems to persist as the system size increases. This interpretation of the data is compatible with the RSB picture or the KMPY scenario. The range of lattice sizes is very small, however, so this conclusion can be considered at most tentative.

For the gauge glass, the variance of the link overlap indicates that the surface of low-energy large-scale excitations is fractal with $`dd_s=0.25\pm 0.02`$ in agreement with the KMPY scenario. The log-log plot for $`\mathrm{Var}(q_l)`$ for the $`XY`$ spin glass shows curvature, possibly indicating a non-zero value in the thermodynamic limit, a result compatible with RSB. Due to the small range of system sizes, however, I cannot rule out the possibility that $`\mathrm{Var}(q_l)0`$ at large $`L`$, which is compatible with the KMPY scenario or droplet picture. The effects of vortices in the spin glass phase still remain to be understood. It would be useful to look more carefully at the nature of the large-scale low-energy excitations to see whether they correspond to gradual orientations in the spin directions or whether vortices play a role.

I would like to thank A. P. Young for useful discussions. This work was supported by the National Science Foundation under grant DMR 0086287 and a Campus Laboratory Collaboration (CLC).