Обзор некоторых определений по поводу слова тип: https://www.researchgate.net/publication/334174126
И комментарий:
Откуда есть пошла Земля Русская пошло слово тип?
После создания Георгом Кантором наивной теории множеств,
некто Фреге попытался создать логическую формальную версию теории множеств.
То есть, аксиоматическую, вроде как геометрия Евклида.
/* Фреге придумал кванторы, которыми вы все неправильно пользуетесь.
*/
Но Бертран Рассел тут же построил в ней парадокс. Причем прямо перед изданием книги Фреге, так шоб последний не успел ничего поправить. (;
Парадокс -- такое состояние чтения и размышления над (исполнением формального текста) формальным текстом,
при котором дальнейшие размышления невозможны. Ну, например, правда это ложь.
Что бы выкрутиться Рассел предложил теорию типов. И запретил
использовать множества разных типов в выражении.
Это привело к устранению парадоксов.
То есть, Рассел придумал статическую типизацию.

У нас парадокс называется исключительным состоянием -- такое состояние вычисления
по формальному тесту программы, при котором дальнейшие вычисления невозможны.
Например, 1 == 0.
А существование типов запрещает (на шаге компиляции)
формально использовать выражения некоторых типов
в одном (большем) выражении, что предотвращает (некоторые) исключительные состояния во время исполнения.

пысы
Программирование -- это математика без бесконечных множеств.