This project is very work in progress. The content may contain mistakes and it should be considered draft. Notes are written down in my spare time and made public without revision.
This is a personal notebook where I writes about GraphQL and related topics. This is not another tutorial about GraphQL, but my own unconventional way to try to learn it.
Click here to open an almost updated version of the notebook.
As far I know, GraphQL does not provide a formal semantics of the language. Hence, I am trying to fill the gap with the definition of an abstract syntax and semantics.
The abstract syntax is not syntactically one-to-one with the language generated by the GraphQL grammar. For example, I introduced more constructs (e.g. holes, contexts, ...) than those described by the official spec. Ideally, the abstract syntax should be a tool for reasoning about the real or target language and not the language itself.
The general approach I am following for the formalization of GraphQL semantics can be summarized in these assumptions.
- Queries are terms with a type.
- Schemas are types.
- The execution of a query yields a value following an operational semantics.
- Execution does not get stuck if the schema type is a subtype of the query type.
My main reference is [Pierce2002], that is also recommended as background material. Other references can be found in the text.
- Working on safety proof
- Reviewing fragments rules, in particular wrt context values
- Started thinking about partial evaluation
See Changelog to stay updated.