Thursday, October 04, 2012

Is TypeScript gradually typed? Part 1

If you haven't heard already, there's a new language named TypeScript from Microsoft, designed by Anders Hejlsberg and several others, including a recent alumni from my research group named Jonathan Turner. The TypeScript language extends JavaScript with features that are intended to help with large-scale programming such as optional static type checking, classes, interfaces, and modules. In this post I'll try to characterize what optional static typing means for TypeScript. There are a large number of possible design decisions regarding optional static typing, so the characterization is non-trivial. When discussing types, it's often easy to fixate on the static semantics, that is, how the type checker should behave, but we'll also need to look at the dynamic semantics of TypeScript in Part 2 of this post. The punch line will be that TypeScript is a gradually-typed language, but only to level 1. (I'll define levels that go from 1 to 3 and discuss their pros and cons.)

Static Semantics (Type System)

TypeScript has an any type. Variables and fields of this type can store any type of value. TypeScript has function types that describe the types of the parameters and return types of a function and the way in which the any type and function types interact is closely related to the design I wrote about in Gradual Typing for Functional Languages, SFP 2006. Further, TypeScript has object types to describe the types of fields and methods within an object. The way in which the any type and the object types behave in TypeScript is closely related to the system I described in Gradual Typing for Objects, ECOOP 2007.

The basic feature of any is that you can implicitly convert from any type to any and you can implicitly convert from any to any other type. For example, the following is a well-typed program in TypeScript that demonstrates converting from type string to type any and back to string.

var answer : string = "42";
var a : any = answer;
var the_answer : string = a;
document.body.innerHTML = the_answer;
On the other hand, a gradual type system acts like a static type system when the any type is not involved. For example, the following program tries to implicitly convert from a number to a string, so the type system rejects this program.
var answer : number = 42;
var the_answer : string = answer;

Next, let's look at how any and function types interact. TypeScript uses structural typing for function types, which means that whether you can convert from one function type to another depends on the parts of the function type. The parts are the parameter and the return types. Consider the following example, in which a function of type (string)=>string is implicitly converted to (any)=>string and then to (any)=>any.

function f(x:string):string { return x; }
var g : (any)=>string = f;
var h : any = g;
document.body.innerHTML = h("42");
The first conversion is interesting because, if g is called with an argument of type any, then the argument needs to be implicitly converted to the string that f expects. This is an implicit down-cast, and doesn't follow the contra-variance rule for functions that one sees in the subtyping rules for object-oriented languages. Indeed, in a gradually typed system, assignment compatibility is co-variant in the parameter type of a function, at least, with respect to the any type. The second conversion, from (any)=>string to any is not so surprising, it's just up-casting from (any)=>string to any. Interestingly, there is a third implicit conversion in this program. Can you see it? It's in the call to h. The fact that we're calling h implies that h needs to be a function (or something callable), so there's essentially an implicit conversion here from any to (string)=>any.

Next let's look at implicit conversions involving object types. Like function types, object types are also structural. Consider the following well-typed program in TypeScript, in which an object of type {x:number; y:any} is implicitly converted to {x:any; y:string}, then {x:number}, and finally to any.

var o : {x:number; y:any;} = {x:1, y:"42"};
var p : {x:any; y:string;} = o;
var q : {x:number;} = p;
var r : any = p;
document.body.innerHTML = r.y;
The assignment of o to p shows structural changes within an object type, both to and from any. The next conversion, to {x:number}, shows that the type system allows implicit narrowing of object types. Thus, the rules governing implicit conversion are quite close to the consistent-subtyping relation described in Gradual Typing for Objects. This relation combines the consistency relation that governs the static behavior of any (sometimes called compatibility) with the traditional subtyping relation of structural type systems that allows the implicit narrowing of object types. Getting back to the above example, similar to the function call at type any, TypeScript allows member access on things of type any.

The next example is not well-typed in TypeScript.

var o : {x:number; y:any; } = {x:1, y:"42"};
var q : {x:number;} = o;
var r : {x:number; y:any;} = q;
document.body.innerHTML = r.y;
The tsc compiler complains that
example.ts(3,29): Cannot convert '{ x: number; }' 
    to '{ x: number; y: any; }':
Type '{ x: number; }' is missing property 'y'
    from type '{ x: number; y: any; }'
which shows the TypeScript doesn't allow implicit widening (again in line with the consistent-subtyping relation).

To wrap up the discussion of the static semantics, let's take a look at the interaction between function types (arrows) and object types. To quote John Reynolds by way of Olivier Danvy, "As usual, something funny happens at the left of the arrow". I'm curious to see whether object narrowing is contra-variant in the parameters of function types, which is what I'd expect based on traditional subtyping relations and based on wanting a consistent design with respect to not allowing implicit widening. Consider the following example.

function f(o: {x:number;}):string { return "42"; };
var g : (o: {x:number; y:number;})=>string = f;
var h : (o: {x:number;})=>string = g;
document.body.innerHTML = h({x:1,y:2});
The conversion from f to g should be OK, because it only requires an argument of type {x:number; y:number;} to be up-cast (narrowed) to {x:number;}. However, the conversion from g to h should not be OK because it requires an argument of type {x:number;} to be implicitly down-cast (widened) to {x:number; y:number;}. Surprisingly, the tsc compiler does not give a type error for the above example! So what I said above about TypeScript disallowing implicit widening is not quite true. In many cases it disallows widening, but here we see an exception to the rule. I don't like exceptions in language design because they increase the complexity of the language. So on this one point, TypeScript differs from the design in Gradual Typing for Objects. Perhaps Jonathan can comment on whether this difference was intentional or accidental.

7 comments:

  1. Anonymous3:57 PM

    Is there any way i can just drop typescript into my already existing javascript code?

    I do have vs2012 installed and TypeScript. But everytime im trying to add it to project it just wont compile or pickup changes..

    ReplyDelete
    Replies
    1. Sorry, I don't use Visual Studio. Sounds like a good question for the TypeScript team.

      Delete
  2. A good introduction on what actually happens behind the scenes - thank you

    ReplyDelete
  3. @Anonymous - A good place to get help with TypeScript is on the StackOverflow forums: http://stackoverflow.com/questions/tagged/typescript

    @Jeremy - Covariance in the argument type, while odd to those of us who work in type systems, can get in the way of how many programmers work. By being slightly more relaxed, there's less friction between expectations and the rules being enforced. I wasn't actually part of the call for this, so Anders would be a good person to go into it in more detail.

    In general, the type system for TypeScript serves two purposes: early error detection and tooling. Because we allow working directly with JavaScript, there is no (and can be no) type safety guarantee. Instead, we aim for type utility - that the types you provide make sense in a way that helps you create software more easily and with fewer errors.

    ReplyDelete
    Replies
    1. Thanks for the reply Jonathan! I wonder if this decision is influenced by the current lack of generics in TypeScript? Often times the situations in which one needs covariance are situations that can be solved by generics.

      Regarding type safety, I thought JavaScript (and therefore TypeScript) is type safe in the same way the most dynamic languages are type safe: all errors are trapped at runtime by the language implementation. A language is not safe only in the case when there are untrapped errors. Does JavaScript have untrapped errors?

      Delete
  4. (Was showing someone this thread and just saw you'd replied to me, probably ages ago.)

    The new generics in TypeScript follow a straight-forward structural constraint style, in that they don't admit types which don't meet the constraints. Admittedly, this makes the covariant arguments a bit of anomaly where the rest of the type system enforces conformance as you'd expect.

    Originally, I believe, the covariant args came from working with class-based languages which admitted only contravariant args during method overriding. A programmer might write:

    class Parent {
    method(x: Animal): Animal { return x; }
    }

    class Child extends Parent {
    method(x: Bear): Bear { return x; }
    }

    This is technically unsound, though it's not immediately obvious (unless you're a type theoretician) why. Time will tell whether striking the balance of not getting in the developer's way with rules that are hard to understand will prove itself out in terms of utility. Early results seem to suggest that in practice this unsoundness negatively impacts developers rarely or not at all.

    ReplyDelete
  5. Anonymous4:01 PM

    A compiler flag to set the error level for contravariant arguments to silent(defalut)/warning/error would be nice.

    ReplyDelete