Выводимость типов

Схема типизации

Типизация выражений в SML

Аксиомы вывода типа комбинатора

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

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

Аксиома (I)	Ix = x	существования комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя
Аксиома (K)	Kxy = x	существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка*
Аксиома (S)	Sxyz = xz(yz)	попарного связывания третьего элемента с первыми двумя

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

В случае комбинаторной логики будем считать, что тип a приписан комбинатору X тогда и только тогда, когда это утверждение получено из следующих аксиом (||- «имеет тип»):

(FI) ||- #(I) = (a,a), тип тождества

(FK) ||- #(K) = (a,(b,a)) = (a,b,a), тип канцелятора

(FS) ||- #(S) = ((a,(b,c)), ((a, b)(a,c))) тип связывания (коннектора)

и правила вывода типа

(F) если ||- #(X) = (a,b) и ||- #(U) = a,

то ||- #(XU) = b.

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

Сравним математическую теорию типов с подходом к типизации выражений, принятым в языке программирования SML.

Каждому выражению (константа, переменная, функция) языка SML поставлен в соответствие тот или иной тип. Такая система типизации в языках функционального программирования называется системой сильной типизации, а сам язык - языком с сильной типизацией.

Система типов в SML формируется по следующей схеме:

1. Определяется множество базисных типов. В частности, в языке программирования SML выделяются следующие базисные типы:

· int - целые числа;

· string - строки символов;

· bool - логические значения.

2. Принимается следующее соглашение для выводимости производных типов: если a и b считаются типами, то функция из a в b имеет тип a→b.

Как можно заметить, формирование системы типов в SML аналогично построению системы типов в формальных математических теориях, в частности в комбинаторной логике.

Язык функционального программирования SML представляет собой язык со статической типизацией. Это означает, что процедура контроля типизации, которая является неотъемлемой частью транслятора любого современного языка программирования, должна поставить тот или иной тип в соответствие каждому выражению в тексте программы. Таким образом, приписывание типов выражениям происходит во время компиляции (compile time), а не во время выполнения (run time) программы, т.е. статически с точки зрения выполнения программы.

Тот факт, что каждый объект программы должен быть типизирован до начала ее выполнения, не означает необходимости явного приписывания типа в ходе проектирования и реализации программы.

Важным преимуществом языка программирования SML, который возник как инструментальное средство для доказательства теорем, т.е. построения цепочек логического вывода, является так называемое свойство выводимости типов (type inference). Это свойство означает, что тип некоторых выражений языка SML может быть выведен из контекста окружающих его выражений, типы которых уже известны, путем сопоставления (при этом учитываются объемлющие и внутренние функции, аппликация, присваивание и другие операции). Этот механизм, известный как выводимость типов (type inference), адекватно моделируется в терминах комбинаторной логики.

При этом выводимость допускает не строгое равенство типов параметров, а лишь их сводимость друг к другу. С математической точки зрения прослеживается аналогия с отношением конвертируемости.

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

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

Контроль соответствия типов в языке SML, в отличие от LISP и подобных ему языков программирования, в полном объеме осуществляется на этапе компиляции, что также способствует безопасности типизации.

Дата добавления: 2014-01-07