discussion.tex

% !TEX root = ./main.tex
\section{Discussion}\label{sec:discussion}

\paragraph{Limitations.}

Currently, \gcoql captures the core of \gql, but not the full specification. While this is already valuable to study key aspects of \gql---as illustrated in \S\ref{sec:norm}---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~\cite{gqlspec} where they are defined:

\begin{itemize}
\item \emph{Executable definitions:}\ \ %
% \et{meaning?}\td{That is just the name \gql gives to these features}: 
mutations (\S2.3), subscriptions (\S2.3), fragments (\S2.8).
\item \emph{Types and type operations:}\ \ Non-null types (\S2.11-3.4.1-3.12), schema and type extensions (\S3.2.2-3.4.3), argument default values (\S3.6.1), input object types (\S3.10), directives (\S3.13).
\item \emph{Queries:}\ \ input object values (\S2.9.8), variables (\S2.10), variable and argument coercion (\S6.1.2-6.4.1), normal and serial execution (\S6.3.1), error handling (\S6.4.4).
\item \emph{Introspection:}\ \ fully unsupported (\S4). 
\end{itemize}

\noindent Considering \gcoql'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 \gcoql's current implementation. 
Similarly, it is not clear how mutation and subscription should be modeled, and
what reasoning can be performed on these operations. 
% Their difficulty lies beyond the scope of this mechanization.  

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 \gcoql, such as including environments and error propagation, among others.
% However, these changes seem manageable with enough engineering power. 
% The main challenge may lie in properly handling normalization and the semantic preservation in the presence of errors.

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 the tree structure of queries, possibly increasing the
difficulty in reasoning about them. 
% This is even more so when the definitions are composed between them. 



\paragraph{Trustworthiness.}

% To address the trustworthiness of \gcoql, 
We have striven to establish a direct ``eyeball correspondence'' between \gcoql 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~\cite{jscert} and \coqr~\cite{coqr}. 
In particular, the \gcoql 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.
% \et{how does this correspondence manifest? do you reference the spec sections explicitly in the Coq development?}\et{argue}\td{I had links and then removed them, but I can add them again}\{yes!}

As mentioned earlier, \gcoql adopts a graph data model in order to give semantics to data access. This approach, which follows \HP, goes beyond what the \spec mandates. Indeed, the \spec defers to {\em resolvers} to give meaning to data accesses, which are essentially arbitrary pieces of code. However, reasoning about \gql requires some sensible data model. In this respect, \gcoql follows \HP almost literally, while the query evaluation algorithm of \gcoql can be traced closely to \spec.
% \et{anything else to say?}\td{Not really}

% While \spec leaves the underlying data model unspecified \et{or under-specified?}, 
% \et{integrate: the resolvers can actually be mentioned at the intro when you mention whether readers will understand why a data model is necessary -- because 
% \gql simply assumes the existence of resolver functions.}
% \HP adopts at its core a graph-based data model; 

% \gcoql follows \HP in this regard, while the query evaluation algorithm of \gcoql can be traced closely to \spec.

% \et{\gql is data model agnostic. \HP specializes to a graph-based data model. So do we. Readers will wonder: is this necessary? why? aren't we moving away from the actual \gql by taking this path? -- this needs some careful justification}


\paragraph{Validation.}

In order to further validate that \gcoql adequately captures the semantics of \gql, 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.

% \et{you say four sources, but below there is only three}
% \td{Ah, lol. The fourth one was the one we use in the paper (Goodbois) -- although it is in essence the same as the one in \HP}
% \td{I didn't want to reuse the same example they used, bc it felt like just copy paste -- Although now it is not that far off tbh}

First, we implement all of the examples used in the \spec validation section (\cf\S5~\cite{gqlspec}), for features that \gcoql 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. 

%First, We implemented a subset of the examples used in the \spec validation section (\cf\S5~\cite{gqlspec}).
%We include 41 of the 92 total examples present in that section.\et{this is not a very good number. Can you get it up by the deadline? or give better evidence that the subset includes the most important ones?}
%The large majority of the examples that we have not implemented correspond to 
%variables validation (31 cases) and fragments (29)\td{Some of these are tests that overlap with the inline fragments -- So we are still kind of testing them}
%\td{The cases that are exclusive to fragments are 8}\td{Also, some cases use fragment only as a way to write the tests, but they are not really necessary
%(they are not testing things from the fragments) so I don't consider them}.
%\td{The rest of cases are a mix of things -- 11 are related to operations (\eg no two queries with the same name, no named query + another unnamed query, etc)}

% \et{relate to the limitations above: of course you can't include examples that require unsupported features. Is it as simple as saying that you have implemented all examples that do not require such features?}
% \td{Yes}
%\et{try to put some "positive characterization" of what the implemented examples cover}

Second, we implemented the main example used in \HP, from its schema to its graph, query and corresponding response. Note that this example is quite close to the running example of this paper.
% \td{This is actually done in all examples.}
% \td{There is not much to say about HP's example tbh}


\iffalse
	-	Only executable definitions when evaluating = -1 (text + query)
	- Uniqueness of operation = -3
	- Anonymous operation = -2
	- Suscription = -5 (single root field)
	- Fields = 2 + 2 + 2 - 1 (introspection on union)
	- Field merging = 3 + 1 - 1 (variable) + 2 - 2  (variables) + 2  + 1
	- Leaf fields = 2 + 3 - 1 (type ext)
	- Argument names = 2 - 1 (directives) + 1 - 1 (directives) + 2  - 1 (type extension)
	- Required args = -5 (required arguments - non-null + default values)
	- Fragment uniqueness = -2 (fragments)
	- Fragment spread type existence = 1 - 3 (2 fragments y 1 directive) + 1 - 2 (fragments)
	- Fragments on comp types = 3 - 3 (fragments) + 2 - 2 (fragments)
	- Fragments must be used = -1
	- Fragments spread = -4 (fragments) + 2 - 2 (fragments) + 1 - 2 (fragments) + 1 - 2 (fragments) + 2 - 2  + 2 - 2 + 1 - 2 + 1 - 2 
	- Valid Input values = -5
	- Input objects = -3
	- Directives = -3
	- Variables = - 2 - 8 - 7 - 4 - 7
	
	Hechos : 2 + 2 + 2 + 3 + 1 + 2 + 2 + 2 + 3 + 2 + 1 + 2  + 1 + 1 + 3 + 2 + 2 + 1 + 1 + 2 + 2 + 1 + 1 = 41
	No hechos : -1 - 3 - 2 - 5 - 1 - 1 - 2 - 1 - 1 - 1 - 1 - 5 - 2 - 3 - 2 - 3 - 2  - 1 - 2 - 2 - 2 - 2 - 2 - 2 -2 - 2 - 5 - 3 - 3 - 2 - 8 - 7 - 4 - 7  = 92
	- Variables = -1 - 2 - 2 - 8 - 7 - 4 - 7 = 31
	- Fragments = -2 - 2 - 2 - 3 - 2 - 1 - 4 - 2 - 2 - 2 - 2 - 2 - 1 - 2 = 29 
	- Operations = -1 - 3 - 2 - 5 = 11
	- Directives = -1 -1 - 1 - 3 = 6
	- Valid input values = 5
\fi 
	
Finally, we also implemented the Star Wars example defined in the reference implementation of \gql,\footnote{https://github.com/graphql/graphql-js/tree/master/src/\_\_tests\_\_} up to the currently-supported features in \gcoql.
For instance, we include the complete schema definition except for the \texttt{secretBackstory} field, which resolves to an error, as these are not yet supported. 

% The data modeled as a graph and 
% evaluation of 9 queries (out of a total of 17), comparing them to the expected outputs. Of the not implemented cases, 3 correspond to errors, 2 to introspection, 1 to fragments, 2 to variables and 
% one where execution is over an object with named properties.\td{I am not sure about the granularity of this (although otherwise it might seem a bit empty)}

% \et{is it only the error stuff that's missing?}\td{Same as above, it is missing not implemented features (errors, fragments, etc.)} 
% \td{Idk, something more specific to JS than \gql}.
% \td{There are 7 other about validation, which I didn't notice, but I can add them}
% \td{In that same repo (https://github.com/graphql/graphql-js/tree/master/src) each subfolder (type, execution, etc) contain other \_\_tests\_\_ folders, but
% I didn't delve too much into them -- some are a bit too particular to JS. They can still be adapted, but not now}
		



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\endinput
%%% OLD DISCUSSION SECTION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Intro to section

\et{I suggest to split this section in two parts: one that is related to the core (schema, data model, queries, semantics), and on that is related to normalization/simplified semantics. And to move the first to just after section 3 (either as a 3.5 or as a separate section 4 if it's length justifies it)}

\subsection{\gql Schema}

\et{I don't get what is the point of this paragraph, and why it matters -- what's the takeaway message? how does it relate to what we did?}
We believe that the \spec's definition of the schema can be slightly confusing and ambiguous. The schema is described as being ``\textit{defined in terms of the types and directives it supports as well as the root operation types for each kind of operation}''\footnote{https://graphql.github.io/graphql-spec/June2018/\#sec-Schema}. However, the \spec also defines a structure called \texttt{schema}\footnote{https://graphql.github.io/graphql-spec/June2018/\#SchemaDefinition} that only contains the root operation types (query, mutation and subscription), meanwhile the type definitions and directives are defined separately. We think this introduces the first ambiguity to the definition. Now, to actually capture the notion described above, it is necessary to define what is called a \textit{Document}\footnote{https://graphql.github.io/graphql-spec/June2018/\#Document}, consisting of a list of definitions and queries. Among these definitions one can include the \texttt{schema} structure, as well as the type definitions and directives (by repeatedly using the \textit{Type System Definition}\footnote{https://graphql.github.io/graphql-spec/June2018/\#TypeSystemDefinition} rule). This effectively permits building the schema as expected, however we think it is unintuitive to allow mixing definitions with queries. Also, the naming of the different structures seems to introduce confusion and inconsistency.

 
% the \spec defines each of the three elements (types, directives and root operation types) as separate entities. The first candidate is the \textit{Type System} \footnote{https://graphql.github.io/graphql-spec/June2018/\#TypeSystemDefinition} but it is a disjunction of the three elements: types, directives and root operation types. 


% Secondly, the \spec defines the \texttt{schema}\footnote{https://graphql.github.io/graphql-spec/June2018/#SchemaDefinition} structure that only contains the root operation types (query, mutation and subscription). The type definitions and directives are defined separately. Even though it is not a major difference, it lends itself to possible confusion when referring to the schema of a \gql service. In addition, the previously quoted definition does


%The previously quoted definition actually matches the \textit{Type System} structure\footnote{https://graphql.github.io/graphql-spec/June2018/\#TypeSystemDefinition}. Our formalization follows the latter but rename it to schema to also match the quoted description.

\et{contrast with what you did, and the tradeoffs (what's convenient, what's not)}
Regarding \HP's consistency property, they embed many properties in their structures, such as uniqueness of types given by using sets. They include an additional check on objects implementing interfaces, where they validate that fields are properly implemented. The definition given is not complete due to missing validation on arguments, but a corrected version is included in \cite{olafschema}.

\subsection{Data model}

As described in Section~\ref{subsec:graph}, \gql is agnostic to the technology used and the underlying data model. We follow \HP and instantiate the semantics to a graph setting, allowing to reason about it\et{see my comment in the intro}. We describe here severe limitations \et{why is the list nesting situation "severe"?? what backs up this characterization?} that this data model introduces on the possible results generated and the open questions regarding how to properly model certain aspects of \gql schemas \et{vague}. This model is exploited by \HP and \cite{olafschema} but neither discuss nor mention the limitations. \et{you only discuss one, without really explaining why it matters, or to what extent. Does it break all established results? etc.}

The main issue with this graph model is that there is no proper accounting of list types containing other list types (with any nesting depth). When it comes to list types it is not clear what they represent in a graph. Let us illustrate this with an example.
%The different features that compose a \gql schema can be represented in a graph somehow. For instance, a field is either a property or the label of an edge, while its return type can be associated to a target node in an edge. However, when it comes to list types it is not clear what they represent in a graph. Let us illustrate this with an example.


% Our definition is in essence the same as in \HP but differs greatly in implementation. \HP defines a \gql graph in a more ``centralized'' manner. For instance, nodes and field names are defined by sets. Node types are defined by a single function which receives a node identifier and gives its type. Properties are also defined by a single function which receives a node identifier and a field name with arguments. Contrarily, our approach attempts to recreate the structures individually. For instance, a node contains all the information pertaining to itself; its type and its properties. We believe this is a more natural approach to defining the graph from an engineering point of view.

A service may declare the field \texttt{friends:[Human]} in a given type, representing the list of friends.
In a graph this can be pictured as having a node with multiple outgoing edges labeled \texttt{friends}, reaching other nodes of type \texttt{Human}. It is possible to then extend the service by including a new field \texttt{friendsByName:[[Human]]}, in which one can request a list of friends but grouped by their names. At the moment neither our implementation, \HP nor \cite{olafschema} properly handle this situation. The open question is what does this represent in the graph? These should be outgoing edges similarly to the previous case but, what should the target nodes be? Should these be intermediate blank nodes? Is every edge labeled or only the last one that reaches a node with type \texttt{Human}? What happens if we increase the nesting? Since the information is ultimately collected from ``concrete'' nodes, should the graph be kept the same but introduce \textit{formatter} functions to match the schema? How does this differ from the \gql resolvers?

These questions and more \et{what are the more? instead of spending half a page on nested lists, tell us what are the other limitations and what their possible impact is -- ie. like a typical "threats to validity" section} are not addressed nor discussed in \HP and it is actually more restrictive than expected\et{expected by whom?}, by not allowing nested lists for scalar values (in nodes's properties)\et{in the previous paragraph, you put all three approaches in the same bag, now it seems \HP does worse}. Meanwhile, our approach and the one used in \cite{olafschema} allow any list type at the property level but simply ignore any possible nesting when the list type refers to neighboring nodes (composite types), as in the example above.\et{for instance, a typical question would be: "how prevalent are those situations?" if you don't know the answer to this question, how can you evaluate if it's severe or anecdotical?}
In the case of \cite{olafschema}, they do not address nor discuss these questions\et{you said that already}. This choice of modeling has some consequences\et{what are they?} when defining the semantics of \gql queries, because the possible results generated are restricted to a smaller subset\et{the limitation seemed to be about the data model, not the queries or their results}. It is not clear what the proper way is to handle this issue\et{still talking about nested lists?} but more is explored in Section~\ref{subsec:semantics}\et{watch out: 3.4 is now *before* this text}. 
We also address the \spec's semantics and how this is managed.\et{?}

\subsection{Queries}

\et{overall verbose and not very clear/insightful}

\HP differs from both the \spec and \gcoql when defining queries, as they include an additional rule for lists of queries. Their grammar includes a production rule for lists of queries, which is defined at the same level of \et{same....as...} the other rules. The main issue we found with this approach is that it allows building arbitrary trees instead of just a list of queries.\et{you say on page 5 that "a valid query has a tree structure"!} These trees can be flattened to recover the list structure but increasing the effort when defining functions and reasoning over queries. We believe this is assumed by \HP but not explicitly mentioned otherwise.


On a different note, we mentioned in Section~\ref{subsec:query} that we split a validation rule\et{which?} into two separate predicates\et{which?}. The reason behind this is that we noticed that the \spec's definition includes redundant recursive calls\et{meaning?} which may result in increased computational time\et{are you worrying about performance in the model?}. By splitting the definition in two parts, we expect to optimize the algorithm and also facilitate reasoning about them\et{why?}. At the time of writing this paper, a new algorithm was proposed by a team at XING\footnote{https://www.xing.com/} that also addresses this very same issue and is described in~\cite{xingalg}. They follow a different approach to resolving it, using sets, and provide a much more elaborate analysis of execution times than us\et{sure, you don't provide any ;-)}. Comparing both approaches and analyzing execution times could be an interesting venue to explore.

Finally, we also noticed that the previous rule\et{which?} is too conservative and may consider valid queries as invalid. This occurs because the \spec allows defining fragments that are never evaluated. The issue is that the validation rule can then consider the subqueries in these fragments as invalid, even though they are never evaluated, rendering the whole query invalid\footnote{An example query can be seen in the following link: https://tinyurl.com/y3hz5vgv.}. We attempt to remove this conservativeness in the predicate that checks the merger of fields but we have not provided proofs that it does. For the predicate regarding unambiguous results, it is equally conservative as the \spec. We believe it should not be hard to modify the definition, however we decided against it at the moment, to keep it simple and facilitate reasoning over the predicate, as well as preserving some similarity to the \spec\td{Although it may not be entirely similar from the start...}.


\subsection{Semantics}

%We finish this section by addressing two major aspects about our formalization; completeness and errors.

The first one\et{?} was briefly mentioned in Section~\ref{subsec:graph}\et{seems this has been moved}, when discussing the limitations and open questions regarding the graph model. These translate in the fact that we currently do not produce list results with nested lists of objects. For instance, the field \texttt{friendsByName:[[Human]]} is treated as if it were defined as \texttt{friendsByName:[Human]} and the results match the latter format. Otherwise, there is no restriction in the case of nested lists for scalar values\et{yep, that was in 5.2}. In \HP, there is no possibility to produce nested lists for either scalar or object values\footnote{The grammar itself does not permit it.} and there is no mention of this restriction.\et{all this was said before}

Regarding error handling, we currently do not implement it. Errors may have two main sources; validation errors and execution errors.\td{Not sure how to write this}\et{does not belong here---more of a "limitations" section (before the conclusion)}

\et{so this section seems vacuous}

\et{overall, after looking at 5.1-5.4, I think that a compressed/selected list of points good be put in a "3.6 Design considerations and discussion" section}

%\subsection{Normalization}

%\et{this section could be a similar section at the end of the normalization section}