Demonstrating TypeScript 0.8 type system to be unsound. The subtyping relationship is defined in a way that admits the following code that results in TypeError exception being thrown.

subtyping.v

Require Import Utf8.

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

Infix ":>" := subtype (at level 50).

Definition st {x y} f := ST x y f.

Definition unpack {a b : Set} (st : a :> b) :=
  match st with
    | ST f => f
  end.

Notation " x ~ y " := (unpack x y) (at level 50).

Definition sub_call {s x y} (p : s :> x) (f : x → y) : (s → y) :=
  fun x => f (p ~ x).

Definition sub_ret {s x y} (p : s :> y) (f : x → s) : (x → y) :=
  fun x => p ~ f x.

Definition sub_refl {a : Set} : a :> a :=
  st (fun x => x).

Definition sub_fst {a b : Set} : (a * b) :> a :=
  st (fun xy => fst xy).

Definition sub_snd {a b : Set} : (a * b) :> b :=
  st (fun xy => snd xy).

Definition sub_fun {a b p q : Set} :
  (p :> a) → (b :> q) → (a → b) :> (p → q) :=  
  fun g h => st (fun f x => h ~ f (g ~ x)).

Definition sub_fun_bad {a b p q : Set} :=
  (a :> p) → (b :> q) → (a → b) :> (p → q).

Inductive empty : Set := .

Theorem empty_absurd : empty → False.
Proof. intro H. case H. Qed.

Definition fun_rule_absurd (r : sub_fun_bad) : False :=
  let f (k : unit → empty) : empty := k tt in
    let g (i : unit * empty) : empty := snd i in
      empty_absurd (sub_call (r sub_fst sub_refl) f g).

unsound.ts

class A {}

class B extends A {
  foo(x: string) : string {
    return x + "!";
  };
}

function f1(k: (a: A) => void) : void {
  k(new A());
}

function f2(k: (a: B) => void) : void {
  f1(k);
}

f2(function (x: B) { console.log(x.foo("ABC")); });

Link to the relevant issue: http://typescript.codeplex.com/workitem/595

Link to forum discussion: http://typescript.codeplex.com/discussions/428572

Likewise, the generics are unsound: https://gist.github.com/valtron/5688638

I'm afraid I don't know the maths or language theory required to understand this, but is it any way related to what I posted here?

Are you arguing that TypeScript is fundamentally "unsound", by design, or are you saying it still needs work? (in your opinion, can it be fixed?)

Just wondering.

I've been using TypeScript on a smaller project, and I have been thrilled with the results - I realize it has problems, I ran into a few along the way, but overall, this was a much better experience than either JavaScript or C# ... it seems you get the type-checks, safety, scalability (in terms of complexity) and maintainability of C#, but only when you want it, and without breaking or inhibiting the dynamic features and "hackability" of JavaScript.

I don't know of any other language that attempts to do that. You guys know languages you would consider alternatives to TypeScript?

Thanks.

@mindplay-dk This is two years late, but PureScript. :)

I find the demonstration a bit easier to follow without the lambda:

class A {}

class B extends A {
  foo(x: string) : string {
    return x + "!";
  };
}

function f1(k: (a: A) => void) : void {
  k(new A());
}

function f2(x: B) {
  console.log(x.foo("ABC"));
}

f1(f2);