Типизированное лямбда-исчисление

Типы

Причина введения типов в лямбда-исчисление и в языки программирования возникает как с точки зрения логики так и пограммироваия.

Лямбда-исчисление разрабатывалось для формализации языка математики. Черч предполагал включить в лямбда-исчисление теорию множеств. По заданному множеству S можно определить его характеристическую функцию χ _s, такую что:

С другой стороны, имея унарный предикат Р, можно определить множество таких х, что Р (х) = true. Однако определение предикатов (и, следовательно, множеств) в виде произвольных лямбда-выражений может привести к противоречиям.

Рассмотрим парадокс Рассела. Определим множество R, состоящее из всех множеств, которые не содержат себя в качестве элемента:

Тогда , что является противоречием. В терминах лямбда-исчисления можно определить предикат и получим противоречие . Выражение R R является неподвижной точкой оператора отрицания.

Парадокс Рассела в лямбда-исчислении возникает из-за того, что мы применяем функцию к самой себе. Однако это не обязательно приводит к парадоксу: например, функция идентичности λх. х или константная функция λх. у не приводят к противоречиям. Более четкое представлене функций, обозначаемых лямбда-термами, требует точного знния области их определения и значений и применения только к аргументам, принадлежащим областям их определения. По этим причинам Рассел предложил ввести понятие типа.

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

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

Существуют также безтиповые языки, как императивные, так и функциональные. Некоторые языки являются слабо типизированными, когдакомпилятор допускает некоторое несоответствие в типах и сам делает необходимые преобразования. Существуют языки (например, Python), которые выполняют проверку типов динамически, во время выполнения программы, а не во время компиляции.

Определение системы типов, которая позволяет выполнять статические проверки и в то же время не накладывает жестких ограничений - сложная задача. Система типов, использующаяся в таких языках, как Haskell - предоставляет возможность полиморфизма, когдаодна и та же функция может использоваться с различными типами. Это оставляет возможность статических проверок, предоставляя в то же время преимущества слабой или динамической типизации. Более того, программист не обязан указывать типы в Haskell: компилятор может вывести наиболее общий тип любого выражения и отвергнуть выражения, не имеющие типа.

Модифицируем лямбда-исчисление введя в него понятие типа. Каждый лямбда-терм должен иметь тип, причем терм S можно применить к терму Т вкомбинации S Т, если их типы правильно соотносятся друг с другом, т.е. S имеет тип функции σ —> τ и Т имеет тип σ. В результате, S Т, имеет тип τ. Это свойство называется сильной типизацией. Приведение типов не допускается.

Будем использовать запись вида Т:: σ для утверждения «Т имеет тип σ».