Skip to content

Commit

Permalink
Merge pull request #1 from shati-patel/typeunions-edits
Browse files Browse the repository at this point in the history
Editorial suggestions for "type unions"
  • Loading branch information
ginsbach authored May 27, 2020
2 parents 460b64c + 6c9c803 commit 748d01f
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 13 deletions.
2 changes: 2 additions & 0 deletions docs/language/ql-handbook/aliases.rst
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ of ``OldVersion``, you could deprecate the name ``OldVersion`` as follows::
That way both names resolve to the same module, but if you use the name ``OldVersion``,
a deprecation warning is displayed.

.. _type-aliases:

Type aliases
============

Expand Down
26 changes: 13 additions & 13 deletions docs/language/ql-handbook/types.rst
Original file line number Diff line number Diff line change
Expand Up @@ -482,35 +482,35 @@ program, so it's helpful to extend a new type (namely ``TTaintType``)::
.. _type-unions:

Type Unions
Type unions
***********

.. note::
The syntax for type unions is considered experimental and is subject to change.
However, they appear in the `standard QL libraries <https://github.com/github/codeql>`.
The following sections should help you understand those examples
However, type unions appear in the `standard QL libraries <https://github.com/github/codeql>`__.
The following sections should help you understand those examples.

Type unions are user-defined types that are declared with the keyword ``class``.
The syntax resembles type aliases, but with two or more type expressions on the right-hand side.
The syntax resembles :ref:`type aliases <type-aliases>`, but with two or more type expressions on the right-hand side.

Type unions are used for creating restricted versions of existing algebraic datatypes, by explicitly
selecting a subset of the branches of said datatype and binding them to a new type.
In addition to this, type unions of database types are also supported.
Type unions are used for creating restricted versions of an existing :ref:`algebraic datatype <algebraic-datatypes>`, by explicitly
selecting a subset of the branches of that datatype and binding them to a new type.
Type unions of :ref:`database types <database-types>` are also supported.

Using a type union to explicitly restrict the permitted branches from an algebraic datatype
can resolve spurious recursion in predicates.
You can use a type union to explicitly restrict the permitted branches from an algebraic datatype
and resolve spurious :ref:`recursion <recursion>` in predicates.
For example, the following construction is legal::

newtype T =
T1(T t) { not exists(T2orT3 s | t = s) } or
T2(int x) { x = 1 or x = 2 } or
T3(int x) { x = 3 or x = 4 or x = 5 }
T1(T t) { not exists(T2orT3 s | t = s) } or
T2(int x) { x = 1 or x = 2 } or
T3(int x) { x = 3 or x = 4 or x = 5 }

class T2orT3 = T2 or T3;

However, a similar implementation that restricts ``T`` in a class extension is not valid.
The class ``T2orT3`` triggers a type test for ``T``, which results in an illegal recursion
``T2orT3->T->T1->¬T2orT2`` due to the reliance of ``T1`` on ``T2orT3``::
``T2orT3 -> T -> T1 -> ¬T2orT3`` since ``T1`` relies on ``T2orT3``::

class T2orT3 extends T {
T2orT3() {
Expand Down

0 comments on commit 748d01f

Please sign in to comment.