Коллеги!

В моём перегретом солнцем (я сейчас в южных краях отдыхаю) мозгу крутится идея.
Вспомним давний спор между статической и динамической типизацией. Аргументы за статическую — раннее обнаружение ошибок типизации на этапе компиляции программы (и, в более широком смысле — доказательство корректности программы с точки зрения типов). Аргументы за динамическую — статические системы типов, поддерживаемые языками программирования, не только помогают программисту, но иногда и мешают ему, поскольку их выразительная сила ограничена и программист должен тратить дополнительные силы на то, что бы "вписаться" в систему типов языка. Кроме того, иногда (на моей практике достаточно редко) возникают ситуации, когда конкретная система типов просто не позволяет выразить требуемые программисту абстракции.

В чем сущность системы типов, как средства поддержки целостности программы? Её можно выразить просто — обеспечить, что на вход в программу (подпрограмму, процедуру, функцию, метод, предикат etc) будут поданы только те данные, которые эта программа может корректно переварить. Иными словами, необходимо все множество значений, которые могут существовать в данном языке, разбить на два — допустимые для передачи в эту программу и недопустимые. Соответственно, если проверка допустимости осуществляется на этапе анализа программы — это статическая система типов, если в момент выполнения — это динамическая. Если проверки нет — это memory corruption

Разные системы типов по-разному справляются с этой задачей, предоставляя программисту разные инструменты для описания этих границ "можно-нельзя". Например, объявляя тип параметра как Integer, я указываю, что принимаются только целые числа. Если мне надо принимать только целые в интервале [-100..100], то я могу написать обертку над Integer или унаследоваться от него и породить класс ConstrainedInteger. Может быть ещё что-то, а может и ничего — все зависит от того, что поддерживается языком. Но в целом суть одна — я неявно описываю некоторый предикат, который для каждого возможного значения дает ответ — принадлежит значение типу или нет.

Суть идеи можно описать просто — дать программисту возможность описывать это разграничение максимально гибко. Дать ему язык для описания типов с выразительностью, не уступающей языку, на котором он производит разработку. То есть тьюринг-полный язык. Это может быть спец. язык или некоторое декларативное подмножество основного языка. Спецификации типов на этом языке могут быть вызваны как обычные функции-предикаты для проверки принадлежности заданного значения типу, так и использованы для доказательства взаимоотношения типов (несовместимы, пересекаются, включение, совпадение) в целях статической проверки корректности программы. Предикат с более чем одним параметром описывает параметризованный тип. При какой либо передаче данных производится проверка на совместимость типов. Если типы совместимы — все хорошо. Если типы заведомо несовместимы — ошибка компиляции. Если типы имеют пересечение — генерируется код проверки типа в run-time.

Данный подход, имхо, может иметь смысл в динамических языках для включения в них опциональной статической типизации. В традиционных статически типизированных языках эта идея вряд ли приживется, ибо в них на системы типов помимо обеспечения корректности, завязаны механизмы диспетчеризации вызовов (то есть две совершенно разные ответственности), а озвученная идея подразумевает ортогональность этих аспектов.

Я не предлагаю проработанной концепции и у меня нет ответов на все вопросы. Просто предлагаю обсудить.
Спасибо за внимание.

P.S. Я в отпуске, так что отвечать буду нерегулярно.