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.

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.

The guilt of impurity

ML is guilty of impurity, so it can’t escape from a restriction. In other words, the presence of mutable ref cells and parametric polymorphism in ML requires the language to be controlled by the value restriction.

Here is a small example which shows that the ML type system is unsound without the value restriction. This allows putting a value of int where we expect a value of type string.

val r = ref NONE (* val r: 'a option ref *)
val _ = r := SOME "hi"
val i = 1 + valOf (!r)

ML fixes this by enforcing the value restriction: a variable-binding can have a polymorphic type only if the expression is a variable or value. ref NONE is a function call which belongs to neither, so the type of ref NONE is filled with dummy types that are no longer usable.

But there is a downside too. The value restriction can cause problems even when we don’t use mutable cells. The type-checker does not know that Lisp.map is not making a mutable reference, so it must impose the value restriction.

val pairWithOne = List.map (fn x => (x, 1))

To circumvent the value restriction, we must wrap it in a function binding (η-conversion).

fun pairWithOne xs = List.map (fn x => (x, 1)) xs

Haskell is free from the guilt of impurity. In Haskell, because IORefs can only be created (and used) in the IO monad, no such restriction is necessary. This is another reason why we love purity of Haskell.