What is the motivation for the current subtyping rule on functions? AFAIK, the 0.8 language spec has both of the following rules:

(A :> B) |- (A -> R) :> (B -> R)

(B :> A) |- (A -> R) :> (B -> R)

The first of these is not sound. I created a small TS example that demonstrates this. There is also a little Coq formalization that interprets "A :> B" as "there exists a function from A to B" and shows that the first rule above leads to an inconsistency, while the correct rule is:

(P :> A), (B :> Q) |- (A -> P) :> (B -> Q)

You're right that allowing both co- and contra-variance in the parameter position isn't sound.  This is actually intentional and also somewhat controversial (one example is http://siek.blogspot.com/2012/10/is-typescript-gradually-typed-part-1.html).

The type system in TypeScript has a different set of motivations that is often the case in other type systems.  In TypeScript, the motivations tend to favor tooling and ability to express common idioms in JavaScript over being type safety or soundness.  It also tends to favor simplicity in the type system.

The classic one that Java and C# is that arrays should actually be invariant.

var array1: {foo:number;}[] = [{foo: 1}];
var array2: {}[] = array1;

array2[0] = {bar: "bar"};

console.log(array1[0]);

 In order to prevent issues like this, you have to make your type system more complex (by adding, for example, variance or in/out annotations on your generics).  TypeScript instead tries to simplify and give the user a fairly straightforward story, at the expense that there are some cases that become less safe. 

Toyvo,

"A :> B" as "there exists a function from A to B"

do you mean "A -> B"?

The way I've seen it is "A <: B" meaning A is a subtype of B.

ShiqiCao, please refer to the Coq file. I am not overly familiar with type systems including subtyping, as you see I was even confused about the standard notation; but I like things being formal, and at a first glance my intuition for subtyping would be this:

Inductive subtype (a b : Set) : Set :=
| ST : (a -> b) -> subtype a b.

In plain words, this says: we can demonstrate that A is a subtype of B by providing a function (as in math) from A to B. That is, A contains all the information in B and more. 

jonturner, thanks for your reply. I would question the assumption that a sound type system would hinder your scenarios - ability to express JavaScript idioms, and hinder tooling. I also doubt that a sound type system would be significantly more complex, and I would argue you do not need to expose any of the additional complexity to the user.

For example, to avoid the need for variance annotation on generics, you could simply exclude rules that depend on it from the formalized subtyping relation. It is a strategy works quite well - when the compiler is in doubt, assume a NO answer. In the limit, it could also achieve removing subtyping altogether. You can then recover JavaScript idioms by providing an explicit "cast" primitive compiled to the identity function. That is, when the user is certain a cast is safe, but TypeScript's approximation of subtyping fails to infer safety, the user inserts an explicit cast.

I have a strong preference for an explicit cast, because in this setup a compiling cast-free program gives me a static guarantee there will be no type errors. In current TypeScript the fact a program compiles tells me nothing about type errors - they can still manifest themselves for certain runs of the program.

I am speaking from experience. In our company we have developed an F#->JavaScript platform, WebSharper, and have been quite happy with the explicit cast over the years. This is indeed how F# works - a sound core typesystem with use-at-your-own-risk extensions. I have not had any problem expressing JavaScript idioims. Our programs are typically written mostly in the sound core of F#, and casts are inserted at the FFI boundary to make sense out of untyped JavaScript and bring it into the typed setting.

If anything, we have felt the need for more *safety*, not more flexibility. For example, we are now looking at implementing a contract system to check at runtime that untyped JavaScript fragments preserve the announced typing, in the spirit of Findler and Felleisen (http://www.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf).

The design choices here (and Anders may even weigh in) are about balance rather than removing all unsafe activity.  JavaScript code tends to be, especially to many coming from languages like F#, more on the fast and loose side of coding. 

The more we require users to use casts to port code over, the less it feels like coding in helpful superset of JavaScript and the more it feels like a restrictive, type-heavy language.  We'd rather avoid that and keep the language easier to use for doing the types of things JavaScript is good at, even if it means risking some type safety in some cases.  The hope is the holes it opens up in the type system are rarely felt in practice, but we gain a net positive by having a lighter weight type system.

That said, TypeScript won't be everyone's cup of team.  There are other languages that compile to JavaScript that favor a more strict system, like your own project, which may be a better fit for programmers who want that extra level of assurance a stricter type system gives them.

Just count my feedback as a vote for a sound type system. I think I understand your arguments, but from my (biased) position, I fail to see any benefit at all in allowing implicit TS holes. See also some more or less informed discussion on LtU: http://lambda-the-ultimate.org/node/4612.