Motivating example

Recently, I came across different errors in Typescript which bothered me. Although I am not an expert in type theory and I love Typescript, let me explain what I think could be made better.

A method returns an IIterable<TreeElement>, where the TreeElement is called a type parameter. The method fromArray is generic and accepts an argument of type T[] and returns an IIterable<T> for any T.
Resharper 9. gives me the following suggestion.

When I accept the suggestion, I get the following new error.

Why is Typescript, like many other languages, unable to perform such correct type checking?

It is because type checking is not just about verifying types. It is really about proving program properties. For that, I believe that engineers can really learn a lot from Academia.

First, let me show that it is possible to correctly type-check the sentence above.

How to solve the type equation

For example, with the first example, it gives the following type equations:

TreeElement[] <: T[]
IIterable<TreeElement> >: IIterable<T>

This means that

1. An array of TreeElements should be viewed as an array of T to pass to the method .fromArray
2. The result, and IITerable<T> should be viewed as an IIterable of TreeElements

A trivial solution exists: T = TreeElement. Is it really the only solution? How to solve it in the general case?

A word about variance and contravariance

The type parameter of an array is nor covariant nor contravariant. This means that:

1. No covariance: Covariance would mean that an array of apple is an array of fruits. If it were, then we could put a cherry in the array of fruits and the original array would not be an array of apple anymore.
   a =  [,,,] is an array of apples.
   An apple is itself a fruit.
   But if we say, to abstract, that a is also an array of fruits, we would put a cherry at the first element.
   a[0] = 
   but then a would be  [,,,] which is NOT an array of apples.
2. No contravariance. Contravariance would mean that an array of fruits is also an array of apples. This is obviously wrong.

Therefore the first equation yields the unique solution T = TreeElement which satisfies the second.

Without the explicit type parameter?

The equations become trickier if we remove the explicit type parameter, as the suggestion tells it. In this case, the array can be an array of anything, let's say an array of U where U is an unknown type variable.

U[] <: T[]
IIterable<TreeElement> >: IIterable<T>

Because there is no way to define covariance and contravariance in Typescript (as of 1.4), the only way IIterable<T> can be a sub-type of IIterable<TreeElement> is that T = TreeElement. Filling this solution to the first, we get:

U[] <: TreeElement[]

where we have the result that U should also be TreeElement for that to work. So this should work as well...

Why does Typescript fails there?

Like many other examples, Typescript does not set up type equations or type constraints. It solves equations in a greedy manneer, without back-tracking. Although this is viable for small programs, this does not scale and it's a shame.

Alternatives to Typescript?

if not developping with Visual Studio, I would recommend modern languages such as Scala, which now can compile to Javascript.

The type checker does this thinking and we can define the following statements without error.

class IIterable[T]
object IIterable { def fromArray[T](input: Array[T]): IIterable[T] = ??? }
def testMethod: IIterable[TreeElement] = IIterable.fromArray(Array())

It will correctly infer the missing type parameter for the array. Besides, thanks to the huge collection available, no need to reinvent the wheel.

But what are types?

Although the question of solving type equations is trivial here, this question is less trivial in general, because if the type system is sound and complete, types can generally encode arbitrary mathematical notions. Even without predicates types, like a simple int {x=> %2=0 x=>x>3} x , we can encode many mathematical problems in types which the compiler will have to solve, and sometimes will fail.

This is why it's hard.

Conclusion: Please add a modern type checker into Typescript.

Here is what is currently missing in Typescript 1.4

• Support for abstract classes.
• Support for type constraints, like mentionned above.
• A solver for type constraints.
• Support for F-bounded polymorphism.
• Support for traits or mixins.

It's worth it for many reasons:

• Types help refactoring
• Types provide guarantees about your program
• Types structure any home-made library and make component reusable
• Types provide clever code completion
• ...

Useful references:

- A Core Calculus for Scala Type Checking, 2006, Vincent Cremet, François Garillot , Sergueï Lenglet, Martin Odersky