TypeScript: Best Common Type

TypeScript tries to find the best common type when a type inference is made from several expressions.

Let’s experiment a bit with following types. Square is a subtype of Shape and Circle is also a subtype of Shape.

class Shape {
    color: string;
}

class Square extends Shape {
    sideLength: number;
}

class Circle extends Shape {
	radius: number;
}

The type of xs1 is Shape[] because Shape is the common supertype of Shape, Square and Circle. However, surprisingly the type of xs2 is not Shape[] though Shape is the common supertype of Square and Circle. Here the type of xs2 is (Circle | Square)[] because there is no object that is strictly of type Shape in the array.

var xs1 = [new Shape(), new Square(), new Circle()];
var xs2 = [new Square(), new Circle()];

You can override this type by annotating the type explicitly with Shape[].

var xs3: Shape[] = [new Square(), new Circle()];

Now let’s see how the return type of a function is inferred when the function returns two values with different types.

function createShape1(square: boolean) {
    if (square) {
        return new Square();
    } else {
        return new Shape();;
    }
}

The return type of createShape1 function is Shape as expected because Shape is the common supertype of Square and Shape.

function createShape2(square: boolean) { // Type Error
    if (square) {
        return new Square();
    } else {
        return new Circle();
    }
}

However, if we change the return value of else branch to new Circle(), createShape2 function no longer type checks. TypeScript complains about “error TS2354: No best common type exists among return expressions.” It fails to find the best common type though it can be inferred as either Square|Circle or Shape.

We can satisfy the type checker by giving an explicit type. The return type can be either Square | Circle or Shape.

function createShape3(square: boolean): Square | Circle {
    if (square) {
        return new Square();
    } else {
        return new Circle();
    }
}

function createShape4(square: boolean): Shape {
    if (square) {
        return new Square();
    } else {
        return new Circle();
    }
}

From the examples above, we can see that the type inference rule of TypeScript is not orthogonal. When you mix multiple types in an array, TypeScript finds the best common type that is the union of the types of the element expressions. But when a function mixes multiple return types in return values, it finds the best common type that is the first supertype of each of the others.

You can see the difference in the type inference rules taken from the TypeScript 1.4 specification.

Array Type

  • If the array literal is empty, the resulting type is an array type with the element type Undefined.
  • Otherwise, if the array literal is contextually typed by a type that has a property with the numeric name ‘0’, the resulting type is a tuple type constructed from the types of the element expressions.
  • Otherwise, the resulting type is an array type with an element type that is the union of the types of the element expressions.

Function Return Type

  • If there are no return statements with expressions in f’s function body, the inferred return type is Void.
  • Otherwise, if f’s function body directly references f or references any implicitly typed functions that through this same analysis reference f, the inferred return type is Any.
  • Otherwise, if f is a contextually typed function expression (section 4.9.3), the inferred return type is the union type (section 3.4) of the types of the return statement expressions in the function body, ignoring return statements with no expressions.
  • Otherwise, the inferred return type is the first of the types of the return statement expressions in the function body that is a supertype (section 3.10.3) of each of the others, ignoring return statements with no expressions. A compile-time error occurs if no return statement expression has a type that is a supertype of each of the others.
Advertisements

Thoughts on Intersection Types

Facebook’s Flow is a static type checker, designed to find type errors in JavaScript programs. Flow’s type system is similar to that of TypeScript in that it is a gradual type system and relies heavily on type inference to find type errors.

One interesting feature of Flow that is missing in TypeScript is intersection types. For example, in Flow you can represent a function which takes either Bar or Foo with intersection types.

/* @flow */
class Foo {}
class Bar {}
declare var f: ((x: Foo) => void) & ((x: Bar) => void);
f(new Foo());
f(true); // Flow will error here.

The function f has type ((x: Foo) => void) & ((x: Bar) => void). The notation A & B represents the intersection type of A and B, meaning a value of A & B belongs to both A and B. We can capture this intuition with the following sub-typing rules:

[1] A & B <: A
[2] A & B <: B
[3] S <: A, S <: B ~> S <: A & B

In Flow, intersection types are primarily used to support finitary overloading. func takes either number or string and returns nothing. This can be represented as intersection of two function types as in the following:

type A = (t: number) => void & (t: string) => void
var func : A;

However, TypeScript doesn’t need intersection types to support finitary overloading because it directly supports function overloading.

interface A {
  (t: number): void;
  (t: string): void;
}
var func: A

Or in TypeScript 1.4, you can represent the same function more succinctly with union types.

interface A {
  (t: number | string): void;
}
var func: A

This is not a coincidence! Intersection types are the formal dual of union types. When an arrow is distributed over a union, the union changes to an intersection.

(A -> T) & (B -> T)  <:  (A | B) -> T

So it means the following two types are equivalent:

  • (t: number | string): void
  • (t: number) => void & (t: string) => void

So far intersection types seem redundant once a language have union types (or vice versa). However, there are some real world use cases where intersection type are actually required.

Let’s check how ES6’s new function Object.assign is typed in TypeScript (lib.core.es6.d.ts).

interface ObjectConstructor {
    /**
      * Copy the values of all of the enumerable own properties from one or more source objects to a 
      * target object. Returns the target object.
      * @param target The target object to copy to.
      * @param sources One or more source objects to copy properties from.
      */
    assign(target: any, ...sources: any[]): any;
    ...
}

Currently, both the argument types and the return type of Object.assign is any because the type system of TypeScript can’t represent the type correctly. Let’s try to type this function correctly. First, we can make this function polymorphic by assigning A to target and B[] to sources.

Object.assign<A,B>(target: A, ...sources: B[]): ?;

Okay. We are now stuck with the return type. The return value has all the properties of both A and B. It means with structural typing, the return value is a subtype of both ‘A’ and ‘B’ (belongs to both A and B). Yeah! We need intersection types to represent this value. So the correct signature of this function is:

Object.assign<A, B>(target: A, ...sources: B[]): A & B;

The same reasoning also applies to mixins.

mixins<A,B>(base: { new() :A }, b: B}) : { new(): A & B} 

TypeScript developers are still discussing on adding intersection types. Many people think that there are not enough compelling use cases. Also intersecting two primitive types like string & number makes no sense, which makes intersection types less desirable.

I think adding intersection types to TypeScript makes the language more consistent because these two concepts are the dual of each other and can’t really be separable. But I also think that the language design must be conservative. So let’s just wait until we have more compelling reasons to add intersection types.

A First Look At TypeScript Type System

TypeScript type system is just a formalisation of JavaScript types. You can represent runtime types of JavaScript statically by annotating them in the source code. But at the same time it is quite unique compared to other programming language type systems as it is optional and not “provably type safe”.

  • Optional

Because TypeScript is a strict superset of JavaScript, it must accept all legal existing JavaScript code as valid TypeScript code. This means that TypeScript can’t enforce programmers to annotate every type with type annotations.

With optional typing, you can incrementally change your existing JavaScript code into TypeScript code. As you add more type annotations, you get more help from the toolset.

  • Not “provably type safe”

TypeScript type system is not for correctness safe or performance safe because it is impossible to guarantee the correctness of JavaScript with only optional typing. Traditionally, a type system that is unsound is useless as it proves nothing.

However, TypeScript type system is still meaningful because it provides information needed to implement static analysis, code completion and refactoring capabilities in tools. So we can say that TypeScript type system is for tooling safe.

TypeScript also supports type inference and structural typing to help programmers write type annotations more succinctly. It is still evolving by introducing Generics, Tuple Type, Union Type and Type Alias. I will talk more about these in later articles.

A Hindley-Milner type inference implementation in OCaml

Hindley–Milner (HM) is a classical type system for the lambda calculus with parametric polymorphism. If you want to know what HM is and why it is cool, please read Daniel Spiewak’s article “What is Hindley-Milner? (and why is it cool?)

There are multiple implementations of HM in many different languages.

I reimplemented the algorithm in OCaml guided by Scala and Python implementations. All these implementations are based on the Modula-2 implementation of the Cardelli 1987 paper. Because the algorithm described in the paper depends on mutable states for optimization, it is not easy to implement it directly in a purely functional programming language like Haskell.

The program implements a small functional programming language with no concrete syntax. The language consists of identifier, lambda, application, let and let rec. The type inference algorithm reconstructs the type of the given example expressions in the context of some predefined types. The program produces the following results when executed:

letrec factorial = fn n => cond zero n 1 times n factorial pred n in factorial 5 : int
fn x => pair x 3 x true : Type mismatch bool != int
pair f 4 f true : Undefined symbol f
let f = fn x => x in pair f 4 f true : (int * bool)
fn f => f f : Recursive unification
let g = fn f => 5 in g g : int
fn g => let f = fn x => g in pair f 3 f true : (a -> (a * a))
fn f => fn g => fn arg => g f arg : ((c -> d) -> ((d -> b) -> (c -> b)))

The age of type inference

Main stream languages have been continuously adopting good ideas from functional programming. Java and C# has gradually added programming constructs such as garbage collection, parametric polymorphism, lambda expressions and closures.

In spit of these ongoing endeavors, dynamically typed languages such as Python, Ruby, JavaScript and even Clojure are gaining popularity over statically typed languages. These languages are concise and elegant, and you don’t need to spend your precious time writing complex type annotations.

To regain the power stolen by dynamic languages, statically typed main stream languages have begun to introduce local type inference. For example, C++11 added auto keyword, which directs the compiler to use the initialization expression of a declared variable to deduce its type. Java and C# also added similar constructs.

#include <iostream>
 
using namespace std;
 
int main( )
{
    int count = 10;
    int& countRef = count;
    auto myAuto = countRef;
 
    countRef = 11;
    cout << count << " ";
 
    myAuto = 12;
    cout << count << endl;
}

Unfortunately, the power of type inference in these languages are very limited. Because type inference is tightly coupled with type system, we can’t introduce global type inference such as Hindler-Milner to these languages. Because of compatibility, it is practically impossible to retrofit the type system to allow global type inference.

I think it is time to design and implement a new statically typed language which looks almost the same to dynamic typed languages. Developers from Python, Ruby and JavaScript must be able to use it without learning how to put types all over the program. Dynamic vs Static typing controversy is meaningless if you don’t need to annotate any type in both languages. A statically typed language is always better because it detects errors at compile time for free.

Daniel Spiewak expects in his talk that statically typed languages with structural type systems (necessary for type inference) will dominate in the future and I totally agree with him.