Static languages check a program's types at compile time without executing the program. Any program whose types don't follow the type system's rules is rejected. For example, most static languages will reject the expression "a" - 1 (with C being a notable exception that allows it). The compiler knows that "a" is a string and 1 is an integer, and that - only works when the left and right hand sides are of the same type, so it doesn't need to run the program to know that there's a problem. Every expression in a statically typed language has a definite type that can be determined without executing the code.

Many statically typed languages require type declarations. The Java function public int subtract(int x, int y) takes two integers and returns a third integer. Other statically typed languages can infer types automatically. That same subtract function is written subtract x y = x - y in Haskell. We don't tell it the types, but it can infer them because it knows that - only works on numbers, so x and y must be numbers, so the function subtract must take two numbers as arguments. This doesn't decrease the "staticness" of the type system; Haskell's type system is notoriously static, strict, and powerful, and is more so than Java's on all three fronts.