В 1971-м святой логик Жан-Ив Жирар придумал математическую модель типизации - System F (лямбда-исчисление второго порядка).

В 1973-м святой Робин Милнер реализовал эти подходы в языке программирования ML (OCaml, F#...): из одной только сигнатуры типа функции можно вывести нетривиальные теоремы о её поведении, вообще не заглядывая в код.
(система типов Хиндли-Милнера, автоматический вывод типов, пи-калкулусы как стандарт параллельных вычислений... европейская школа cs абсолютный топчик)

В частности, тогда и появилась концепция "дженериков" (параметрический полиморфизм, который так-то был известен с 1960-х). Возможность написать функцию, которая принимает неизвестный тип T и ничего не знает о его внутренностях, активно использовалась в академических языках, пока святой Филипп Вадлер, занимаясь попутно созданием Хаскеля, в легендарной статье "Theorems for free" 1989 г. доказал нужную математику для абстрактных лямбда-исчислений, гарантировав, что такие методы суть морфизмы функторов.
 
...Но вся эта математическая красота и строгость, увы, осталась заперта в башне из слоновой кости. Индустрия программирования, в своей жажде быстрого профита отвернулась от чистоты теорий типов и категорий. Мир выбрал JavaScript с его неявным приведением типов, Java с её null, который ломает все функторы, и Python, где типы лишь необязательные подсказки. Рефлексия, побочные эффекты, исключения и грязные хаки пробили брешь в идеальных лямбда-исчислениях...
И даже Хаскель, спустившись с небес в мэйнстрим, ради производительности и интеграции с внешним миром был вынужден впустить в себя unsafePerformIO и другие чёрные ходы, сделав "бесплатные теоремы" условными, а естественные преобразования теорката тотально нарушаемыми...
  
И самое грустное во всем этом - что софт, от которого зависят жизни миллионов людей и работа критических инфраструктур, пишется (и чем дальше, тем больше) не на языках с математически доказанной корректностью, а на костылях, склеенных изолентой ad-hoc полиморфизма, где любая функция с идеальной сигнатурой в любой момент может оказаться бэкдором...