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
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:
// 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
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.
x is an int when later you assign a string, that compiler has a bug.
TypeScript's type system can be characterized as “gradual typing or (depending on settings) static typing with type inference”.