Учебник по Haskell

С помощью этих функций можно избавиться в формулах от переменных, так например свойство комму-

тативности функции A можно представить так: T A = A. Эти комбинаторы зависят друг от друга. Можно

убедиться в том, что:

I

=

SCC

Z

=

S( CS) S

T

=

S( ZZS)( CC)

Все комбинаторы выражаются через комбинаторы C и S. Ранее мы пользовались другими обозначениями

для этих комбинаторов. Обозначения K и S ввёл Хаскель Карри (Haskell Curry). Независимо от Шейнфинкеля

он переоткрыл комбинаторную логику и существенно развил её. В современной комбинаторной логике для

обозначения комбинаторов I, C, T , Z и S (по Шейнфинкелю) принято использовать имена I, K,

C, B, S

(по Карри).

224 | Глава 14: Лямбда-исчисление

14.3 Лямбда-исчисление с типами

Мы можем добавить в лямбда-исчисление типы. Предположим, что у нас есть множество V базовых типов.

Тогда тип это:

T = V | T → T

Тип может быть либо одним элементом из множества базовых типов. Либо стрелочным (функциональ-

ным) типом. Выражение “терм M имеет тип α” принято писать так: Mα. Стрелочный тип α → β как и в

Haskell говорит о том, что если у нас есть значение типа α, то с помощью операции применения мы можем

из терма с этим стрелочным типом получить терм типа β.

Опишем правила построения термов в лямбда-исчислении с типами:

• Переменные xα, yβ, zγ, … являются термами.

• Если Mα→β и Nα – термы, то ( Mα→βNα) β – терм.

• Если xα – переменная и Mβ – терм, то ( λxα. Mβ) α→β – терм

• Других термов нет.

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

плюсы и минусы. Теперь наша система является строго нормализуемой, это означает, что любой терм име-

ет нормальную форму. Но теперь мы не можем выразить все функции на числах. Например мы не можем

составить Y -комбинатор, поскольку теперь самоприменение ( ee) невозможно.

Мы ввели типы, но лишились рекурсии. Как нам быть? Эта проблема решается с помощью введения

специальной константы Y ( τ→τ) →τ

τ

, которая обозначает комбинатор неподвижной точки. Правило редукции

для Y :

( Yτ f τ→τ ) τ = ( f τ→τ ( Yτ f τ→τ )) τ

Можно убедиться в том, что это правило роходит проверку типов. Типизированное лямбда-исчисление

дополненное комбинатором неподвижной точки способно выразить все числовые функции.

14.4 Краткое содержание

В этой главе мы познакомились с лямбда-исчислением и комбинаторной логикой, двумя конструктив-

ными теориями функций. Конструктивными в том смысле, что определение функции содержит не набор

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

из каких простейших частей она состоит. Редукция термов позволяет вычислять функции.

Мы узнали, что функциями можно кодировать логические значения и числа. Узнали, что все численные

функции могут быть закодированы лямбда-термами.

14.5 Упражнения

• С помощью редукции убедитесь в том, что верны формулы (в терминах Карри) :

B

=

S(

KS) S

C

=

S( BBS)( KK)

Bxyz

=

xzy

Cxyz

=

x( yz)

• Попробуйте закодировать пары с помощью лямбда термов. Вам необходимо построить три функции:

P air, F st, Snd, которые обладают свойствами:

Лямбда-исчисление с типами | 225

F st ( P air a b)

=

a

Snd ( P air a b)

=

b

• в комбинаторной логике тоже есть комбинатор неподвижной точки, найдите его с помощью алгоритма

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

SKK писать просто I

.

• Напишите типы Lam и App, которые описывают лямбда-термы и термы комбинаторной логики в Haskell.

Напишите функции перевода из значений Lam в App и обратно.

226 | Глава 14: Лямбда-исчисление

Глава 15

Теория категорий

Многие понятия в Haskell позаимствованы из теории категорий, например это функторы, монады. Теория

категорий – это скорее язык, математический жаргон, она настолько общая, что кажется ей нет никакого

применения. Возможно это и так, но в этом языке многие сущности, которые лишь казались родственными

и было смутное интуитивное ощущение их близости, становятся тождественными.

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

становка значения в функцию, а в теории категорий мы сосредоточимся на операции композиции. Мы будем

соединять различные объекты так, чтобы структура объектов сохранялась. Структура объекта будет опреде-

ляться свойствами, которые продолжают выполнятся после преобразования объекта.

15.1 Категория

Мы будем говорить об объектах и связях между ними. Связи принято называть “стрелками” или “мор-

физмами”. Далее мы будем пользоваться термином стрелка. У стрелки есть начальный объект, его называют

доменом (domain) и конечный объект, его называют кодоменом (codomain).

f

A

B

В этой записи стрелка f соединяет объекты A и B, в тексте мы будем писать это так f : A → B, словно

стрелка это функция, а объекты это типы. Мы будем обозначать объекты большими буквами A, B, C, …, а