RFC: Formal Type System

[andylokandy]

RFC: Formal Type System

Motivation

1. Detect as many as possible type errors in the SQL planning phase.
2. Formal definition helps type system be complete and avoid pitfalls.
3. Ease the way to declare function type.
4. Predictably insert cast when necessary.
5. Remove the legacy dirty typing hacks.

Type Definition

Except for the obvious primitives and generic container types, there are a special Any, which is the supertype of all other types, and a Hole, which is the subtype of all other types and has no instance value (void type). Variadic type is similar to Array<Any> and only used in variadic functions.

Primitive	Container	Top Type	Bottom Type
Boolean	Array<T>	Any	Hole
String	Nullable<T>
Date
Timestamp
Object
Variant
Variadic
UInt8
UInt16
UInt32
UInt64
Int8
Int16
Int32
Int64
Float32
Float64

Type Check Mechanism

The type information that helps detect type errors is mostly from function signature. Let's consider the following expression:

1 + 'foo'

The type checker will firstly desugar it into a function call:

plus(1, 'foo')

and the type checker can easily infer that:

1 :: Int8
'foo' :: String

also, the function plus has some overloads:

plus(Int8, Int8) -> Int8
plus(Int16, Int16) -> Int16
plus(Int32, Int32) -> Int32
plus(Timestamp, Timestamp) -> Timestamp
...

we can easily find that plus(Int8, String) doesn't unify with any of the overloads, so the type check can raise an error stating that:

1 + 'foo'
  ^ function `plus` has no overload for parameters `(Int8, String)`

  available overloads:
    plus(Int8, Int8) -> Int8
    plus(Int16, Int16) -> Int16
    plus(Int32, Int32) -> Int32
    plus(Timestamp, Timestamp) -> Timestamp

On the other hand, a function can accept a more general type as an argument, and the type checker can check if the argument upcasts to the function's parameter type.

Consider the following definition of function is_null:

is_null(Nullable<Any>) -> Boolean

The type checker should proof that String can be upcast to Nullable<Any>, and thus the following expression should be valid:

is_null('foo')

The detailed upcast rule will be explained in the following section.

Upcast Rule

There are only a few rules necessary to define sound and complete subtype relations ('A is a subtype of B' is equivalent to 'A upcasts to B'):

Self Reflexity

All types are subtype of itself:

Top Type

All types can be upcast to Any:

Bottom Type

Hole can be upcast to any type:

Introduce Nullable

Type can be wrapped by nullable (which means to drop the guarantee that the type is not null):

Covariant

Nullable<T> upcasts to Nullable<U> if and only if T upcasts to U. Same as Array<T>.

Transitivity

If T upcasts to S and S upcasts to U, we infer that T upcasts to U.

Number coercion

UInt8 -> UInt16 -> UInt32 -> UInt64
Int8 -> Int16 -> Int32 -> Int64
UInt8 -> Int16
UInt16 -> Int32
UInt32 -> Int64
Float32 -> Float64
Int32 -> Float32
Int64 -> Float64

Special literal type

[] :: Array<Hole>
NULL :: Nullable<Hole>

number literals use the fittest type:

1 :: UInt8
-1 :: Int8
256 :: UInt16

Example

Given a function definition of is_all_null:

is_all_null(Array<Nullable<Any>>) -> Boolean

then check the following expression:

is_all_null(['foobar'])

and because we know the type of literal ['foobar']:

['foobar'] :: Array<String>

now we can start trying to prove that Array<String> upcasts to Array<Nullable<Any>>:

1. String -> Any
   (by top-type rule)

2. Nullable<String> -> Nullable<Any>
   (by covariant rule and obligation (1.))

3. String -> Nullable<String>
   (by introduce-nullable rule)

4. String -> Nullable<Any>
   (by transitivity rule and obligation (2.) and (3.))

5. Array<String> -> Array<Nullable<Any>>
   (by covariant rule and obligation (4.))

Q.E.D

Function Overload

A function can have multiple overloads. The type checker will try to find the most specific overload to check the function call.

Function overloads must not be ambiguous, which formally speaking is that there must be at most one overload that can be used to check the function call for every possible input type.

We have an exception rule about allowing ambiguous overloads. Consider the following example:

foo(Any, Any) -> Boolean
foo(Boolean, String) -> Boolean

It's obvious that the latter overload is more specific than the former overload, which means for a function call foo(TRUE, 'abc') the type checker can use the latter overload. So ambiguity is allowed in this case.

In general, there are two forms of forbidden ambiguous overload:

1. Unrelated overlap

   foo(Nullable<Array<Int8>>) -> Boolean
   foo(Array<Any>) -> Boolean
   

   Since Array<Int8> upcasts to both Nullable<Array<Int8>> and Array<Any>, for an input value with type Array<Int8> the type checker can't decide which overload to use. So an error will be raised.

2. Unordered overlap

   foo(Boolean, Any) -> String
   foo(Any, Boolean) -> String
   

   For a function call foo(TRUE, TRUE), the type checker can not decide which overload to use. So an error will be raised.

Checking ambiguity

Ambiguity is checked once the function overloads are registered. To check ambiguity, the type checker will compare the overlap of parameters.

The following cases are allowed:

• Two overloads don't overlap at all.
• Some parameters overlap, but one overload is always subtype of the other.

and the following cases are forbidden:

• Two overloads overlap, and subtype order differs on parameters, or some parameter isn't a subtype of each other at all.
• All parameters are identical.

To test overlap, we use the following rules:

1. Given two types T and U.
2. Generate all subtypes of T and U, by reversely applying the upcast rule, but don't use the rule of top-type, bottom-type, and self-reflexity.
3. If any subtypes of T upcast to U, T overlap with U, and vice versa.

Example

Let's think of the example we've seen before:

foo(Nullable<Array<Int8>>) -> Boolean
foo(Array<Any>) -> Boolean

To see if they are ambiguous, we need to test if Nullable<Array<Int8>> and Array<Any> overlap. And at first, we generate their subtypes:

// subtypes of Nullable<Array<Int8>>:
Array<Int8>

// subtypes of Array<Any>:

since Array<Int8> upcasts to Array<Any>, we proved they overlap.

And since Nullable<Array<Int8>> and Array<Any> aren't subtypes of each other, it's a forbidden case.

Runtime Types

The types described above all have related runtime types (physical type). For example, Boolean is related to runtime type BoolScalar, BoolArray.

If T upcasts to U, it's guaranteed that impl From<T::RuntimeType> for U::RuntimeType.

Detailed designs are still under investigation. So currently the type checker is only a linter.

[leiysky]

AFAIK, we don't have a mechanism to list overloads of a function. The argument types are checked(even optionally) with some hard coded rules when instantiating the Function object.

Do you have any idea about this?

[andylokandy]

I prefer to add an additional method in Function trait to list the function signatures.

In the future, we may automatically generate the signature.

[sundy-li]

An extra method to list the function signatures is a good idea.

But some aggregate/scalar functions support variadic arguments, eg: in, ignore, char, concat, tuple, field, retention. It's hard to list all combinations.

StarRocks used a python config file to save the signatures, but I think it's not a good idea to save it in other lang.

[andylokandy]

But some aggregate/scalar functions support variadic arguments, eg: in, ignore, char, concat, tuple, field, retention. It's hard to list all combinations.

can variadic arguments be treated as Array?

[sundy-li]

can variadic arguments be treated as Array?

I'm afraid not. Variadic arguments may not be the same type. Even they are same type T, Array(T) vs a, b, c are different memory layout.

Maybe we can ignore these variadic cases and just throw the hard code error message to users if type mismatch.

[b41sh]

In addition to Array<T>, we also have an Array type, which is actually a Variant type, but restricts that the data must be put into an array.

[andylokandy]

In addition to Array, we also have an Array type, which is actually a Variant type, but restricts that the data must be put into an array.

Is it Array<Any>?

[b41sh]

In addition to Array, we also have an Array type, which is actually a Variant type, but restricts that the data must be put into an array.

Is it Array<Any>?

yes, we can treat it as Array<Any>

[andylokandy]

I'm afraid not. Variadic arguments may not be the same type. Even they are same type T, Array(T) vs a, b, c are different memory layout.

Added Variadic to the type list. Should solve the problem.

[Xuanwo]

Convert this RFC to discussions for better communication.

@andylokandy We can create a tracking issue if we have tasks to track. In which, we can refer to this RFC.

[Xuanwo]

Will we have Uint128 in the future?

[usamoi]

No overlap seems like a very strong restriction. Array<Int8> and Array<String> cannot be two overload parameters of a function since the literal [] is an inhabitant of Array<Hole>. Only nonnullable primitives could be overload parameters.

[andylokandy]

In the process of overlap checking, the rule of bottom-type will not be taken.

[usamoi]

@andylokandy But if a Array<Hole> is passed to a function with two overloads Array<Int8> -> Array<Int8> and Array<String> -> Array<String>, which overload is picked?

[andylokandy]

Good catch! Since that, we have to apply the bottom-type, for instance, your example should throw an error unless a overload accepting Array<Hole> is provided.