Введение в теорию программирования. Функциональный подход


Теория типов и комбинаторная логика - часть 2


, d2

, и так далее).

Во-вторых, примем соглашение, что всякий базисный тип считается типом.

В-третьих, условимся, что если a и b считаются типами, то функция из a в b также считается типом и при этом имеет тип  a>b.

Заметим, что в основе теории типов лежит принцип иерархичности, который заключается в том, что производные типы содержат базисные как подмножества.

Этот принцип построения справедлив и для языков программирования. В частности, иерархии классов в объектно-ориентированных языках программирования формируются аналогично приведенному выше построению математической системы типов.

Для иллюстрации построения теории типов расширим комбинаторную логику операцией приписывания типа.

Напомним аксиомы комбинаторной логики, задающие свойства отношения конвертируемости:

(I) Ix = x; (K) Kxy = x; (S) Sxyz = xz(yz).

Аксиома (I) означает существование комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя.

Аксиома (K) означает существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка. Интуитивно ясно, что эта аксиома близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.

Оказывается, что комбинаторная логика обладает возможностью не только моделировать процесс реализации программного обеспечения на языке функционального программирования, но и прозрачно формализовать процедуру приписывания типов объектам этого языка.

Под типом (сортом) будем понимать относительно устойчивую и независимую совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области).




Начало  Назад