Теория типов и комбинаторная логика
Рассмотрим построение системы типизации на основе комбинаторной логики.
В математике принято называть типами (или, иначе, сортами) относительно устойчивые и независимые совокупности элементов, которые можно выделить во всем рассматриваемом множестве (предметной области). Заметим, что разделение элементов предметной области на типы или сорта во многом является условным и носит субъективный характер, т.к. зависит от эксперта в этой области.
Тип, подобно множеству, может определяться двояко.
Во-первых, возможно определение типа посредством явного перечисления всех элементов, принадлежащих типу (заметим, что такой подход применяется и в математике, и в программировании, где существуют так называемые перечислимые типы).
Другим способом определения типа T является формализация общих свойств тех элементов d из предметной области D, которые объединяются в этот тип, посредством задания индивидуализирующей предикатной функции Y, значение которой истинно, если элемент принадлежит данному типу и ложно в противном случае:
T = {d: D|?}.
При более формальном подходе к теории типов и типизации в связи с исчислением ламбда-конверсий следует определить чистую систему типов.
Чистой системой типов называется семейство ламбда-исчислений, в которых каждый элемент характеризуется тройкой
<S, A, R>,
где:
S - подмножество констант, называемых сортами;
A - множество аксиом вида c:s, где с является константой, а s является сортом;
R - множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы.
Далее введем обозначение, характеризующее то обстоятельство, что тот или иной объект является типизированным, или, иначе говоря, что тому или иному объекту приписан тип.
В частности, для ламбда-терма M приписывание ему типа T обозначим как
#M ||- T
и будем в таком случае говорить, что ламбда-терм M имеет тип T.
При более общем подходе, который верен и для математики, и для программирования, система типов формируется следующим образом.
Во-первых, задается множество базисных типов (обозначим их символами d1
, d2
, и так далее).
Во-вторых, примем соглашение, что всякий базисный тип считается типом.
В-третьих, условимся, что если a и b считаются типами, то функция из a в b также считается типом и при этом имеет тип a>b.
Заметим, что в основе теории типов лежит принцип иерархичности, который заключается в том, что производные типы содержат базисные как подмножества.
Этот принцип построения справедлив и для языков программирования. В частности, иерархии классов в объектно-ориентированных языках программирования формируются аналогично приведенному выше построению математической системы типов.
Для иллюстрации построения теории типов расширим комбинаторную логику операцией приписывания типа.
Напомним аксиомы комбинаторной логики, задающие свойства отношения конвертируемости:
(I) Ix = x; (K) Kxy = x; (S) Sxyz = xz(yz).
Аксиома (I) означает существование комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя.
Аксиома (K) означает существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка. Интуитивно ясно, что эта аксиома близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.
Оказывается, что комбинаторная логика обладает возможностью не только моделировать процесс реализации программного обеспечения на языке функционального программирования, но и прозрачно формализовать процедуру приписывания типов объектам этого языка.
Под типом (сортом) будем понимать относительно устойчивую и независимую совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области).
