Учебник по Haskell

Глава 16

Категориальные типы

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

ся как начальные и конечные объекты в специальных категориях, которые называются алгебрами функторов.

Для понимания этой главы хорошо освежить в памяти главу о структурной рекурсии, там где мы говорили

о свёртках и развёртках.

16.1 Программирование в стиле оригами

Оригами – состоит из двух слов “свёртка” и “бумага”. При программировании в стиле оригами все функ-

ции строятся через функции свёртки и развёртки. Есть даже такие языки программрования, в которых это

единственный способ определения рекурсии. Этот стиль очень хорошо подходит для ленивых языков про-

граммирования, поскольку в связке:

fold f . unfold g

функции свёртки и развёртки работают синхронно. Функция развёртки не производит новых элементов

до тех пор пока они не понадобятся во внешней функции свёртки.

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

fix.

Например так выглядит рекурсивная функция сложения всех чисел от одного до n:

sumInt :: Int -> Int

sumInt 0 = 0

sumInt n = n + sumInt (n-1)

Эту функцию мы можем переписать с помощью функции fix. При вычислении fix f будет составлено

значение

f (f (f (f ... )))

Теперь перепишем функцию sumInt через fix:

sumInt = fix $ \f n ->

case n of

0

-> 0

n

-> n + f (n - 1)

Смотрите лямбда функция в аргументе fix принимает функцию и число, а возвращает число. Тип этой

функции (Int -> Int) -> (Int -> Int). После применения функции fix мы как раз и получим функцию

типа Int -> Int. В лямбда функции рекурсивный вызов был заменён на вызов функции-параметра f.

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

обобщённый тип, который обозначает рекурсивный тип:

newtype Fix f = Fix { unFix :: f (Fix f) }

В этой записи мы получаем уравнение неподвижной точки Fix f = f (Fix f), где f это некоторый тип

с параметром. Определим тип целых чисел:

240 | Глава 16: Категориальные типы

data N a = Zero | Succ a

type Nat = Fix N

Теперь создадим несколько конструкторов:

zero :: Nat

zero = Fix Zero

succ :: Nat -> Nat

succ = Fix . Succ

Сохраним эти определения в модуле Fix. hs и посмотрим в интерпретаторе на значения и их типы, ghc не

сможет вывести экземпляр Show для типа Fix, потому что он зависит от типа с параметром, а не от конкретно-

го типа. Для решения этой проблемы нам придётся определить экземпляры вручную и подключить несколько

расширений языка. Помните в главе о ленивых вычислениях мы подключали расширение BangPatterns? Нам

понадобятся:

{-# Language FlexibleContexts, UndecidableInstances #-}

Теперь определим экземпляры для Show и Eq:

instance Show (f (Fix f)) => Show (Fix f) where

show x = ”(” ++ show (unFix x) ++ ”)”

instance Eq (f (Fix f)) => Eq (Fix f) where

a == b = unFix a == unFix b

Определим списки-оригами:

data L a b = Nil | Cons a b

deriving (Show)

type List a = Fix (L a)

nil :: List a

nil = Fix Nil

infixr 5 ‘cons‘

cons :: a -> List a -> List a

cons a = Fix . Cons a

В типе L мы заменили рекурсивный тип на параметр. Затем в записи List a = Fix (L a) мы произ-

водим замыкание по параметру. Мы бесконечно вкладываем тип L a во второй параметр. Так получается

рекурсивный тип для списков. Составим какой-нибудь список:

*Fix> :r

[1 of 1] Compiling Fix

( Fix. hs, interpreted )

Ok, modules loaded: Fix.

*Fix> 1 ‘cons‘ 2 ‘cons‘ 3 ‘cons‘ nil

(Cons 1 (Cons 2 (Cons 3 (Nil))))

Спрашивается, зачем нам это нужно? Зачем нам записывать рекурсивные типы через тип Fix? Оказыва-

ется при такой записи мы можем построить универсальные функции fold и unfold, они будут работать для

любого рекурсивного типа.

Помните как мы составляли функции свёртки? Мы строили воображаемый класс, в котором сворачивае-

мый тип заменялся на параметр. Например для списка мы строили свёртку так:

class [a] b where

(:) :: a -> b -> b

[]

:: b

После этого мы легко получали тип для функции свёртки:

foldr :: (a -> b -> b) -> b -> ([a] -> b)

Программирование в стиле оригами | 241

Она принимает методы воображаемого класса, в котором тип записан с параметром, а возвращает функ-

цию из рекурсивного типа в тип параметра.

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

мы строим типы с параметром, а затем получаем из них рекурсивные типы с помощью конструкции Fix.

Теперь методы класса с параметром это наши конструкторы исходных классов, а рекурсивный тип записан

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

fold :: (f b -> b) -> (Fix f -> b)

Смотрите функция свёртки по-прежнему принимает методы воображаемого класса с параметром, но те-