Tomás Díaz

Imfd Chile

Federico Olmedo
email: folmedo@dcc.uchile.cl

Éric Tanter
email: etanter@dcc.uchile.cl

A Mechanized Formalization of GraphQL

Keywords: CCS Concepts, Information systems → Web services, Query languages, • Theory of computation → Semantics and reasoning GraphQL, mechanized metatheory, Coq

GraphQL is a novel language for specifying and querying web APIs, allowing clients to flexibly and efficiently retrieve data of interest. The GraphQL language specification is unfortunately only available in prose, making it hard to develop robust formal results for this language. Recently, Hartig and Pérez proposed a formal semantics for GraphQL in order to study the complexity of GraphQL queries. The semantics is however not mechanized and leaves certain key aspects unverified. We present GraphCoQL, the first mechanized formalization of GraphQL, developed in the Coq proof assistant. GraphCoQL covers the schema definition DSL, query definitions, validation of both schema and queries, as well as the semantics of queries over a graph data model. We illustrate the application of GraphCoQL by formalizing the key query transformation and interpretation techniques of Hartig and Pérez, and proving them correct, after addressing some imprecisions and minor issues. We hope that GraphCoQL can serve as a solid formal baseline for both language design and verification efforts for GraphQL.

Introduction

GraphQL is an increasingly popular language to define interfaces and queries to data services. Originally developed internally by Facebook as an alternative to RESTful Web Services [START_REF] Richardson | RESTful Web APIs: Services for a Changing World[END_REF], GraphQL was made public in 2015, along with a reference implementation 1 and a specification-both of which have naturally evolved [START_REF]GraphQL specification[END_REF]. Since early 2019, as a result of its successful adoption by major players in industry, GraphQL is driven by an independent foundation 2 . The key novelty compared to traditional REST-based services is that tailored queries can be formulated directly by clients, allowing a very precise selection of which data ought to be sent back as response. This supports a much more flexible and efficient interaction model for clients of services, who do not need to gather results of multiple queries on their own, possibly wasting bandwidth with unnecessary data.

The official GraphQL specification, called Spec hereafter, covers the definition of interfaces, the query language, and the validation processes, among other aspects. The specification undergoes regular revisions by an open working group, which discusses extensions and improvements, as well as addressing specification ambiguities. Indeed, as often happens, the Spec is an informal specification written in natural language. Considering the actual vibrancy of the GraphQL community, sustained by several implementations in a variety of programming languages and underlying technologies, having a formal specification ought to bring some welcome clarity for all actors.

Recently, Hartig and Pérez [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF] proposed the first (and so far only) formalization of GraphQL, called H&P hereafter. H&P is a formalization "on paper" that was used to prove complexity boundaries for GraphQL queries. Having a mechanized formalization would present many additional benefits, such as potentially providing a faithful reference implementation, and serving as a solid basis to prove formal results about the GraphQL semantics.

For instance, the complexity results of Hartig and Pérez rely on two techniques: a) transforming queries to equivalent queries in some normal form and, b) interpreting queries in a simplified but equivalent definition of the semantics. However, Hartig and Pérez do not provide an algorithmic definition of query normalization, let alone proving it correct and semantics preserving; nor do they prove that the simplified semantics is equivalent to the original one when applied to normalized queries.

This work presents the first mechanized formalization of GraphQL, carried out in the Coq proof assistant [START_REF]The Coq proof assistant[END_REF], called GraphCoQL (|graef•co•k e l|). GraphCoQL currently includes the definition of the Schema DSL, query definition, schema and query validation, and the semantics of queries, defined over a graph data model as in H&P ( §3).

As well as precisely capturing the semantics of GraphQL, GraphCoQL makes it possible to specify and prove the correctness of query transformations, as well as other extensions and optimizations made to the language and its algorithms. We illustrate this by studying H&P's notion of query normalization ( §4). Specifically, we define an algorithmic presentation of normalization, which we then prove correct and semantics preserving. We also formalize and prove the equivalence between the original query evaluation semantics and the simplified semantics used by H&P for normalized queries. In the process, we address some imprecisions and minor issues that Coq led us to uncover.

We discuss the limitations and validation of GraphCoQL, including its trustworthiness, in §5. We hope that GraphCoQL can serve as a starting point for a formal specification of GraphQL from which reference implementations can be extracted. Although we have not yet experimented with extraction, GraphCoQL facilitates this vision by relying on boolean reflection as much as possible.

We briefly introduce GraphQL in §2. We discuss related work in §6 and conclude in §7. The fundamental challenge of the Coq formalization of GraphQL in comparison to similar formalization efforts (e.g. [START_REF] Auerbach | Q*cert: A platform for implementing and verifying query compilers[END_REF][START_REF] Benzaken | A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF][START_REF] Benzaken | Certifying standard and stratified Datalog inference engines in Ssreflect[END_REF]) resides in the nonstructural nature of most definitions related to GraphQL queries. In particular, as we will see, both query semantics and query normalization are defined by well-founded induction on a notion of query size ( § 3.3).

GraphCoQL and the results presented in this paper have been developed in Coq v.8.9.1 and are available online on GitHub 3 . GraphCoQL extensively uses the Mathematical Components [START_REF] Mahboubi | Mathematical components[END_REF], Ssreflect [START_REF] Gonthier | A small scale reflection extension for the Coq system[END_REF] and Eqations [START_REF] Sozeau | Equations reloaded: High-level dependently-typed functional programming and proving in Coq[END_REF] libraries. This work is based on the latest GraphQL specifications, dated June 2018 [START_REF]GraphQL specification[END_REF].

A Brief Introduction to GraphQL

We briefly introduce GraphQL by means of the running example that we use in the rest of the presentation. The example is about a fictional dataset Artists, containing information about artists and the artworks they have been involved in, particularly movies and books. We discuss the dataset schema, the underlying data model and the query evaluation. GraphQL schema. The first step when defining a GraphQL API is to define the service's schema, describing the type system and its capabilities. The type system describes how data is structured and precisely what can be requested and received. A schema consists of a set of types, which can have declared fields. Only fields that are part of such type definitions can be accessed via a GraphQL query. In contrast to traditional data management systems, field accesses in GraphQL are handled by the backend via user-defined functions (called resolvers).

Figure 1 depicts the schema for the Artists dataset, which contains artists and their artworks. The definition is done using the GraphQL Schema Definition Language. The object type Artist declares three fields: an identifier, a name, and a list of artworks in which the artist has participated. The list of artworks is declared of type [Artwork]. Note that the field may receive an argument, role, which can be used to select only those artworks for which the author plays a certain role, such as being the director. Possible roles are modeled with the enum type Role, containing three scalar values. An Artwork is a disjoint union of fictional movies, animated movies and books. Both fictional and animated movies are defined as object types, namely Fiction and Animation, implementing the same interface type Movie. 4An object implementing an interface may add more fields, such as the field style in the type Animation. To model the animation style, we use the enum type Style containing Finally, GraphQL requires that the schema includes a query type, which, for convenience, we call Query. This type is the same as a regular object type 5 , however it is special in the sense that it represents the entry point from where users have to start querying the API and explore the dataset. In this API, a user may only access the Artists dataset by requesting a particular artist or movie (with a given id).

Graph data model. The complete Artists dataset can be represented with the graph in Figure 2. Nodes in the graph represent object values as defined in the schema; they are tagged with the corresponding object type and include a set of properties (key-value pairs) that describe the object's content. Edges between nodes are accompanied with a label that indicates the relationship they establish. For instance, the central node in the graph represents an object of type Artist. The node properties say that the artist is called Tom Hanks and his id is 1000. The node's outgoing edges indicate that the artist performed as an actor in the movies Forrest Gump and Toy Story (represented by the leftmost and rightmost nodes, respectively), and that he was the author of book Uncommon Type (represented by the bottommost node).

GraphQL query and response. With the schema and data defined, it is possible to query the service. As previously hinted, GraphQL queries are simply requests over the fields of types defined in the schema. They have a tree structure, similar to JSON, which follows the fields and relations established between the types in the type system. 5 The query type can e.g. have any custom name and even implement interfaces. To illustrate this, we define the query in Figure 3. Intuitively, the query is asking for the name of the artist with id 1000, as well as the title and some additional information of the artworks where he performed as an actor. The request starts with the keyword query, which allows proceeding with any of (and as many as) the dataset entry points declared by the query type Query. Concretely, we select field artist and include the value of argument id to indicate which artist we want to retrieve. Because the field is of an object type, namely Artist, we can continue making requests over the fields of this type, precisely specifying the desired information about the fetched artist. In this case, the query continues with the field name and the field artworks. The argument role of field artworks is used to restrict the search to those artworks where the artist performed as an actor. For such artworks, we request on one hand their title and on the other hand further information which depends on the concrete kind of artwork. (Recall that union type Artwork is composed by the object types Book, Fiction and Animation). For animated movies, we request the animation style, while for fictional movies, we request the year of release; for books, we require no related information. This is achieved by the pair of selections ... on Animation { style } and ... on Fiction { releaseYear:year }, called inline fragments. In the latter, the field selection releaseYear:year introduces a field alias, indicating that in the response the original field year should be renamed to releaseYear. Field aliasings are particularly relevant when validating and transforming queries, and originated one of the imprecisions uncovered in H&P's definitions (see § 4.5).

This query is then evaluated, resulting in the response depicted on the right of the node with type Query, the field artist(id:1000) indicates that we are looking for an adjacent node that can be reached after traversing an edge whose label matches the field and id. The first step then takes the evaluation process to the central node, of type Artist. From there, it accesses the value of the node's property matching the field name and then continues navigating the graph in search of the artist's artworks.

To summarize, in order to define a GraphQL service it is necessary to define the schema that describes the service's type system, to which both the underlying dataset and the queries must adhere. GraphQL queries consist of selections over fields and types defined in the schema, and their responses closely match the queries tree structure.

GraphCoQL

In this section we describe our formalization of GraphQL in Coq. We start by defining a schema and its properties ( §3.1), then the graph data model ( §3.2), and finally present queries ( §3.3) and their semantics ( §3.4). We highlight key connections with the Spec [START_REF]GraphQL specification[END_REF] and H&P [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF] along the way, and end this section with a discussion of various design considerations ( §3.5).

Schema

We formalize schemas and type definitions following the Spec. A schema is represented as a record, containing a list of type definitions and a root query type that specifies the entry points to the dataset. A Name is simply a string, according to the Spec.

Record graphQLSchema := GraphQLSchema { query_type : Name; type_definitions : seq TypeDefinition }.

Schemas may also include additional root types for specifying mutations and subscriptions (cf. [16, §3.2.1]). These operations are, however, out of the scope of this work.

Type definitions in GraphCoQL closely follow the Spec, as depicted in Figure 4. A type may be a scalar type, an object type, which possibly implements a set of interfaces, an interface type, a union type or an enumeration type. Object and interface type definitions comprise a set of fields; union types are defined by a set of type names and enumeration types by a set of scalar values.

The mere syntax of schema and types does not ensure that only valid schemas are defined. For instance, one can build an object that implements scalar types or use a nonexistent type as the root query type. To avoid this problem, the Spec provides several validation rules (cf. [16, §3]). We refer to these rules as the well-formedness condition of a GraphQL schema: 6Definition 3.1. A GraphQL schema is well-formed if:

• its query root type (is defined and) is an object type,

• there are no duplicated type names, and • every type definition is well-formed.

In GraphCoQL, this is captured by the Boolean predicate below. The notion of well-formedness for type definitions requires e.g. that the members of union types are existent object types and that object and interface types contain at least one field. Note that the Spec syntactically requires certain sets of elements to be non-empty (see the grammar on the left of Figure 4). This requirement is not enforced at the level of a type definition in GraphCoQL, but is instead part of the well-formedness check. Full definitions can be found in our Coq development.

For convenience, we encapsulate schemas with their wellformedness proof in a single structure.

Record wfGraphQLSchema := WFGraphQLSchema { schema : graphQLSchema; _ : schema.(is_a_wf_schema); }.

Data Model

Following H&P, we adopt a data model based on graphs, where datasets are modeled as directed property graphs, with labeled edges and typed nodes. Nodes contain a type and a set of properties (key-value pairs) and edges contain single labels. Properties and labels may contain a list of arguments (key-value pairs). Values are either scalars or lists of values. Note that graphs are modeled using sequences-rather than sets-of edges. In our experience, this design decision led to a simpler formalization, as verifying edge unicity extrinsically is straightforward.

Intuitively, the dataset modeled by a GraphQL graph is built following a schema. However, the definition of GraphQL graph above is fully independent of any schema. To capture this relationship, we employ the following notion of conformance, partially based on H&P:

Definition 3.3. A GraphQL graph G conforms to a schema S if:
• the types of G root node and S query root coincide,

• every node of G conforms to S, and

• every edge of G conforms to S.

The conformance of nodes validates that a node's type is declared as an object type in the schema and that its properties conform. In turn, a property conforms if its key and arguments are defined in a field in the corresponding object type, and any value, either in an argument or the property's value, is valid w.r.t. the expected types described in the schema. For instance, if a field has type Float, the Spec dictates that a node property matching the field must have a value that represents a double-precision fractional value (cf. [16, §3.5.2]). To model this validation of values, we parameterize the Coq development with a Boolean predicate check_scalar : graphQLSchema → Name → Scalar → Bool.

The conformance of edges imposes some final natural restrictions on graphs. For instance, given an edge, it requires that the label match some field in the type of the source node, and that the type of the target node be compatible with the type of the matched field.

It is worth noting that, in accordance with the flexibility advocated by graph databases, the notion of conformance does not require that a graph contain full information about the represented objects. More precisely, a node need not provide values for all the fields in its type. For instance, in our running example in Figure 2, the bottommost node of type Book need not contain a property defining the book title.

With this in mind, the notion of conformance of a graph w.r.t. a schema is formalized as follows: Similarly to GraphQL schemas, we define a structure that encapsulates the notion of a conformed graph, containing a graph and a proof of its conformance to a particular schema.

Record conformedGraph (s : wfGraphQLSchema) :=

ConformedGraph { graph : graphQLGraph; _ : is_a_conforming_graph s graph check_scalar }.

Queries

To define queries we faithfully follow the Spec, as shown in Figure 5. A query consists of a list of selections, and can optionally be named. A selection σ can be a single field with arguments (f[α]), a field with arguments followed by a set of subselections (f[α]{σ }) or an inline fragment comprising a type condition and a set of subselections (... on t {σ }).

Fields can be aliased (a:f[α], a:f[α]{σ }). For notational simplicity, when a field selection contains an empty list of arguments, we omit it and simply write the field name. Intuitively, a query has a tree structure, where leaves correspond to fields of scalar types and inner nodes correspond to either fields of some object type or abstract type (i.e. an interface or union), or to inline fragments that condition when their subselections are evaluated.

Observe that the definition of queries in Figure 5 is not bound to any schema, thus requiring a separate validation process to ensure that they adhere to a given schema. We introduce the notion of query conformance, based on a set of validation rules scattered throughout the Spec (cf. [16, §5]). The validity of queries depends on the validity of their selection sets, which in turn requires the notion of type in scope To illustrate this, consider the query to the right with two occurrences of field title. In the first occurrence, the field is requesting information about the Animation type, while in the second it is requesting information about the Fiction type. The distinction is important because some field selections might be valid in some contexts but not in others. For instance, this is the case of field style, which is valid in the scope of the Animation type but it is invalid in the scope of the Fiction type, as the Fiction type does not contain any such field. Now that we have clarified the notion of type in scope, we define the notion of conformance for selection sets. Definition 3.4. A GraphQL selection set σ conforms to a schema S over a type in scope ts if:

• every selection in σ is well-formed w.r.t ts, and • any two field selections in σ are type-compatible and renaming-consistent. 7 The first rule ensures that every selection is well-formed on its own, w.r.t. the type in scope. This requirement depends on the kind of selection. For instance, if the selection is a field, the rule checks that the field is part of the type in scope and that its arguments are correctly provided; if the selection is an inline fragment, then the type condition must share at least one subtype with the type in scope. This rule also includes validating the values used in arguments, similarly to the case of graphs.

In the second rule, the type-compatibility requirement forbids the selection set to produce results of different types for the same key; e.g. the following query 7 In the Spec, these two notions roughly correspond to SameResponseShape and FieldsInSetCanMerge, respectively (cf. [16, §5.3.2]). Formally, the definition of field type-compatibility is recursive. Two nested field selections are type-compatible if whenever they have the same response name, any two fields in the concatenation of their subselections (possibly reached traversing inline fragments) are also type-compatible. Two single field selections are always type-compatible, unless they have the same response name and different type.

Finally, the renaming-consistency condition ensures that fields with the same response name refer to the same piece of information. Consider, for instance, the following query: The query is considered invalid because the fields with response name title both refer to distinct pieces of information; the first occurrence refers to the field title of a Movie, while the second occurrence refers to the field style of an Animation.

Formally, two field selections are renaming-consistent if whenever they have the same response name and lie under types in scope with at least one common subtype, they have the same (actual) name, the same arguments and any two fields in the concatenation of their subselections (possibly reached traversing inline fragments) are also renamingconsistent. In the Spec, the last two rules are defined as a single validation rule (cf. [16, §5.3.2]). We chose to split them because it simplified both their implementation and reasoning about them. 8 With the notion of conformance for selection sets at hand, the notion of conformance for queries is straightforward: Definition 3.5. A GraphQL query φ conforms to a schema S if its selection set conforms to S over the query root type.

In GraphCoQL, this is captured by the following predicates: As a technical observation, most of our recursive definitions over selection sets are well-founded according to the following notion of size: Definition 3.6 ( [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF]). The size of a selection σ and selection set σ , noted |•|, is recursively defined as:

|f[α]| = |a:f[α]| = 1 |f[α] {σ }| = |a:f[α] {σ }| = |... on t {σ }| = 1 + |σ | |σ | = σ i ∈ σ |σ i |
8 GraphCoQL uses an optimized version of the algorithm in the Spec. Recently, a team at XING developed another optimized algorithm [START_REF] Xing | Overlapping fields can be merged fast[END_REF].

Semantics

Now we have all the prerequisites to define the semantics of GraphQL queries and their selection sets. We begin by briefly examining the responses generated by executing queries and then we give an informal description of the semantics, finishing with the formal definition.

Roughly speaking, a GraphQL response maps keys (field names) to response values. We model response values with a tree structure, similar to JSON. Concretely, a response value can be either a value in Scalar or the distinguished value null, an object mapping keys to other response values, or an array of response values. Full definition is provided in Figure 6.

As a first step to define the semantics of queries, we observe that it is not compositional, in the sense that the result of a sequence of selections is not obtained by simply concatenating the results of individual selections. Therefore, the evaluation function takes as input a (whole) selection set, rather than single selections.

Informally, the evaluation of a selection set represents a navigation over a graph, starting from the root node, traversing its edges and collecting data from its nodes. To build the response, the values in nodes are coerced into proper response values. If this coercion fails or the data requested by the selection set is not present in the graph, the evaluation function simply returns null.

This validating transformation from values within graph nodes into values within responses is captured by the function complete_value (cf. [16, §6.4.3]). To carry out the transformation the function relies on two auxiliary functions: coerce that coerces scalar values and check_scalar that checks whether the resulting values have the expected type according to the schema. 9With this in mind, we can now define the evaluation function of selection sets. Definition 3.7. Let G be a graph and σ a selection set, both conforming to a schema S. The evaluation σ u G of σ over graph G from node u ∈ nodes(G) is defined by the rules in Figure 7. The evaluation function is parametrized by a coercing function coerce : Scalar → Scalar and a value validation predicate check_scalar : graphQLSchema → Name → Scalar → Bool.

In order not to clutter the notation, we omit the underlying schema when defining σ u G in Figure 7. The schema is implicitly used e.g. when invoking function complete_value.

The definition starts with the base case of empty selection set [START_REF] Auerbach | Q*cert: A platform for implementing and verifying query compilers[END_REF], which results in an empty response. Single fields (2) correspond to accessing a node's property that matches the field name and using function complete_value to coerce and validate the requested value. This function is implemented by simply calling coerce and check_scalar.

Nested fields (3) represent a traversal to neighboring nodes: the evaluation function searches for nodes that are connected to the current node by an edge whose label matches the field name and then evaluates the subselections on these nodes. If the field has list type, there is no constraint on the number of such neighboring nodes to recursively continue the evaluation. On the contrary, if the field does not have list type, then there should be exactly one neighboring node to successfully continue the recursive evaluation on this node (the case of multiple neighboring nodes is discarded by the conformance assumption); if there is no neighbor, the result is considered null.

To avoid the duplication of responses, rules (2) and (3) handling the evaluation of fields ensure that within a selection set, fields with the same response name are evaluated only once. This is achieved by collecting and merging all fields in subsequent selections that have the same response name as the current field being evaluated (using auxiliary functions collect and merge) and removing these fields from subsequent selections (using auxiliary function filter), before they are evaluated. Finally, inline fragments (4) simply condition whether their subselections are evaluated (in the current node) or not. The decision is based on the fragment_type_applies predicate (cf. [16, §6.3.2]) that verifies whether the guard type matches the current node type or supertype thereof. 10For space reason, Figure 7 does not present aliased fields. They are evaluated the same way as unaliased fields, but differ in that the produced key-value pairs are renamed accordingly. Definition 3.8. Let G be a graph and φ a query, both conforming to a schema S. The result of evaluating φ over G is obtained by evaluating the selection set of φ from the root node of G, that is,

φ G = φ.selection_set G.root G .
In GraphCoQL we have: Definition execute_query (s : wfGraphQLSchema) (g : conformedGraph s check_scalar) (φ : query) := execute_selection_set s check_scalar g coerce g.(root) φ.(selection_set).

Design considerations and discussion

We now discuss some design considerations that manifested when developing GraphCoQL, in particular with respect to the two existing sources of information on GraphQL, namely the Spec and H&P.

Representation choices. The definition of schemas in H&P relies on defining sets of field names, types and values, and using a number of functions to relate the different elements. For example, the object types of the schema from Figure 1 are defined as the set O T = {Artist, Fiction, Animation, Book, Query} and their fields are defined with a function fields S : O T → 2 F , where F is a set of field names. In contrast, GraphCoQL uses a more data-structure centric approach, in which schemas are records. While H&P's approach simplifies many validation rules, our approach is closer to the schema definition language from the Spec (which did not exist yet when H&P was published). Another advantage of the approach we take is that it is closer to an actual implementation and hence the definitions could be directly extracted as a reference implementation. The same observation holds for the data model.

Schema validation. The definition of well-formedness of a schema given by H&P does not capture all the validation rules established by the Spec. In particular, it does not properly account for arguments of implemented fields in objects implementing interfaces. A corrected version of H&P has been proposed recently by Hartig and Hidder [START_REF] Hartig | Defining schemas for property graphs by using the GraphQL schema definition language[END_REF], which coincides with both the Spec and GraphCoQL.

Data model. We observe that both H&P and GraphCoQL have a slightly limited graph model that does not entirely describe the universe of a GraphQL service: graphs cannot model nested lists, when the underlying type is an object or abstract type. 11 For instance, these semantics cannot account for a selection over a field whose type is

[[Artist]].
The underlying question is how to interpret such nested lists in a graph-based data model. The importance of this limitation in practice remains to be assessed. Recent empirical studies that analyze the structure of GraphQL schemas over a collection of industrial and open-source projects provide some insights such as the most common object types, which indeed do not have nested list types [START_REF] Kim | An empirical analysis of GraphQL API schemas in open code repositories and package registries[END_REF][START_REF] Wittern | An empirical study of GraphQL schemas[END_REF]. Regardless, we believe that while this limitation might turn out problematic for an extracted reference implementation of GraphQL, it should play little role in metatheoretical results, as those studied in §4.

Responses. The Spec only states that responses are a map from keys to values, but encourages the ordering of selections to be preserved (cf. [16, §7.2.2])-the similarity between query selections and responses being one of GraphQL's attraction for programmers. We embrace this recommendation: modeling of responses as trees allows us to preserve similarity w.r.t. selections and ordering of response values.

The downsides of this representation choice are possible duplication of response names, and access cost. We establish unicity of names by extrinsic proofs, and consider that the access cost is not of primary importance in this work.

Query semantics. The query semantics of GraphCoQL (Figure 7) is similar to the Spec in that it performs a collection of fields at the level of selections. In contrast, H&P adopt a different formulation in which collection is done at the level of responses, i.e. as a post-processing phase. Initially, we experimented with the H&P approach in order to be as close as possible to their formalization. However, the nonstructurally recursive nature of both the transformations and the post-processing function made reasoning about semantic equivalence of queries very hard. In contrast, we found that following the Spec approach made such reasoning in Coq much more convenient.

Finally, while the Spec presents the query evaluation semantics in two separate phases, first grouping fields by name and then evaluating each group, we define the whole query evaluation in a single pass. The technical reason is that following the Spec approach makes Eqations produce a reasoning principle for the query evaluation function that is too large and inconvenient to work with. With our presentation, the reasoning principle is more concise and adequate, due to a more localized handling of inline fragments.

Case Study: Normalization

To illustrate how GraphCoQL can be used to reason about query transformations, we study the normalization process proposed by Hartig and Pérez (H&P) [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF], which is fundamental for the complexity results they prove. These results are based on two premises: a) every query can be normalized to a semantically-equivalent query; b) on such queries, one can use a simplified evaluation function. For normalization, H&P provide a set of equivalence rules to establish the existence of a normal form. However they do not provide an algorithm for query normalization, let alone prove it correct and semantics preserving. Likewise, they do not prove the equivalence of the simplified semantics when applied to normalized queries.

In this section, we show how to define the property of being in normal form in GraphCoQL, define a normalization procedure, and prove it both correct and semantics preserving. Finally, we define the simplified semantics given by H&P, and prove it equivalent to the original semantics ( § 3.4) when applied to normalized queries. is_object_type checks whether the given type is an object type in the schema. get_possible_types get all object subtypes of the given type.

N ts (•) : seq Selection → seq Selection (1) N ts (•) = [•] (2) N ts (f[α] :: σ ) = f[α] :: N ts (filter(f, σ )) (3) N ts (f[α] {β} :: σ ) =          f[α] {N

Correctness and Semantic Preservation

We now establish two fundamental results about the normalization procedure. The first result states that the normalization procedure is correct in that it does indeed produce queries in normal form. The proof of the main lemma proceeds by well-founded induction over the size of the selection set and relies on some auxiliary lemmas about subtyping. Each of the two conditions (groundedness and non-redundancy) are established separately.

The second result states that the normalization procedure is semantics-preserving in that a normalized query has the same evaluation semantics as the original query from which it was derived. Formally, this requires proving that evaluating a query and its normalized version from the root node of a graph both yield the same result. To be able to establish this equivalence, we must however consider a generalized statement that quantifies over every node of the graph. Similarly to the previous result, the proof of the main lemma above proceeds by well-founded induction over the size of the selection set.

Simplified Semantics of Normalized Queries

One of the main properties of queries in normal form is that they produce non-redundant responses. This in turn permits defining a simplified evaluation function which H&P crucially use to establish their complexity results. However, H&P do not formally prove that this simplified semantics is equivalent to the original, when considering normalized queries.

We define the simplified semantics • G of H&P as shown in Figure 9 and prove that, for queries in normal form, both φ G and φ G produce the same response. The proof is once again performed by induction over the size of the selection set.

Observations

Mechanizing normalization and the simplified semantics, as well as associated properties and proofs, led us to identify some issues in H&P's definitions. While these are admittedly minor, they confirm the value of mechanized formalization.

the tree structure of queries, possibly increasing the difficulty in reasoning about them.

Trustworthiness. We have striven to establish a direct "eyeball correspondence" between GraphCoQL and the Spec whenever possible-though this correspondence has not (yet) been as seriously and systematically established as in other language formalization efforts such as JSCert [START_REF] Bodin | A trusted mechanised JavaScript specification[END_REF] and CoqR [START_REF] Bodin | A trustworthy mechanized formalization of R[END_REF]. In particular, the GraphCoQL definitions closely follow the algorithmic definitions of the Spec. Also, whenever it makes sense, we explicitly reference the corresponding specific sections from the Spec, inside of comments in the Coq definitions.

As mentioned earlier, GraphCoQL adopts a graph data model in order to give semantics to data access. This approach, which follows H&P, goes beyond what the Spec mandates. Indeed, the Spec defers to resolvers to give meaning to data accesses, which are essentially arbitrary pieces of code. However, reasoning about GraphQL requires some sensible data model. In this respect, GraphCoQL follows H&P almost literally, while the query evaluation algorithm of GraphCoQL can be traced closely to Spec.

Validation. In order to further validate that GraphCoQL adequately captures the semantics of GraphQL, we implemented several examples, coming from different sources. In all examples we define the values used in arguments and properties of nodes as elements of an inductive type, which wraps standard Coq types such as integers and strings, and a coercion function to transform these values into the corresponding JSON format.

First, we implement all of the examples used in the Spec validation section (cf. §5 [START_REF]GraphQL specification[END_REF]), for features that GraphCoQL currently supports. These correspond to tests over fields, such as valid definition in given types in scope, proper use of arguments and whether they are are type-compatible and renaming-consistent. Also, the examples include validation of inline fragments and whether they can be used in certain contexts.

Second, we implemented the main example used in H&P, from its schema to its graph, query and corresponding response. Note that this example is quite close to the running example of this paper.

Finally, we also implemented the Star Wars example defined in the reference implementation of GraphQL, 12 up to the currently-supported features in GraphCoQL. For instance, we include the complete schema definition except for the secretBackstory field, which resolves to an error, as these are not yet supported.

Related Work

To the best of our knowledge, the only formalization efforts around GraphQL are H&P [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF] and [START_REF] Hartig | Defining schemas for property graphs by using the GraphQL schema definition language[END_REF], which we have already discussed. The rest of the GraphQL literature focuses on practical issues such as creating GraphQL services and migrating REST-based web services GraphQL [START_REF] Bryant | GraphQL for archival metadata: An overview of the EHRI GraphQL API[END_REF][START_REF] Vázqez-Ingelmo | Improving the OEEU's data-driven technological ecosystem's interoperability with GraphQL[END_REF][START_REF] Vogel | Experiences on migrating RESTful web services to GraphQL[END_REF], automatic migration [START_REF] Wittern | Generating GraphQLwrappers for REST(-like) APIs[END_REF], and testing techniques [START_REF] Vargas | Deviation testing: A test case generation technique for GraphQL APIs[END_REF]. A couple of empirical studies analyze the structure of GraphQL schemas in commercial and open-source projects [START_REF] Kim | An empirical analysis of GraphQL API schemas in open code repositories and package registries[END_REF][START_REF] Wittern | An empirical study of GraphQL schemas[END_REF], shedding interesting insights on GraphQL in practice.

Despite being used mostly for web services, there are efforts to extend notions used in GraphQL to other areas of database specification and querying. Hartig and Hidders [START_REF] Hartig | Defining schemas for property graphs by using the GraphQL schema definition language[END_REF] use the GraphQL schema definition DSL to define the structure of property graphs, which can be linked to similar efforts to define the structure of graph databases [START_REF] Bonifati | Schema validation and evolution for graph databases[END_REF]. Taelman et al. study the transformation of GraphQL queries to SPARQL [START_REF] Taelman | Linked data querying with GraphQL[END_REF]; however we are not aware of any mechanized formalization of SPARQL.

The mechanized formalization of data management systems has received a lot of attention in the traditional relational data model [START_REF] Benzaken | A Coq formalization of the relational data model[END_REF], SQL and its semantics [START_REF] Benzaken | A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra[END_REF][START_REF] Benzaken | A Coq formalisation of SQL's execution engines[END_REF][START_REF] Chu | Axiomatic foundations and algorithms for deciding semantic equivalences of SQL queries[END_REF][START_REF] Chu | HoTTSQL: proving query rewrites with univalent SQL semantics[END_REF], as well as related query languages and engines [START_REF] Auerbach | Q*cert: A platform for implementing and verifying query compilers[END_REF][START_REF] Benzaken | Certifying standard and stratified Datalog inference engines in Ssreflect[END_REF]. Coq is the proof assistant of choice for all these efforts. The tree-based nature of GraphQL queries and response differs significantly from the tuple-based semantics in traditional query languages, requiring different models and techniques. Doczkal and Pous [START_REF] Doczkal | Graph theory in Coq: Minors, treewidth, and isomorphisms[END_REF] develop a mechanization of graph theory in Coq, including simple graphs, digraphs, and their properties. Their work could possibly be extended to deal with property graphs, and used for GraphCoQL. Bonifati et al. [START_REF] Bonifati | Certified graph view maintenance with regular Datalog[END_REF] build a Coq incremental graph view maintenance and evaluation engine; they experimentally assessed it on synthetic graphs generated from real-world schemas. The engine supports Regular Datalog queries and does not entirely fit the GraphQL setting; it could however serve as a base to extend GraphCoQL with mutation.

Conclusion

We have presented GraphCoQL, the first mechanized formalization of GraphQL, implemented in the Coq proof assistant. GraphCoQL currently covers most of the schema definition DSL, the query definition language, validity checking, and the query semantics over a graph data model. We study the query transformation proposed and exploited by Hartig and Pérez to establish their complexity results. Specifically, we provide an algorithmic definition of query normalization, proving it correct and semantics preserving. In the process we uncover and address some minor issues in the original definitions.

This work is a first step towards a mechanization of all of GraphQL, leaving several open venues for future work. The most pressing are supporting mutation, directives and non-null types, and experimenting with extraction in order to (ideally) derive a reference implementation directly from the mechanized specifications. We anticipate that extending GraphCoQL to support new features should be fairly straightforward. More engineering work needs to be done to adequately prepare the Coq development for such extensions, in particular through better modularity and automation. Finally, we would like to study a more abstract evaluation function that is not tied to the graph data model, which should then be derivable as a specific instance.

Figure 1 .

 1 Figure 1. Example of GraphQL schema.

Figure 2 .

 2 Figure 2. Example of GraphQL graph.

Figure 3 .

 3 Figure 3. GraphQL query (left) and its response (right).

Figure 3 .

 3 Observe that the response structure closely resembles the query, which is a key usability asset of GraphQL. While data accesses are handled by resolvers in the backend, the query evaluation process of GraphQL can be intuitively understood by considering a graph data model. In such a model, the selections in a query indicate what edges to traverse in the graph and what properties to access on each node. In this manner, starting from TypeDefinition ::= | scalar name | type name (implements name + ) ? {Field + } | interface name {Field + } | union name = name (|name) * | enum name {name + } Field ::= name (Arg + ) ? : Type Arg ::= name : Type Type ::= | name | [Type] Inductive TypeDefinition : Type := | ScalarTypeDefinition (name : Name) | ObjectTypeDefinition (name : Name) (interfaces : seq Name) (fields : seq FieldDefinition) | InterfaceTypeDefinition (name : Name) (fields : seq FieldDefinition) | UnionTypeDefinition (name : Name) (members : seq Name) | EnumTypeDefinition (name : Name) (members : seq EnumValue). Inductive type : Type := | NamedType : Name -> type | ListType : type -> type.

Figure 4 .

 4 Figure 4. Definition of GraphQL types: (left) Spec grammar; (right) GraphCoQL definition. The (•) ? notation denotes optional attributes.

Definition

  is_a_wf_schema (s : graphQLSchema) : bool := is_object_type s s.(query_type) && uniq s.(type_names) && all is_a_wf_type_def s.(type_definitions).

  query { movie[id:2000] { . . . on Animation { title style } . . . on Fiction { title style } } } at a given selection location.

φ

  ::= query (name) ? {σ } σ ::= f[α] | a:f[α] | f[α] {σ } | a:f[α] {σ } | ... on t {σ } Record query := Query { qname : option string; selection_set : seq Selection }. Inductive Selection : Type := | SingleField (name : Name) (arguments : seq (Name * Value)) | SingleAliasedField (alias : Name) (name : Name) (arguments : seq (Name * Value)) | NestedField (name : Name) (arguments : seq (Name * Value)) (subselections : seq Selection) | NestedAliasedField (alias : Name) (name : Name) (arguments : seq (Name * Value)) (subselections : seq Selection) | InlineFragment (type_condition : Name) (subselections : seq Selection).

Figure 5 .

 5 Figure 5. Definition of GraphQL queries: (top) Spec grammar; (bottom) GraphCoQL definition.

  Definition query_conforms (s : wfGraphQLSchema) (φ : query) : bool := selections_conform s s.(query_type) φ.(selection_set). Definition selections_conform (s : wfGraphQLSchema) (ts : Name) (σ s : seq Selection) : bool := let σ s_with_scope := [seq (ts, σ ) | σ <-σ s] in all (is_consistent ts) σ s && σ s_with_scope.(are_type_compatible) && σ s_with_scope.(are_renaming_consistent).

Figure 8 .

 8 Figure 8. Normalization procedure for GraphQL selections.

  ftype(ts,f) (β ++ merge(collect(ts, f, σ )))} :: N ts (filter(f, σ )) if is_object_type(ftype(ts, f)) f[α] {map (λt i . ... on t i {N t i (β ++ merge(collect(ts, f, σ )))}) get_possible_types(ts)} :: N ts (filter(f, σ )) otherwise

	(4) N ts (... on t {β} :: σ ) =	N ts (β ++ σ ) if fragment_type_applies(ts, t) N ts (σ ) otherwise

https://github.com/graphql/graphql-js

https://foundation.graphql.org/

Note that GraphQL still requires objects to redeclare the implemented fields.

In H&P, this condition is referred to as the consistency of schemas.

Function check_scalar is also used for verifying the conformance of graphs w.r.t. schemas; see §3.2.

Function fragment_type_applies is called does_fragment_type_applies in the Spec.

The situation is worse in H&P, which cannot model nested list types for scalar types.

https://github.com/graphql/graphql-js/tree/master/src/__tests__

* This work is partially funded by ERC Starting Grant SECOMP (715753).

The keywords v and f represent leaf values and keys in a key-value pair, respectively.

• u G : seq Selection → GraphQLResponse (1)

f[α] :: σ u G = f:(complete_value(ftype(u.type, f), u.property(f[α]))) ::

... on t {β} :: As usual, notation x :: y on the left denotes pattern matching deconstruction of a list into its head x and tail y; on the right, it denotes list construction.

property and type are accessors to a node property and type. neighbors gets the neighbors of a node whose edge is labeled with the given field. edges gets the set of edges of a graph. ftype retrieves the type of a field from the underlying schema. list represents the list type (over any other type).

Defining Normal Forms

The notion of normal form introduced by Hartig and Pérez consists of the conjunction of two conditions: being in groundtyped normal form and being non-redundant.

Ground-typed normal form. Informally, a query is in groundtyped normal form, or grounded for short, if any two selections within the same selection set are of the same kind, either field selections or inline fragments. Consider for instance the queries below: The query on the left is not grounded because the selection set under field movie contains two selections of different kind. The query on the right represents a grounded version thereof.

Definition 4.1 ([18]

). A GraphQL selection set σ is in groundtyped normal form if it can be generated by the following grammar, where t is an object type:

A GraphQL query φ is in ground-typed normal form if its selection set is in ground-typed normal form.

Non-redundancy. Informally, the notion of non-redundancy further constraints that of groundedness by forbidding queries that induce a repeated evaluation of selections. For example, consider the two queries below: The query on the left is redundant for two reasons: it requests the field title twice, and it contains multiple inline fragments with the same type condition. Conversely, the query on the right is semantically equivalent and non-redundant. Definition 4.2 (Adapted from [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF]). A GraphQL selection set σ is non-redundant if:

• there is at most one field selection with a given response name, • at most one inline fragment with a given type condition, and • subselections are non-redundant.

A GraphQL query φ is non-redundant if its selection set is non-redundant.

Defining Normalization

The normalization procedure of selection sets is described in Figure 8. It is parametrized by a type in scope and acts as follows. Whenever a field selection is encountered (2-3), normalization removes any field that shares the same response name. This step ensures the non-redundancy of the resulting selection set. However, in order not to lose information during filtering, normalization collects fields with the same response name and merges their subselections in the first occurrence [START_REF] Benzaken | A Coq formalization of the relational data model[END_REF]. This also serves to preserve the order of selections.

Finally, to obtain a selection in ground-typed normal form, normalization performs two separate steps, depending on whether the selection is a field (3) or an inline fragment (4). For the former, the process either directly normalizes the subselections or wraps them with inline fragments, based on the field's type. For the latter, the process either removes fragments or lifts their subselections, depending on whether they apply to the given type in scope.

To normalize a query, we simply normalize its selection set, setting the initial type in scope to the query root type of the underlying schema.

Example. We illustrate the normalization procedure with the example below. On the left we have the original query and on the right its normalized version. Subselections from fragment with type condition Query are lifted and the multiple occurrences of field movie are merged into a single occurrence. Since the type of the field movie is the abstract type Movie, the subselections are wrapped in fragments for each concrete object subtype, namely Animation and Fiction. The normalized query is both non-redundant and in ground-typed normal form.

... on t {β} ::

. Simplified semantics for selections in normal form, adapted from [START_REF] Hartig | Semantics and complexity of GraphQL[END_REF].

First, some queries are considered non-redundant by H&P although they actually produce redundant results. A simple example is the following query: which produces two repeated values. This occurs because H&P's definition of non-redundancy does not consider the case when an unaliased field and an aliased field share the same response name. This cornercase is properly handled in GraphCoQL, by grouping fields by their response names. We discovered this case when proving the equivalence of the simplified semantics. Second, using H&P's equivalence rules, some queries cannot be normalized. For instance: In H&P there are no rules that explicitly consider and use the type in scope to transform selections. In this example, by considering the Query type, either the fragment's contents could be lifted or the field could be wrapped in a fragment, and then the existing rules would apply. We uncovered this issue when working on the semantics preservation proof of the normalization function. In fact, at the time we were formalizing the query semantics following H&P's approach. Working on fixing this issue and the others discussed in §3.5 led us to change the approach of the query semantics, and to adjust the definition of responses.

Discussion

Limitations. Currently, GraphCoQL captures the core of GraphQL, but not the full specification. While this is already valuable to study key aspects of GraphQL-as illustrated in §4-more work is needed to fully cover the specification. For the sake of exhaustiveness, we now list all missing features, referring to the Spec sections [START_REF]GraphQL specification[END_REF] where they are defined: Considering GraphCoQL's current status, integrating some of these missing features should be straightforward: fragments, schema and type extensions, argument default values, input object types and values. For directives, some of the builtin cases have a clear semantics and should be simple to include as well. However, custom directives would be quite hard to integrate because they arbitrarily alter the semantics of queries. It is not entirely clear how these should be modeled and how normalization would be affected by it, regardless of GraphCoQL's current implementation. Similarly, it is not clear how mutation and subscription should be modeled, and what reasoning can be performed on these operations.

Contrarily to custom directives, mutation and subscription, features such as variables, non-null values and error handling, can be properly modeled and implemented, though at some engineering cost. Their implementation would require several changes to GraphCoQL, such as including environments and error propagation, among others.

Supporting introspection would be challenging, given the amount of details involved. Many adjustments would probably be based on case analyzing string values in search of certain patterns, in order to identify introspection selections.

Note that many of the challenges in implementing these features arise from either the fact that it is not entirely clear how to model them (without recurring to generalizations that might compromise valuable reasoning), or that most definitions require nested well-founded recursion as result of


Tanja Hamann

Barbara Schmidt-Thieme²

Cross-linking maths: Using keynotes to structure a curriculum for future teachers

Keywords: Teacher education curriculum, history of mathematics, language

Initial conditions and requirements

Subject-specific content knowledge is an essential component of professional teacher knowledge (for the concept of professional knowledge see for example [START_REF] Schwarz | Professionelle Kompetenz von Mathematiklehramts-studierenden: Eine Analyse der strukturellen Zusammenhänge[END_REF]. It forms a basis for the ability to judge a specific topic's significance for an entire subject and thus forms an important requisite for didactical reflections [START_REF] Dreher | What kind of content knowledge do secondary mathematics teachers need? A conceptualization taking into account academic and school mathematics[END_REF]. Considering this, mathematics teachers' content knowledge must comprise not only advanced insight into specific topics but also a netlike overview of mathematics as one, consisting of notions and relations between them as well as methods and basic principles. A survey in a second-year lecture on arithmetic showed that the students were not able to connect what they heard about equivalence relations, functions or groups to corresponding contents they had learned in previous lectures (e. g. congruence and the group of congruence mappings in geometry, isomorphisms and linear functions in linear algebra).

To achieve that students are able to see these parallels, a university curriculum for future teachers demands cross-links between the single courses. Basic notions (such as sets, functions, algorithms, relations…) that are found in diverse mathematical subdomains seem suitable for serving as crosslinks between scientific lectures, both, in a horizontal and a vertical way. This would transfer [START_REF] Bruner | The process of education[END_REF] concept of fundamental ideas and a spiral curriculum onto teacher education, also suggested in Dreher et al. (2018, pp. 330 f.).

Basic ideas and fundamental notions can be found when one looks into the history of a subject as they should appear throughout time [START_REF] Schweiger | Fundamentale Ideen" der Analysis und handlungsorientierter Unterricht[END_REF], though maybe in different disguises. Apart from that aspect, including the history of mathematics into teacher education has been suggested long-since, presumably bearing a whole lot of further benefits [START_REF] Schubring | History of mathematics for trainee teachers[END_REF][START_REF] Katz | Using history to teach mathematics: An international perspective[END_REF][START_REF] Jankvist | Mathematical knowledge for teaching teachers: The case of history in mathematics education[END_REF], for example experiencing mathematics as a process conducted by human beings rather than as a mere product and thus influencing future teachers' beliefs. In addition, through history of mathematics one learns about the synthesis of notions and terms. This is of special importance for future teachers as it surely facilitates due decompression of scientific content into school content, which requires thorough analysis. (Dreher et al., 2018, 331) Generation, clarification and precision of mathematical concepts and notions require the use of language (e.g. [START_REF] Morgan | Language and communication in mathematics education: an overview of research in the field[END_REF]. Without language, definitions and propositions could not be worded and not be taught either, so language forms another essential part of content as well as pedagogic content knowledge. Due to increasing heterogeneity in pupils' language abilities, it is necessary that future teachers learn to illustrate subject matters on differing language levels and that they become able to vary by those levels.

The Hildesheim concept of "Learning along Keynotes" (LaK)

We suggest that integrating the three keynotesbasic notions, history and language of mathematics -into a teachers' curriculum and thus cross-linking the courses supports the construction of a professional teacher content knowledge as required. Therefore, the keynotes should become a constitutional part of all scientific lectures throughout studies. Our poster presents a concept of how the three keynotes might constitute a scaffolding for a spiral curriculum, where historical and language elements serve as enrichment as well as embedding of basic contentual and methodical concepts. We also present an exemplary concretization for the basic notion "algorithm".

LaK started 2018 in a first-year (linear algebra) and a second-year (arithmetic) lecture at the university of Hildesheim. Historical and linguistic tasks that are mostly integrated into exercises associated to the lectures comprise transferring formulas into common language or working on original historical texts.

To emphasize the netlike structure students are encouraged to design concept maps for a selection of basic notions (see poster for complete list) and augment them in the course of their studies, starting from first year and going on through all lectures. The next step will be to design appropriate tasks for all scientific lectures as well as a research frame for evaluating the concept in the form of a long term study.


Fiona Haniak-Cockerham
email: f.cockerham@mmu.ac.uk

Teacher education: Developing the individual within the collaborative

Keywords: Collaboration, identity, emotion, psychoanalysis

This study explored student teachers' ability to develop their own teaching identity whilst teaching collaboratively as a trio in a "University School Model" of initial teacher education. The paper considers this from a psychoanalytical viewpoint in which the student teachers' emotions and desires are explored in relation to how they experience their work with their peers. The main focus is on how they negotiated the tensions around differing individual pedagogies within the group whilst maintaining the delicate balance between compliance and integrity. The paper concludes that it was through the process of navigating these tensions that they challenged their own pedagogy and in the course of working collaboratively, modified their developing teacher identity.

Introduction

Although 'a considerable amount of current research on teaching and teacher education focuses on teacher collaboration' (Meirink et al., 2007, p.145), previous research tends to focus on qualified teachers supporting each other, or qualified teachers' collaboration with student teachers. Taking a different approach, this paper is concerned with student teachers collaborating with their peers. The paper describes the thinking behind the "University School Model" (USM) and the way in which the author worked with student teachers over the course of a year. Employing [START_REF] Britzman | Lost subjects, contested objects: Towards a psychoanalytic inquiry of learning[END_REF][START_REF] Britzman | Practice makes practice: A critical study of learning to teach[END_REF][START_REF] Britzman | The very thought of education: Psychoanalysis and the impossible professions[END_REF]) and [START_REF] Bibby | Education: An 'impossible profession'? Psychoanalytic explorations of learning and classrooms[END_REF] psychoanalytical approaches to teacher education, it acknowledges there are emotional tensions in developing a teacher identity but that learning to teach is a social process requiring negotiation. Although there is a resistance to changing their perception of teaching, the USM incurs differing pedagogies and argues that this is central in supporting student teachers' development and their autonomy. It considers the university tutor's role and implications for initial teacher education (ITE).

Literature review: Collaborative teaching and multiple placements

A significant amount of research has focused on the role of collaborative practice (Cajkler et al., 2014;[START_REF] Eraut | Learning from other people in the workplace[END_REF][START_REF] Meirink | A closer look at teachers' individual learning in collaborative settings[END_REF] and the effect this has in supporting the developing professional. Cajkler et al. (2014, p.521) found that planning lessons collaboratively led teachers to be 'more courageous and give greater responsibility to students to manage their own learning'. Their study also suggests that collaboration led to a greater willingness for pedagogical risk-taking and 'opportunities for participants to develop individual expertise leading to greater confidence to make changes… and address learning challenges with creative and engaging approaches' (Cajkler et al., 2014, p.526). They conclude that working collaboratively allows for a deeper study of pedagogy.

Teachers in their developing years take on a challenging role within the first weeks on teaching placement, and can struggle to survive in extremely crowded and demanding environments [START_REF] Eraut | Learning from other people in the workplace[END_REF]. Their survival depends on being able to reduce their cognitive load by prioritisation and routinisation, and therefore they may not focus on the pedagogical issues within their teaching [START_REF] Eraut | Learning from other people in the workplace[END_REF]. However, collaborative teaching contexts enable sharing of responsibilities within the classroom and therefore more space for reflection, allowing for routinisation to be less of a necessity in the first few weeks, but developed reflectively with evaluation over time.

Collaborative practice in a 'traditional' model of teacher education takes the form of the student teacher working as an 'apprentice' with the class teacher or a subject mentor. Student teachers in this situation may feel obliged to incorporate advice and ideas from 'expert' teachers and mentors in their school placements into their own teaching, therefore becoming merely compliant with the ideas that have been shared rather than being co-constructors of them. A related issue is that established teachers may find it difficult to articulate their practice to student teachers on placement, since what started as explicit routines in their early experiences have become tacit routines over time [START_REF] Eraut | Learning from other people in the workplace[END_REF]. In contrast, teaching with student teacher peers means that routines which are not yet instinctive can therefore be evaluated and re-assessed together, becoming established in unison. This shift from working alongside more experienced teachers towards working and collaborating with peers is the context for this research.

The University School Model of teacher education

During my necessarily infrequent visits to observe student teachers during their school placements as part of traditional ITE programmes, I was often dismayed to see students who had previously been creative and innovative in their teaching revert to procedural didactic methods. One reason for this commonly observed gap between the theory learnt at the university and the practice seen in school [START_REF] Allen | Valuing practice over theory: How beginning teachers re-orient their practice in the transition from the university to the workplace[END_REF] is that the student teacher in placement is isolated from the support and advice of the university tutor. Too often, the once inventive and imaginative practice enthused over at the university is sacrificed to ensure compliance with the reductionist process-driven teaching dominant in many school placements [START_REF] Cockerham | University schools: A collaborative approach to ITT in secondary mathematics[END_REF].

To address this issue, Manchester Metropolitan University developed a collaborative teacher education programme, namely the 'University School Model' (USM) in 2010. The USM involves placing six student teachers in a school, where they teach collaboratively in two groups of three, as well as individually. The unique attribute of this model is that the university tutor works in the placement school alongside teachers and student teachers, visiting weekly for a whole day. This provides an opportunity to observe and work regularly with student teachers, supporting the integration of practice based on theory and promoting teacher autonomy and professionalism in a more cohesive manner.

Collaborative teaching during these placements is paramount in developing innovative lessons as well as encouraging student teachers to become more reflective practitioners. "Learning about teaching is a collaborative activity" (Northfied and Gunstone, 1997, p.49) and the USM works on the assumption that it is most productive when conducted in groups where ideas and experiences can be discussed. Although working in a group with differing pedagogies and priorities can lead to tensions and emotions that student teachers find hard to navigate, differences of opinion are crucial in fostering discussion and debate about their perceptions of what makes a "good" mathematics teacher, enabling them to identify and articulate their beliefs about teaching [START_REF] Meirink | A closer look at teachers' individual learning in collaborative settings[END_REF]. The research questions which frame this paper are: What opportunities for student teacher's development arise from the USM of collaborative teaching? What emotional support and tensions are evident whilst working collaboratively in the USM?

Theoretical framework

The field of psychoanalysis has many influential perspectives, however this paper focuses on the approaches of [START_REF] Britzman | Lost subjects, contested objects: Towards a psychoanalytic inquiry of learning[END_REF][START_REF] Britzman | Practice makes practice: A critical study of learning to teach[END_REF][START_REF] Britzman | The very thought of education: Psychoanalysis and the impossible professions[END_REF] and [START_REF] Bibby | Education: An 'impossible profession'? Psychoanalytic explorations of learning and classrooms[END_REF] due to their specific insights into mathematics education. [START_REF] Britzman | The very thought of education: Psychoanalysis and the impossible professions[END_REF] asserts that psychoanalysis is the best way to turn education 'inside out' in order to start to understand something of its emotional situation and its inhibitions, symptoms and anxieties. She claims that it is 'one of the few practices and theories in the human professions that begins with and is affected by the relation between our object world and our sense of relationships with self, others and knowledge' (Britzman, 2010, p.86). Student teachers are placed in a situation of negotiating the balance of being a student themselves whilst trying to teach others, and what characterises the relationship between student teachers and their 'others' is the dependency and desire to be seen as already knowledgeable without having to learn [START_REF] Britzman | Practice makes practice: A critical study of learning to teach[END_REF]. [START_REF] Britzman | Practice makes practice: A critical study of learning to teach[END_REF] also discusses the overfamiliarity of the teacher profession as a significant contribution affecting those learning to teach: student teachers draw on their subjective experiences of teaching from their previous experience of education, as a pupil. We all know what a teacher is and does from our years of observation in our own school system growing up, leading to the scenario that 'many students leave compulsory education believing that "anyone can teach"' (Britzman, 2003, p.27). For Anna Freud (cited in [START_REF] Britzman | The very thought of education: Psychoanalysis and the impossible professions[END_REF] this denial of needing to learn how to teach is the ego's defence against its own vulnerable certainty. Consequently, teachers rarely disclose 'the more private aspects of pedagogy: coping with competing definitions of success and failure, and one's own sense of vulnerability and credibility' (Britzman, 2003, p.28). [START_REF] Britzman | Lost subjects, contested objects: Towards a psychoanalytic inquiry of learning[END_REF] argues that learning to teach demands a change in the learner, in that they must reconsider their previous speculations. Education depends on persuading the student teacher to transcend conflict in order to learn, and psychoanalysis insists that the conflict is purely internal. Therefore, the problem of learning to be a teacher becomes 'how the social and the individual can come to tolerate ethically the demands of the self and the demands of the social' (Britzman, 1998, p.8) However, the beliefs we have about teaching are formed not only from our conscious perceptions of good teaching, but also our unconscious self. Earlier experiences we have relating to vulnerability, that of being educated, create resonances in the unconscious, and these unconscious phantasies are projected onto our current situations, that of being a teacher, affecting our beliefs and values and structuring our actions [START_REF] Bibby | Education: An 'impossible profession'? Psychoanalytic explorations of learning and classrooms[END_REF]. Thus, unconscious processes profoundly influence and are intertwined with more conscious processes [START_REF] Britzman | Lost subjects, contested objects: Towards a psychoanalytic inquiry of learning[END_REF]. The unconscious part affects the way we view the self, the self we project to others and the decisions we make.

The sense we make of ourselves, our identity, our ego, is made up of a layering of identifications that we have either found or been presented with 'out there' [START_REF] Bibby | Education: An 'impossible profession'? Psychoanalytic explorations of learning and classrooms[END_REF], and is therefore dependent on other people's responses to us. This is in contrast to the popular image student teachers bring to their teaching practice, that of 'teaching as an individual activity, privatised by the walls between classrooms' (Britzman, 2003, p.63). In order for the student teachers to reflectively question their teaching identity, it is crucial that they experience images provided by others; this system of judgements frames how we come to be seen and known in terms of being located in the others' field [START_REF] Bibby | Education: An 'impossible profession'? Psychoanalytic explorations of learning and classrooms[END_REF]. You can only know yourself through interactions with others, learning to teach therefore is a social process of negotiation [START_REF] Britzman | Practice makes practice: A critical study of learning to teach[END_REF]. Lacan (cited in Bibby 2011:34) states that there is a gap between the 'me' the trainee teacher is experiencing themselves, including what they see mirrored by other people, and the 'me' they would like to experience; desire is the urge to close the gap between these two versions of 'me'. This can be the cause of significant anxiety for the student teachers. exists a tension between anxiety and desire, there cannot be one without the other and there can be no learning without them [START_REF] Britzman | Lost subjects, contested objects: Towards a psychoanalytic inquiry of learning[END_REF], therefore this is an emotional conflict that they must negotiate in order to learn how to teach.

Methodology

This research was carried out at Manchester Metropolitan University (MMU) with twelve student teachers on a Post Graduate Certificate of Education course (PGCE). The participants were members of my personal tutor group, who were placed in two 'University Schools', chosen on the basis of their previous experience of working as a placement school and their established expert practice. All twelve students agreed to take part in the study, and were assured of their anonymity and given the option to withdraw at any time. I discussed the ethical implications of the situation at length with them, and assured them that it would not affect the support or grading that they received throughout the year. In the USM, students teach two out of their three classes in the first placement as a trio and only one out of the three classes in the second placement. Other lessons are taught individually. Every week the university tutor visits for a full day throughout both placements, working alongside the students to help with planning, observe lessons, give feedback and advice, and provide pastoral support throughout the year.

There are four key sources of data in this research. I used a reflective journal to capture an autobiographical perspective on my practice, as the visiting university tutor. The student teachers reflect weekly on their progress on their placements as part of the PGCE course, and these were used to provide insights into their developing teacher identity. I held four focus groups during the placements to discuss various issues, including on one occasion my delivery of a lesson which had been planned by six of the student teachers, and observed by the students and the class teacher. At the end of the lesson the students gave me feedback, along with the class teacher. The lesson was also video recorded, and played to the focus group. At the end of the PGCE course, once the students' grades and final forms were completed, they participated in individual semi-structured interviews, focusing on their experiences of working in the USM, their ability to work collaboratively and the tensions surrounding this, and reflecting on the teacher they became as a result of their experiences. Both focus groups and interviews were audio recorded. This paper focuses on the interviews, analysed with a particular emphasis on considering the emotional aspect of teaching collaboratively and the effect this had on their developing identities as teachers. The data was operationalised by the theoretical framework and a thematic analysis was conducted. Two of the themes are discussed in this paper with respect to the research questions.

Findings Teaching collaboratively

One of the main issues facing the student teachers in the USM is the idea of teaching collaboratively. They come to the course thinking that they simply require some practice in the classroom and that will be sufficient in making them a 'good teacher'. The idea of having to work alongside other student teachers who may not be as strong as them, may not agree with them, may hold them back in their teaching or may be seen as needing support, was difficult:

Edward:

When we all found about the trios, we were all definitely concerned.

Sarah:

When we heard about it initially we were a bit like, oh, I don't want to do that. I want to go in by myself.

Jennifer: I was a bit apprehensive about the trio at first, cos I just thought I don't want to do it, I don't want to be held back or whatever by someone else.

A common perception was that 'learning' from a peer is not effective for teacher education; they wanted to be in the classroom alone. There was an intrinsic denial that being influenced by their peers would support their own development as a teacher; they felt that learning can only take place from an experienced 'teacher'. The prevalent idea was that education is the knowledge given by the expert and received by the novice.

Carol: I thought "well, you are just a trainee like me". I found it easier to draw on people who had more experience than my own, than the people that I was working with.

The university tutor has a delicate role to play in this situation. The dichotomy of being influential in the student teachers' developing pedagogies, whilst also have a role in ensuring the collaborative nature of the placement is effective:

Carol: I think, especially because when you are working in a three, the people are very different, they come from very different walks of life with very different ideas and opinions. And to have that visit every week [from the university tutor] it lubricates the situation and helps everyone to have a common idea and stops one personality maybe dominating others.

In spite of their misgivings and the tensions of the situation, the students reported that the support they receive from collaborating with peers in their lessons and in planning, means that they can try innovative teaching strategies with reduced fear of failure:

Sarah: But I think you have the opportunity to try different things…[you can] try it.

Because there are three of you it can't go drastically wrong.

Developing the individual within the collaborative

There is a subtle balance to strike when teaching as a trio, between gaining credibility and recognition for your individuality in the classroom and successfully working together and collaborating with your peers. The need to ensure that you are being assessed individually is often a contentious issue:

Carol: because people come into this and they are like this is my training I think that is the heart of it. This is my training and I need to push myself forward even though we are collaborating. Unless people are willing to give that idea up…you end up getting caught up in a situation where you're like oh alright this is all about me too.

Whilst teaching collaboratively there are multiple 'others' constructing the student teacher's view of themselves. The students needed to orchestrate the experience of working with their peers and negotiate how their potentially conflicting pedagogical beliefs would inform their teaching. They also needed to work with the class teachers and subject mentor in whose classroom they were a guest, and therefore expectations to comply. In addition, they needed to work with the university tutor who comes with their own views about effective teaching, and also to manage their own internal beliefs based on their prior experience of education of the teacher they want to be. The latter is the most difficult to modify, since how students see themselves in the role of the teacher is the "phantasy" that has led them to undertake this journey. There is a strong desire to become this teacher and therefore the inclination to teach as they were taught is hard to challenge, but is a crucial element in learning to teach. The importance of these personal histories is the independence of individual journeys: the experience that one person had of education, and which has shaped their desire to be a teacher, is different to anyone else's experience:

Justin: I kinda remember things, of ways I was taught ….and I think if that's the way that I learnt it and I thought it was good then, maybe students now will think it's a good way to learn as well.

Edward: Yeah, because obviously I had my feelings of what I wanted to be as a teacher. Shafia obviously had her idea, which was definitely a lot closer to Claire's [the class teachers] than mine.

The notion of "teaching practice" is thus about the individual finding a path between these fluctuating versions of themselves. In Edward's case, his strong sense of the teacher he wanted to be was brought into question by the class teacher and his collaborative partner. Edward was adamant that he was not willing to change his teaching style. However, by the end of the placement he reflected back to say:

Edward: I think it has changed me slightly on where I was going to be, or where I thought I would be, but I think that was more for the better.

Emotional support and tensions

Inevitably, the student teachers are all vying for their persona and their pedagogy to be dominant. When working as a group, if lesson planning and making decisions regarding how to teach a topic lead to differing views, this tension brings with it a strong emotional element. There is a sense of anxiety amongst the student teachers about which methods to teach, how to deal with behaviour, and how to manage the learning. The desire to teach the best lesson possible and be a successful teacher leads to further anxiety. This emotional tension can be difficult to navigate if the lesson is not being planned and delivered in a manner which reflects the teacher they are striving to become. However, the presence of anxiety and therefore desire is needed in order to progress; to close the gap between the image they see of themselves and the image which is projected to others.

However, there is also an opportunity for a student's ego to protect itself from the judgement of others by not contributing ideas and hiding behind the work of others. If the lesson does not go as well as planned there is an opportunity to remove yourself from the emotional disturbance of the feedback because you can convince yourself that this was not your lesson:

Edward: Because I don't like conflict too much so I just like "ok we will do it that way". I think that's probably bad in terms of teaching…going into a lesson and not being fully committed to the lesson…because it's not the way I wanted to do it.

The student teachers' anxiety at the start of the placement about not wanting to collaborate and the desire to teach on their own was alleviated in all of the participants in this research; this was mainly explained in terms of the emotional support they gave each other. This outweighed the emotional conflicts of teaching as a trio, with the anxieties and tensions this incurred:

Jennifer Overall the concern about them developing into the teacher they envisioned at the start of their placement was diminished throughout the year and the USM facilitated their ability to explore their autonomy and their agency in developing their teacher identity.

Jess: I think it has been easy to develop, there has been lots of support. This model has been really good for that. And I've not been one for asking for help but the help was always there.

Alison: You are obviously not always going to get on with your trio, it is inevitable that you are going to have differences, but you'll become the teacher you want to be in the end anyway.

Conclusion

The 'University School Model' of ITE aims to foster collaborative learning which supports student teachers in developing as teachers informed by the university and protected to some degree from mere compliance with placement school practices. What this research has found is at first there is a resistance to working collaboratively in a classroom, due to a host of emotional reasons: their ego, their preconceived perceptions of their teacher identity, fear of being held back. However, throughout the placement, students' ideals about teaching are challenged through working with peers, and although they may resist the change, the situation allows them to develop their pedagogy in a 'safe' environment. Collaboration with their peers allows them to shift their version of themselves, and experience differing pedagogies without the possibility of failure resting solely on their shoulders. The pressure of compliance from their supporting teachers and the university tutor are still perceptible, but the collaborative nature supports them in the negotiation and articulation of their teacher identity. It allows creative and innovative lessons to be explored due to the support of the other student teachers in the room, with a shared responsibility, yet with an emphasis on their personal development. The students' final overall conclusion was that they all individually achieved their desire of becoming the teacher they wanted to be, despite their original notions of this being challenged. This research highlights the nature and role of emotion in the development of student teachers' teacher identities. It is interesting to consider how 'the teacher they wanted to be' at the start of the PGCE evolves as a result of experiences in the USM and the effect the individual personalities in their trios had on their development. It also highlights the role of the university tutor as a facilitator in this development. These are areas to be explored further.

  :If you go into it big headed, that you're the best teacher ever and you don't need it [the support from your peers] you'll fail because you need the people around you, you need that safety blanket.

	Edward:	It's nice having people around you that are in the same boat…obviously, you have
		two other people who are kind of your back bone in that sense and are supporting
		you