Unknown - haskell-notes

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

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

составить 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 , …, а

стрелки – маленькими буквами f , g , h , … Для того чтобы связи было интереснее изучать мы введём такое

правило:

f

A

B

g

f ; g

C

Если конец стрелки f указывает на начало стрелки g , то должна быть такая стрелка f ; g , которая обозна-

чает составную стрелку. Вводится специальная операция “точка с запятой”, которая называется композицией

стрелок: Это правило говорит о том, что связи распространяются по объектам. Теперь у нас есть не просто

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