Is there a name for infered strong typing?

Question

In JavaScript, you can have a loosely typed language. So doing the following is acceptable:

var iterator = new TokenIterator(this.session, cursor.row, cursor.column);
var matchType;
var found = false;
var depth = {};
var i = cursor.column - token.start;
var bracketType;
var brackets = {
    ")": "(",
    "(": "(",
    "]": "[",
    "[": "[",
    "{": "{",
    "}": "{"};

It is faster and saves memory when you can strongly type an object.

But if the language doesn't support strongly typing the variable could a compiler infer the data type from the value? And then prevent that variable from becoming any other type?

So if an loosely typed object is set to false it becomes a Boolean behind the scenes. Or if it's a set to a String then it becomes a String. Then if there is code anywhere attempts to set it to a different type an error is thrown. Is there a name for this? I'd like to enable it in all of the JavaScript I write going forward.

Answer 1

I'd like to avoid the terms “strong typing”, “weak typing”, or “loose typing”, since they have no generally agreed-upon definition. Instead, let's talk about static typing.

• A language is statically typed if for any expression, I can determine the type of that expression just from looking at the source code.

• If expressions don't have a static type but the type is part of each run time value, and types are checked at run time, the language is dynamically typed. (Such a language is also called unityped or even somewhat confusingly called untyped because the static type of every expression is Any).

• If the language does not enforce static typing but allows static typing for some expressions, it is gradually typed (“optional static typing”).

Mainstream statically typed OOP languages use a combination of static and dynamic typing: the static type is just a type bound, but the runtime value may actually have a subtype.

For a statically or gradually typed language, types and type constraints may usually be provided as explicit annotations (e.g. Type variable or expression :: Type). Some languages also support type inference.

A type inference algorithm assigns type variables to expressions of unknown types. It then tries to deduce concrete types for those type variables from known facts, e.g. by examining the types of literals, by using explicit type annotations, or by examining available functions. Type inference has to be handled carefully since certain type system features (like polymorphism, subtyping, gradual typing, recursion) make it more difficult or even impossible to always perform type inference. Languages differ significantly how they handle failure to deduce consistent types. For example:

var x;
// introduce type variable $T
// type x:$T
x = 42;
// type 42:int
// unify $T = int
x = "foo";
// type "foo":string
// unify $T = string
// error because $T = int != string

// alternatively with subtyping:
// ...
// unify int <: $T
// ...
// unify string <: $T
// --> $T = LowestCommonAncestor(int, string) = object

• A statically typed language must abort with an error if it cannot infer a consistent type.
• A gradually typed language may set a type variable to Any if it cannot deduce any constraints.
• Deducing an union type (like str|int) is mostly useless since you would never see a type error. Most type inference algorithms prevent this. If a language with type inference supports union types, this is either special cased (e.g. for nullable types), or requires explicit wrapping and unwrapping for the union. Deducing union types may still be valuable internally after any type checking is done, since an union type is a better type constraint than Any.

Some statically typed mainstream OOP languages support a limited kind of type inference (C++ auto , C# var, lambdas in C# and Java, and template/type argument deduction in C++, Java, and C#). These are sufficiently limited so that type inference will never fail.

An implementation of a language such as a compiler must keep the specified behaviour of the language. If the implementation uses an optimization that changes the specified behaviour, that optimization is wrong.

One possible optimization technique for dynamically typed languages is to internally use type inference to deduce static types for some parts of the code, i.e. use gradual typing. This may result in significant performance gains. But since any optimizations must not change the behaviour of the language, it must not add any extra safety checks. If a JavaScript compiler deduces that x is an int when later you assign a string, that compiler has a bug.

If you want a language that disallows assigning different types to the same variable, that language isn't JavaScript. TypeScript is a super-set of JavaScript, i.e. any syntactically valid JavaScript program is a syntactically valid TypeScript program. But since TypeScript is a different language, it can add type checking rules. In particular, the var x = 42; x = "foo" example will generate a warning or error. However, TypeScript transpiles to JavaScript and the type checking is used only as a developer productivity tool, not as a compiler optimization aid.

This is called “TypeScript is a different language than JavaScript”.

TypeScript's type system can be characterized as “gradual typing or (depending on settings) static typing with type inference”.