Статическая и динамическая типизация

@covalue в дискуссии на тему "статической и динамической типизации" (типовой дурацкий вопрос собеседования программистов, самые умные ещё добавляют "сильная vs слабая типизация") предложил глянуть пару статей: "Search of types" (Kell, 2014) и "Several types of types in programming languages" (S. Martini, 2016).

Сама пара координат для типизации, "статическая и динамическая" и "сильная и слабая", мягко говоря, не совершенна. В целом она придумана вроде как для описания существующих массовых прикладных языков (т.е. заведомо не берём Haskell или Lean, нам бы с Asm - C - Algol - Java - Python разобраться). Но, как видим выше, выкрутить её можно в любую сторону.

Сам уважаемый @covalue понимает это всё хозяйство в том смысле, что существует "административная", "машинная" и "логическая" функция типов.

Мне кажется зайти удобней с другой стороны.

Вот рассмотрим три инструкции:

1. x + y
2. print(x)
3. x.name = "Vasya"

В каждой из них, с точки зрения дизайнера языка, вызывается некая "перегруженная функция" (overloaded function):

1. +(x, y), а точнее integer_plus(x, y)
2. print(x.to_string), а точнее print_string(integer_to_string(x))
3. name_set(x, "Vasya"), а точнее person_name_set(x, "Vasya")

Писать "точные" варианты мы не хотим, нам это неудобно, хотим использовать исходные лаконичные синтаксические конструкции. Но тогда проблема выбора подходящей функции, реализующей "в целом субъективно что-то такое" (почему субъективно – потому что сложение, например, строк и чисел технически между собой ничего общего не имеют), перекладывается на компилятор/интерпретатор.

Для реализации этой задачи приходят к следующим вариантам решения:

1. Наделаем функций на все сочетания операндов, типа сложения чисел и строк ("слабая динамическая типизация"), как в JS или Perl.
2. Сделаем статический анализатор, который будет гарантировать, что для сокращённой синтаксической конструкции всегда будет возможность найти необходимый полный вариант ("сильная статическая типизация").
3. Найдём полную форму для сокращённой в момент исполнения кода, если не находится кидать ошибку ("сильная динамическая типизация").

Короче, в этом вопросе речь идёт как будто не про типы вовсе, а про диспетчеризацию перегруженных функций.