Функциональное программирование. Основы (Файлы для подготовки к экзамену), страница 5

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

Основная идея заключается в том, чтобы каждый лямбда-терм имелтип, и терм S можно применить к терму T в комбинации S T , если ихтипы правильно соотносятся друг с другом, т.е. S имеет тип функцииσ → τ и T имеет тип σ. Результат, S T , имеет тип τ . Это свойство называется сильной типизацией. Терм T должен иметь в точности тип σ:приведение типов не допускается, в отличие от языков типа Си, в котором некоторая функция, ожидающая аргумент типа double или float,может принять аргумент типа int и неявно преобразовать его.Мы будем использовать запись вида T :: σ для утверждения «T имееттип σ». Это напоминает использующуюся в математике стандартную запись вида f : σ → τ для функции f из множества σ в множество τ .

Типыможно представлять себе как множества, которым принадлежат соответствующие объекты, т. е. запись T :: σ можно интерпретировать какT ∈ σ. Однако мы будем рассматривать типизированное лямбда-исчисление как формальную систему, независящую от подобной интерпретации.6.1.1Базовые типыПрежде всего необходимо точно определить, что такое тип. Мы предполагаем, что у нас имеется некоторый набор базовых типов, таких какBool или Integer. Из них можно конструировать составные типы спомощью конструкторов типов, являющихся, по сути, функциями.

Дадим следующее индуктивное определение множества T yC типов, основывающихся на множестве базовых типов C:σ∈Cσ ∈ T yCσ ∈ T yC , τ ∈ T yCσ → τ ∈ T yCНапример, возможными типами могут быть Integer, Bool → Bool,(Integer → Bool) → Integer → Bool и т. д. Мы предполагаем, что функциональная стрелка → ассоциативна вправо, т. е. σ → τ → ν означаетσ → (τ → ν).В дальнейшем мы расширим нашу систему типов двумя способами. Во-первых, мы введем понятие ти́повых переменных, являющихсясредством для реализации полиморфизма. Во-вторых, мы введем дополнительные конструкторы типов, помимо функциональной стрелки.26Например, введем конструктор × для типа пары значений.

В этомслучае к нашему индуктивному определению необходимо добавить:σ ∈ T yC , τ ∈ T yCσ × τ ∈ T yCДалее, как и в языке Haskell, можно вводить именованные конструкторыпроизвольной арности. Мы будем использовать запись Con (α1 , . . . , αn )для применения n-арного конструктора Con к аргументам αi .Важным свойством типов является то, что σ → τ 6= σ (В действительности тип не может совпадать ни с каким своим синтаксически правильным подвыражением.) Это исключает возможность применения терма ксамому себе.6.1.2Типизации по Черчу и КарриСуществуют два основных подхода к определению типизированного лямбда-исчисления.

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

Правила корректного формирования термов выглядят тогда следующим образом:v :: σКонстанта c имеет тип σc :: σS :: σ → τ, T :: σS T :: τv :: σ, T :: τλv.T :: σ → τОднако мы будем использовать для типизации подход Карри, который является неявным. Термы могут иметь или не иметь типа, и еслитерм имеет тип, то он может быть не единственным. Например, функцияидентичности λx.x может иметь любой тип вида σ → σ. Такой подходболее предпочтителен, поскольку, во-первых, он соответствует используемому в языках типа Haskell и ML понятию полиморфизма, а во-вторых,позволяет, как и в этих языках, не задавать типы явным образом.27В то же самое время, некоторые формальные детали типизации поКарри несколько сложнее.

Мы не определяем понятие типизируемостисамо по себе, но по отношению к контексту, т. е. конечному наборупредположений о типах переменных. Мы будем записывать:? ` T :: σчтобы обозначить, что «в контексте ? терм T может иметь тип σ». Мыбудем употреблять запись ` T :: σ или просто T :: σ, если суждениео типизации выполняется в пустом контексте. Элементы контекста ?имеют вид v :: σ, т.

е. они представляют собой предположения о типахпеременных, как правило, тех, которые являются компонентами терма.Будем предполагать, что в ? нет противоречивых предположений.6.1.3Формальные правила типизацииПравила типизации вводятся совершенно естественно, следует толькопомнить о том, что T :: σ интерпретируется как «T может принадлежатьтипу σ».v :: σ ∈?? ` v :: σКонстанта c имеет тип σc :: σ? ` S :: σ → τ, ? ` T :: σ? ` S T :: τ? ∪ {v :: σ} ` T :: τ? ` λv.T :: σ → τЭти правила являются индуктивным определением отношения типизируемости, и терм имеет некоторый тип, если он может быть выведен поэтим правилам. Для примера рассмотрим типизирование функции идентичности λx.x.

По правилу для переменных имеем:{x :: σ} ` x :: σи отсюда по последнему правилу получаем:∅ ` λx.x :: σ → σСледуя соглашению о пустых контекстах мы пишем просто λx.x :: σ → σ.Можно показать, что все преобразования лямбда-термов сохраняюттипы, т. е. если некоторый терм T имел тип σ в контексте ?, то послепреобразования его в T 0 он будет иметь тот же самый тип.286.2ПолиморфизмСистема типов по Карри уже дает нам некоторую форму полиморфизма, в том смысле, что терм может иметь различные типы.

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

В противоположность этому, при перегрузке функция можетиметь различные типы, не связанные друг с другом структурным сходством. Также возможна ситуация когда функция просто определяетсядля некоторого набора типов. Например, функция сложения может иметьтип int → int → int или float → float → float, но не bool → bool → bool.6.2.1let-полиморфизмК сожалению, наша система типов приводит к некоторым нежелательным ограничениям на полиморфизм.

Например, следующее выражениесовершенно приемлемо:if (λx.x) true then (λx.x) 1 else 0Если использовать правила типизации, то можно получить, что это выражение имеет тип int. Два экземпляра функции идентичности имеюттипы bool → bool и int → int.Теперь рассмотрим выражение:let I = λx.x in if I true then I 1 else 0Согласно нашему определению, это всего лишь другой способ записидля(λI.if I true then I 1 else 0) (λx.x)Однако это выражение не может быть типизировано по нашим правилам.

В нем присутствует только один экземпляр функции идентичности,и он должен иметь единственный тип. Это — серьезный недостаток, поскольку мы уже видели, что конструкции с let широко используются вфункциональном программировании.Один из способов преодолеть это ограничение — добавить еще одно правило типизации, в котором let-конструкции рассматривается какпервичная:? ` S :: σ и ? ` T [x := S] :: τ? ` let x = S in T :: σ29Это правило вводит let-полиморфизм.

В нем выражается тот факт,что при типизации мы рассматриваем связывания по let так, как будто унас записаны различные экземпляры этих именованных выражений. Дополнительная гипотеза ? ` S :: σ нужна для того, чтобы гарантировать,что терм S типизируем, иначе были бы типизируемы такие выражениякак:let x = λf.f f in 06.2.2Наиболее общие типыКак уже было сказано, некоторые выражения не имеют типа, например, λf.f f или λf.(f true, f 1).

Типизируемые выражения обычно имеютмного типов, хотя некоторые, например, true, имеют только один. Такжемы говорили о параметрическом полиморфизме, т. е. все типы выражения могут иметь структурное сходство. В действительности истинноболее сильное утверждение: для каждого типизируемого выражения существует наиболее общий тип или основной тип, и все возможныетипы выражения являются экземплярами этого наиболее общего типа.Прежде чем сделать это утверждение строгим, необходимо ввести некоторую терминологию.Прежде всего, расширим нашу нотацию понятием ти́повых переменных. Это означает, что типы могут быть сконструированы с помощьюприменения конструкторов типа либо к типовым константам, либо к переменным.