Types, type expressions, and type operators

1st1 commented 6 years ago

This issue documents our latest stance on how types and type-related operations should be defined in EdgeQL.

1. Union Types

For the UNION set operator we compute a Union Type for its lefthand and righthand sets. We define union types only for Object Types; there is no concept of a union type for Scalar or Collection types.

A union type for scalar (or collection) types is a type that all of the union-ed types can implicitly cast to.

A union type for a single object type is that type. E.g. a union type for Foo object type is Foo.

A union type for two or more object types is an object type that describes an intersection of all properties and links of its types. For example, for the following two types:

type Foo:
  property a -> int
  property b -> int

type Bar:
  property a -> int

a union type would be defined as:

type UnionOfFooAndBar:
  property a -> int

The following EdgeQL operators can produce union types:

UNION
IF..ELSE
??—coalesce operator

2. Type Expressions

In EdgeQL we have a few places where types can appear in:

type casts: <type><expr> as in <int>"123";
righthand side of the IS operator: <expr> IS <type> as in (SELECT ...) IS User;
in IS operator in paths: <path>[IS <type>] as in Card.<deck[IS User];
DDL commands, e.g. CREATE REQUIRED LINK <name> -> <type>; etc.

This can be generalized by replacing the <type> grammar production with a <type_expr>—a type expression.

Type Expressions can appear only in the afore mentioned situations and are defined as follows:

Name production, e.g.NAME or NAME::NAME.
Name < ... > set of productions; allows to specify collection and scalar types like array<int>.
& operator is used to create Intersection Types (detailed in a section below).
| operator is used to create Union Types; it has lower precedence than &.
( and ) can be used for grouping.

A few valid examples of type expressions:

User | SystemUser—a union type of type User and type SystemUser.
int16 | int32—will evaluate to int32 as that is what type {<int16>1} UNION {<int32>2} expression would evaluate to.
std::array<std::int64>—an array of int64.
(User | SystemUser) & Named—an intersection type of Named with a union type of User and SystemUser.

3. Intersection Types

Intersection types for scalar and collection types are not defined.

An intersection type for one object type is that type itself. E.g. User & User is equivalent to User.

An intersection type for two or more object types is a an object type that describes a union of all properties and links of its types. For example, for the following two types:

type Foo:
  property a -> int
  property b -> int

type Bar:
  property a -> int
  property z -> int

an intersection type would be defined as:

type IntersectionOfFooAndBar:
  property a -> int
  property b -> int
  property z -> int

All links and properties of object types that share same names must be implicitly castable to each other. For instance, the following two object types have no intersection or union types:

type A:
  property a -> str

type B:
  property a -> int

so both A & B and A | B type expressions will raise a compile time error.

A good example of where an intersection type can be useful is the IS operator. The following query will return all objects that are instances of both types A and B: SELECT Something IS A & B.

4. Extensions to EdgeQL expressions

As mentioned in section #2, IS, [IS ...], and <casts> will now accept type expressions. E.g. User IS User & Issue will be a valid expression.
A new TYPEOF <expr> operator to statically compute a type of the expression. The result "type" of the TYPEOF operator is type, so it can appear in type expressions too. For example: User IS TYPEOF (SELECT User) or User IS (TYPEOF (SELECT User) | Issue).
A new INTROSPECT <type_expr> operator to transform types to objects (or Type Objects, as defined in a section below). For example: SELECT (INTROSPECT array<int>).name will return "array<int>".

A new TYPE operator valid in WITH blocks:

db> WITH
...   my_type AS TYPE default::User | Issue
... SELECT
...   (INTROSPECT my_type).name;
{"default::User|default::Issue"}

5. Type Objects

Type Objects is a representation of a type in an object form on which an EdgeQL computation can be performed. Type Objects are duck-type compatible with what __type__ link returns for Object Types and with schema::Type.

Internally, at the Postgres level, type objects will be represented with a custom composite type. The compiler will generate different SQL to allow to use shapes for type objects and serialize them to JSON.

Type Objects for union and intersection types will serialize subtypes in a disjunctive normal form (DNF). That will naturally allow for type equivalence of types like Foo | Bar and Bar | Foo and allow type objects to have stable string representations and identifiers.

6. Defining Casts

We'll need to add support in DDL to define explicit and implicit type casts (something similar to CREATE CAST in SQL).

Implicit casts will define how union types are computed. E.g. if there's an implicit cast from int16 to int32, it means that the result of int16 | int32 type expression will be int32.

1st1 commented 6 years ago

@elprans @vpetrovykh feel free to add/edit if I've missed anything.

elprans commented 6 years ago

Looks great, thanks. One minor nit: IF..ELSE and ?? also produce union types.

1st1 commented 4 years ago

@elprans How do we want to approach this issue? Create a list of checkboxes/todo items to see what's left to implement? Are all of the remaining bits 1.0 material?

elprans commented 4 years ago

Adding support for basic type expressions in [IS ] and casts would be nice, we can open a separate issue for that. The rest is implemented. my_type AS TYPE is a nice-to-have and can wait.

1st1 commented 4 years ago

Please open new issues and close this one then. my_type AS TYPE can go into the 2.0 project (we'll pick it up before 1.0 if we have time).

elprans commented 4 years ago

Opened issues for the type alias and type expressions, closing this now.

edgedb / edgedb