In a dynamically typed system, values have types at runtime but variables and functions do not. In a statically typed system, variables and functions have types known and checked at compile-time. E.g. in Python x can be anything; at runtime, if it is 1 it’s a number and if it is "foo", it’s a string. You would only know which type x was at runtime, and it could be different each time you ran the program. In a language like Java, you would write int x if x was to be a number, and you would know at compile time that x always has to be an int.

“Explicit” and “implicit” types both refer to static type systems. The defining characteristic of a static system is that the types are known at compile time, but not necessarily that they have to be written out. In Java, types are explicit–you have to write them out. So in Java, a method might look something like:

public int foo(String bar, Object baz) { ... }

The types are both known at compile time (static) and written out (explicit). However, there are also languages that do not force you to write the type out. They can infer the type of a function from its body and how it is used. An example would be OCaml, where you can write something like:

let foo x = x + 1

Since you used +, OCaml can figure out that x has to be an int all on its own. So the type of foo (foo : int -> int) is known at compile time, just like the Java example. It is entirely static. However, since the compiler can figure out what the types have to be on its own, you do not have to write them out yourself: they’re implicit.

In short: whether a type system is explicit or implicit is a property of static systems. It is a completely different question from whether a type system is dynamic or static.

Often, you have type systems that are at times explicit and at times implicit.

For example, I believe C# lets you infer types using the var keyword. So instead of writing int x = 10, you can write var x = 10 and the compiler figures out that x has to be an int. C++ does something similar with auto. These systems are usually explicit but have some inference.

On the flipside, there are systems that are usually implicit but sometimes force you to write out a type signature. Haskell is a great example. Most of the time, Haskell can infer the types for you. However, sometimes you can write code that is ambiguous like show . read, where Haskell cannot figure out the types on its own. In this case, you would be forced to explicitly specify the type of either show or read. Additionally, some more advanced features of the type system (like rank-n polymorphism) make inference undecidable–that is, it is not guaranteed to halt. This means that code using this feature often needs explicit type signatures.

• static vs dynamic describes when types are checked (more or less at compile time or at execution time)

• nominal vs structural describes when two types are considered the same.

(And there are variations, the best known is the variant of structural typing which considers only what is used instead of the whole type known as duck typing).

The four combinations (static nominal, static structural, dynamic nominal, dynamic structural) are possible, and languages quite often aren’t purely in one class but have aspects which are in others.

For instance, the type systems of C++ is static, mostly nominal but structural when you consider templates (and you can consider part of the problems around concepts in C++ as a conflict between those wanting to from duck typing to a full form of structural typing and those wanting to go to nominal typing). And the use of classes and inheritance allows to use a dynamic and nominal typing in some cases.

Language which a dynamic type systems often are using structural typing, but CLOS as nominal aspects.

Structural: Type compatibility is based on the type structure, e.g. in C if 2 variables are struct types with different names but the same structure, then their types are compatible.

This is usually not the case. Structural typing means that B is a subtype of A if it can satisfy A‘s interface. This usually means having members with the same name; not just the same structure in memory.

This differs from nominative typing that requires super-types to be specified on declaration.

The best explanation I’ve seen of the distinction between (actually subsumption of) dynamic and static type systems is in this blog post by Bob Harper:

• Dynamic languages are static languages

Its main point could be summarized as:

• dynamic languages are those static languages with only one type