![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
Table of Contents for Programming Languages: a survey
"A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute." – Benjamin Pierce
note: other sorts of compile-time analysis are called "static analysis"
note: success typing does not prove the absence of (bad) behavior, but rather its presence (less conservative, looks for proofs of bad behavior rather than proofs of correctness)
"The type of a function specifes (partially) what it does. Although weak as a specifcation language, static types have compensating virtues: they are
As a result, static type checking is by far the most widely used verifcation technology today.
Every type system excludes some "good" programs, and permits some "bad" ones.
For example, a language that lacks polymorphism will reject this "good" program:
f :: [Int] -> [Bool] -> Int f is bs = length is + length bs
Why? Because the length function cannot apply to both a list of Ints and a list of Bools. The solution is to use a more sophisticated type system in which we can give length a polymorphic type. Conversely, most languages will accept the expression 'speed + distance' where speed is a variable representing speed, and distance represents distance, even though adding a speed to a distance is as much nonsense as adding a character to a boolean.
...
The type-system designer wants to accommodate more good programs and exclude more bad ones, without going overboard and losing the virtues mentioned above. "
-- Oleg Kiselyov, Simon Peyton Jones, Chung-chieh Shan, http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf
provably: Sound and/or complete Tract able typechecking Tractable type inference
Expressive
ability for the typical program to simulate it (including type inference, if that is provided) in their head
trying to hit all the criteria above
also, side effect of academia: in academia it's better for your career to do something:
so we get (a) a proliferation of (b) overly abstract work that is (c) uses intimidatingly powerful math.
first-class functions; second-order types; dependent types; union types, intersection types; etc
and foundational crisis in math, etc
http://siek.blogspot.com/2012/10/is-typescript-gradually-typed-part-1.html gives some examples that should be included somewhere:
" 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, ...
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;
...
Consider the following [legal in typescript] example...
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;
...
which shows the TypeScript? doesn't allow implicit widening (again in line with the consistent-subtyping relation).
...
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.
"
see also https://typescript.codeplex.com/discussions/428572 for a more formal discussion
great post: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html
i skipped the first few sections and started reading at section "Operational Semantics".
It covers big-step and small-step operational semantics, and also the common notation for type systems, each with a very concise and easy example.
