В продолжение про интерфейсы.

Например, мы вполне можем убрать из интерфейса стека специальные слова push и pop, и назвать эти операции просто add и remove. Потом мы можем создать интерфейс очереди, также используя операции add и remove. Когда я делал курсы по алгоритмам, сразу отметил, насколько похожи интерфейсы классов стека и очереди. Фактически, если заменить push и pop на add и remove, мы получим идентичный интерфейс! Не знаю, хорошо это или плохо, но люди, которые хотят объединить эти два интерфейса, встречаются примерно так же часто, как люди, которые требуют, чтобы их обслужили первыми, потому что они вошли в очередь последними.

Это показывает, что когда мы думаем об интерфейсах, мы думаем не только о том, содержит ли модуль функции с определёнными сигнатурами. Мы также думаем о спецификации -- о том, какого именно поведения мы ожидаем от этих функций. Возможно, рядом с функцией pop() есть комментарий, говорящий, что она обратна функции push(). Этот факт можно считать частью типа модуля в той же мере, что и сами сигнатуры функций, потому что знание этого факта необходимо для использования модуля! В идеале его надо сделать "физической" частью типа.

Существует несколько языков с достаточно мощными системами типов, чтобы выразить связь между push() и pop() -- например, Coq, Agda, Idris. Я могу показать вам, как это выглядит на любом из них, но к большому сожалению это совсем непрактично. Поэтому пока основное решение -- материалы из СильныхИдей, где я постоянно поясняю, как правильно думать на более высоком логическом уровне -- абстракциями, которые в обычном коде отсутствуют по определению.