John Harrison - Введение в функциональное программирование (1108517), страница 12
Текст из файла (страница 12)
— Прим. перев.2Возможно, также ценой дополнительных затрат.38Глава 4. Типы4.1. Типизированное лямбда-исчислениене менее, мы не хотели бы создать у читателя ложного впечатления, что этот языкслужит универсальным средством от всех проблем программирования.4.1Типизированное лямбда-исчислениеВ первом приближении расширение лямбда-исчисления понятием типа непредставляет особого труда, но в итоге, как будет показано, потребуется кудабольше усилий. Основная идея состоит в том, что каждому терму назначаетсятип, после чего выражение s t, т. е. применение терма s к терму t, допустимоисключительно для совместимых типов, то есть в случае, когда типы s и t имеютвид σ → τ и σ соответственно.
Результирующий терм будет иметь при этомтип τ . Такую типизацию принято называть сильной.3 Терм t обязан иметь тип σ,подтипы и преобразования не допускаются. Такой подход составляет резкий контрастс некоторыми языками программирования, например, с языком C, в которомфункция, ожидающая аргумент типа float либо double, принимает также значениятипа int, выполняя автоматическое преобразование. Аналогичные понятия подтипови преобразований возможно задать и в рамках лямбда-исчисления, но их освещениезавело бы нас слишком далеко.Введём для отношения «t имеет тип σ» обозначение t : σ.
Подобнаязапись традиционно используется математиками при работе с функциональнымипространствами, поскольку f : σ → τ обозначает функцию f , отображающуюмножество σ во множество τ . Будем считать типы множествами, которые содержатсоответствующие объекты, и трактовать t : σ как t ∈ σ.
Однако, несмотряна то, что мы предлагаем читателям также воспользоваться этой удобнойаналогией, типизированное лямбда-исчисление будет в дальнейшем рассматриватьсяисключительно как формальная система, свободная от каких-либо интерпретаций.4.1.1Множество допустимых типовНачнём формализацию строгим определением понятия типа. Предположим,что у нас имеется некоторое множество примитивных типов, в которое входят,например, типы bool и int.
Составные типы могут быть определены при помощиконструктора типа функции. Формально, индуктивное определение множестватипов T yC , основанного на множестве примитивных типов C, выглядит так:σ∈Cσ ∈ T yCσ ∈ T yC τ ∈ T yCσ → τ ∈ T yCНапример, в рамках данного определения допустимы типы int, bool → boolлибо (int → bool) → int → bool. Будем считать операцию «→» правоассоциативной,т. е. полагать выражение σ → τ → υ равным σ → (τ → υ). Такая трактовкаестественно согласуется с другими синтаксическими правилами, касающимисякаррирования.3Сильную типизацию также часто называют строгой.
— Прим. перев.394.1. Типизированное лямбда-исчислениеГлава 4. ТипыСледующим нашим шагом будет расширение системы типов в двух направлениях.Во-первых, введём наравне с примитивными типами (которые выполняют рольконстант) так называемые переменные типа, которые впоследствии лягут в основуполиморфизма. Во-вторых, разрешим использование множества конструкторовдругих типов, помимо типа функции. Например, в дальнейшем нам понадобитсяконструктор × для типа декартова произведения.
Как следствие, наше индуктивноеопределение должно быть дополнено ещё одним выражением:σ ∈ T yC τ ∈ T yCσ × τ ∈ T yCПоскольку язык ML допускает определение пользователем новых типов и ихконструкторов, нам потребуется нотация, пригодная для описания произвольногомножества конструкторов с произвольным количеством аргументов. Обозначимчерез (α1 , . . . , αn )con применение n-арного конструктора типа con к наборуаргументов αi . (Инфиксная форма будет использоваться лишь в некоторых широкоизвестных частных случаях наподобие → и ×.) Например, выражение (σ)listтрактуется как тип-список, все элементы которого имеют тип σ.Принимая во внимание free inductive generation, можно доказать важноесвойство типов, а именно, что σ → τ 6= σ.
(В действительности справедливоболее общее утверждение: тип не может равняться произвольному собственномуподвыражению.) Это свойство исключает возможность применения терма к самомусебе, за исключением случая, когда оба экземпляра терма, о которых идёт речь,имеют различные типы.4.1.2Типизация по Чёрчу и КарриИзвестны два основных подхода к определению типизированного лямбдаисчисления. Один из них, разработанный Чёрчем, подразумевает явное указаниетипов. Каждому терму при этом назначается единственный тип.
Другими словами,в ходе построения термов, каждому нетипизированному терму, которые былирассмотрены ранее, в дополнение указывается тип. Типы констант являютсяпредопределёнными, но типы переменных могут быть произвольными. Точныеправила построения типизированных термов приведены ниже:v:σКонстанта c имеет тип σc:σs:σ→τ t:σst:τv:σ t:τλv. t : σ → τОднако, для наших целей лучше подходит неявная типизация, предложеннаяКарри. Структура термов соответствует нетипизированному случаю, при этом терм40Глава 4. Типы4.1. Типизированное лямбда-исчислениеможет как иметь тип (причём не один), так и не иметь его.4 Например, тождественнойфункции λx.
x может быть вполне обоснованно назначен произвольный типвида σ → σ. Применительно к языку ML существуют два взаимосвязанныхдовода в пользу данного подхода к типизации. Во-первых, он позволяет удобнеевыразить присущий ML полиморфизм, а во-вторых, хорошо согласуется с практикойпрограммирования на этом языке, в ходе которого не требуется задавать типы явно.В то же время, некоторые формальные аспекты назначения типов по Карриоказываются достаточно сложными. Отношение типизируемости не может бытьзадано в отрыве от некоторого контекста, представляющего собой конечноемножество утверждений относительно типов переменных.
Обозначим черезΓ`t:σутверждение «в контексте Γ терму t может быть назначен тип σ». (Если этоутверждение справедливо при пустом контексте, выражение сокращается до ` t : σили даже до t : σ.) Элементы множества Γ имеют вид v : σ т. е. сами по себе являютсяутверждениями относительно типов отдельных переменных, обычно тех, которыевходят в терм t. Будем полагать, что контекст Γ не содержит противоречивыхутверждений о типе некоторой переменной; при желании, мы можем рассуждатьо нём как о частичной функции, отображающей индексное множество переменныхво множество типов.
Использование нами символа ` соответствует его роли втрадиционной логике, где Γ ` φ принято трактовать как «утверждение φ следуетиз множества посылок Γ».4.1.3Формальные правила типизацииФормулировка правил назначения типов выражениям достаточно естественна.Прежде, чем мы приведём эти правила, напомним ещё раз, что t : σ следуетинтерпретировать как «t может иметь тип σ».v:σ∈ΓΓ`v:σКонстанта c имеет тип σc:σΓ`s:σ→τ Γ`t:σΓ`st:τΓ ∪ {v : σ} ` t : τΓ ` λv. t : σ → τЕщё раз повторим, что эти выражения следует понимать как индуктивноеопределение отношения типизируемости, так что терм может иметь тип лишь тогда,когда последний выводим при помощи упомянутых выше правил.
В качестве примера4Поборники чистоты терминологии могут возразить против использования в данном случаетермина «типизированное лямбда-исчисление», считая более подходящим «нетипизированноелямбда-исчисление, дополненное понятием назначения типа»414.1. Типизированное лямбда-исчислениеГлава 4. Типырассмотрим процедуру вывода типа тождественной функции.
Согласно правилутипизации переменных, мы имеем:{x : σ} ` x : σоткуда, применив последнее правило, получаем:∅ ` λx. x : σ → σПрименив установленное ранее соглашение о пустых контекстах, мы можемсократить это выражение до λx. x : σ → σ. На данном примере также хорошовидна как важная роль контекстов в типизации по Карри, так и их необязательностьв рамках типизации по Чёрчу. Опуская контекст, мы можем вывести x : τ дляпроизвольного типа τ , после чего, согласно последнему правилу, получаем λx.
x :σ → τ — налицо различие с интуитивной трактовкой тождественной функции!Эта проблема не возникает в ходе типизации по Чёрчу, поскольку в её рамкахлибо обе переменные имеют тип σ, откуда получаем λx. x : σ → σ, либоэти переменные на самом деле различны (поскольку различны их типы, которыесчитаются неотъемлемой частью терма). В последнем случае тип выражения вдействительности будет равен λx : σ. (x : τ ) : σ → τ , но это обосновано тем, чтоданное выражение альфа-эквивалентно λx : σ.
(y : τ ) : σ → τ . Поскольку в ходетипизации по Карри термы не содержат в себе типов явно, нам требуется некоторыймеханизм связывания между собой одинаковых переменных.4.1.4Сохранение типаОчевидное сходство структуры термов типизированного и нетипизированноголямбда-исчисленияпорождаетестественноежеланиеприменитьвтипизированном случае аппарат формальных преобразований, разработанныйдля нетипизированного. Однако, нам потребуется предварительно доказать, чтотип выражения в ходе преобразований не изменяется (такое свойство называетсясохранением типа).
Убедиться в этом не представляет труда; мы рассмотримкраткое изложение доказательства для случая η-преобразования, предоставивостальные читателю в качестве упражнения. Прежде всего, докажем две леммы,которые весьма очевидны, но тем не менее, требуют формального обоснования.Во-первых, покажем, что добавление новых элементов в контекст не влияет натипизируемость:Лемма 4.1 (О монотонности) Если Γ ` t : σ и Γ ⊆ ∆, то справедливо ∆ ` t : σ.Доказательство: Применим индукцию по структуре t.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
