What concept is for a name referring to different types at different points in execution?

Question

In programming language theory, which concept means that a name can refer to values of different types at different points of execution of a program,

• dynamic typing,
• implicit i.e. inferred typing, defined as opposed to explicit i.e. manifest typing,
• something else?

Let me explain the above question.

1. My question comes from reading following two sources.

   • From Wikipedia https://en.wikipedia.org/wiki/Programming_language#Static_versus_dynamic_typing

     Statically typed languages can be either manifestly typed or type-inferred. In the first case, the programmer must explicitly write types at certain textual positions (for example, at variable declarations). In the second case, the compiler infers the types of expressions and declarations based on context. Most mainstream statically typed languages, such as C++, C# and Java, are manifestly typed. Complete type inference has traditionally been associated with less mainstream languages, such as Haskell and ML. However, many manifestly typed languages support partial type inference; for example, Java and C# both infer types in certain limited cases.[48] Additionally, some programming languages allow for some types to be automatically converted to other types; for example, an int can be used where the program expects a float.

     Dynamic typing, also called latent typing, determines the type-safety of operations at run time; in other words, types are associated with run-time values rather than textual expressions.[47] As with type-inferred languages, dynamically typed languages do not require the programmer to write explicit type annotations on expressions. Among other things, this may permit a single variable to refer to values of different types at different points in the program execution. However, type errors cannot be automatically detected until a piece of code is actually executed, potentially making debugging more difficult. Lisp, Smalltalk, Perl, Python, JavaScript, and Ruby are dynamically typed.

     In "this may permit a single variable to refer to values of different types at different points in the program execution", is it correct that "this" means implicit typing?

     So does it imply that it is implicit typing instead of dynamic typing which "may permit a single variable to refer to values of different types at different points in the program execution"?

   • From https://pythonconquerstheuniverse.wordpress.com/2009/10/03/static-vs-dynamic-typing-of-programming-languages/

     In a dynamically typed language, every variable name is (unless it is null) bound only to an object.

     Names are bound to objects at execution time by means of assignment statements, and it is possible to bind a name to objects of different types during the execution of the program.

     Does it imply that it is dynamic typing which "may permit a single variable to refer to values of different types at different points in the program execution"?

2. In order to answer the above questions, some counterexameples may help. Specifically,

   • Can you give an example when a programming language is dynamic typing, but a name is not allowed to refer to values of different types at different points of execution of a program?

   • Can you give an example when a programming language is implicit typing, but a name is not allowed to refer to values of different types at different points of execution of a program?

Answer 1

A couple of things would fit the bill: polymorphism and dynamic typing.

Polymorphism

Say you have a polymorphic function, first:

first : (A, B) -> A
first (a, b) = a

At runtime, the variables a and b may refer to values of different types on different invocations. e.g. first (1, 'a') and first ("Fred", 42). Polymorphic means many forms/types.

Dynamic typing

Dynamically typed languages also have variables that refer to values of different types at runtime. This happens for functions like first above but also in other situations like:

$ python
>>> a = "hi"
>>> a = 42

Type Inference

You also mentioned "implicit" or inferred typing for statically typed languages. Type inference happens at compile time. If the type inference process decides that a variable is of a monomorphic type (like Int), then that variable will always refer to a value of type Int. Monomorphic simply means a single form/type. The type inferencer can also decide that a function has polymorphic arguments, then it will be as first above. I hope you can see that type inference is a red herring when it comes to the main thrust of your question.