образцом, но на этот раз на типах. Первое уравнение:
type instance Add a Zero
= a
Говорит о том, что если второй аргумент имеет тип ноль, то мы вернём первый аргумент. Совсем как в
обычном функциональном определении сложения для натуральных чисел Пеано. а во втором уравнении мы
составляем рекурсивное уравнение:
type instance Add a (Succ b)
= Succ (Add a b)
Точно также мы можем определить и умножение:
type family Mul a b :: *
type instance Mul a Zero
= Zero
type instance Mul a (Succ b)
= Add a (Mul a b)
При этом нам придётся подключить ещё одно расширение UndecidableInstances, поскольку во втором
уравнении мы подставили одно семейство типов в другое. Этот флаг часто используется в сочетании с рас-
ширением TypeFamilies. Семейства типов фактически позволяют нам определять функции на типах. Это
ведёт к тому, что алгоритм вывода типов становится неопределённым. Если типы правильные, то компиля-
тор сможет это установить, но если они окажутся неправильными, может возникнуть такая ситуация, что
компилятор зациклится и будет бесконечно долго искать соответствие одного типа другому. Теперь про-
верим результаты. Для этого мы создадим специальный класс, который будет переводить значения-типы в
обычные целочисленные значения:
class Nat a where
toInt :: a -> Int
instance Nat Zero where
toInt = const 0
instance Nat a => Nat (Succ a) where
toInt x = 1 + toInt (proxy x)
proxy :: f a -> a
proxy = undefined
Расширения | 259
Мы определили для каждого значения-типа экземпляр класса Nat, в котором мы можем переводить типы
в числа. Функция proxy позволяет нам извлечь значение из типа-конструктора Succ, так мы поясняем ком-
пилятору тип значения. При этом мы нигде не пользуемся значениями типов Zero и Succ, ведь у этих типов
нет значений. Поэтому в экземпляре для Zero мы пользуемся постоянной функцией const.
Теперь посмотрим, что у нас получилось:
Prelude> :l Nat
*Nat> let x = undefined :: (Mul (Succ (Succ (Succ Zero))) (Succ (Succ Zero)))
*Nat> toInt x
6
Видно, что с помощью класса Nat мы можем извлечь значение, закодированное в типе. Зачем нам эти
странные типы-значения? Мы можем использовать их в двух случаях. Мы можем кодировать значения в типе
или проводить более тонкую проверку типов.
Помните когда-то мы определяли функции для численного интегрирования. Там точность метода была
жёстко задана в тексте программы:
dt :: Fractional a => a
dt = 1e-3
— метод Эйлера
int :: Fractional a => a -> [a] -> [a]
int x0 ~(f:fs) = x0 : int (x0 + dt * f) fs
В этом примере мы можем создать специальный тип потоков, у которых шаг дискретизации будет зако-
дирован в типе.
data Stream n a = a :& Stream n a
Параметр n кодирует точность. Теперь мы можем извлекать точность из типа:
dt :: (Nat n, Fractional a) => Stream n a -> a
dt xs = 1 / (fromIntegral $ toInt $ proxy xs)
where proxy :: Stream n a -> n
proxy = undefined
int :: (Nat n, Fractional a) => a -> Stream n a -> Stream n a
int x0 ~(f:& fs) = x0 :& int (x0 + dt fs * f) fs
Теперь посмотрим как мы можем сделать проверку типов более тщательной. Представим, что у нас есть
тип матриц. Известно, что сложение определено только для матриц одинаковой длины, а для умножения
матриц число столбцов одной матрицы должно совпадать с числом колонок другой матрицы. Мы можем
отразить все эти зависимости в целочисленных типах:
data Mat n m a = …
instance Num a => AdditiveGroup (Mat n m a) where
a ^+^ b
= …
zeroV
= …
negateV a
= …
mul :: Num a => Mat n m a -> Mat m k a -> Mat n k a
При таких определениях мы не сможем сложить матрицы разных размеров. Причём ошибка будет вычис-
лена до выполнения программы. Это освобождает от проверки границ внутри алгоритма умножения матриц.
Если алгоритм запустился, то мы знаем, что размеры аргументов соответствуют.
Скоро в ghc появится поддержка чисел на уровне типов. Это будет специальное расширение
TypeLevelNats, при включении которого можно будет пользоваться численными литералами в типах,
также будут определены операции-семейства типов на численных типах с привычными именами +, *.
Классы с несколькими типами
Рассмотрим несколько полезных расширений, относящихся к определению классов и экземпляров клас-
сов. Расширение MultiParamTypeClasses позволяет объявлять классы с несколькими аргументами. Например
взгляните на такой класс:
class Iso a b where
to
:: a -> b
from
:: b -> a
Так мы можем определить изоморфизм между типами a и b
260 | Глава 17: Дополнительные возможности
Экземпляры классов для синонимов
Расширение TypeSynonymInstances позволяет определять экземпляры для синонимов типов. Мы уже
пользовались этим расширением, когда определяли рекурсивные типы через тип Fix, там нам нужно бы-
ло определить экземпляр Num для синонима Nat:
type Nat = Fix N
instance Num Nat where
В рамках стандарта все суперклассы должны быть простыми. Все они имеют вид T a. Если мы хотим хотим
использовать суперклассы с составными типами, нам придётся подключить расширение FlexibleContexts.
Этим расширением мы пользовались, когда определяли экземпляр Show для Fix:
instance Show (f (Fix f)) => Show (Fix f) where
show x = ”(” ++ show (unFix x) ++ ”)”
Функциональные зависимости
Класс можно представить как множество типов, для которых определены данные операции. С появлением
расширения MultiParamTypeClasses мы можем определять операции класса для нескольких типов. Так наше
множество классов превращается в отношение. Наш класс связывает несколько типов между собой. Если из
одной компоненты отношения однозначно следует другая, такое отношение принято называть функцией.
Например обычную функцию одного аргумента можно представить как множество пар (x, f x). Для того
чтобы множество таких пар было функцией необходимо, чтобы выполнялось свойство:
forall x, y.
x == y => f x == f y
Для одинаковых входов мы получаем одинаковые выходы. С функциональными зависимостями мы мо-
жем ввести такое ограничение на классы с несколькими аргументами. Рассмотрим практический пример.
Библиотека Boolean определяет обобщённые логические значения,
class Boolean b where
true, false :: b
notB
:: b -> b
(&&*), (||*) :: b -> b -> b
Логические значения определены в терминах простейших операций, теперь мы можем обобщить связку
if-then-else и классы Eq и Ord:
class Boolean bool => IfB bool a | a -> bool where
ifB :: bool -> a -> a -> a
class Boolean bool => EqB bool a | a -> bool where
(==*), (/=*) :: a -> a -> bool
class Boolean bool => OrdB bool a | a -> bool where
(<*), (>=*), (>*), (<=*) :: a -> a -> bool
Каждый из классов определён на двух типах. Один из них играет роль обычных логических значений, а
второй тип~– это такой же параметр как и в обычных классах из модуля Prelude. В этих определениях нам
встретилась новая конструкция: за переменными класса через разделитель “или” следует что-то похожее на
тип функции. В этом типе мы говорим, что из типа a следует тип bool, или тип a однозначно определяет тип
bool. Эта информация помогает компилятору выводить типы. Если он встретит в тексте выражение v = a <*
b и тип одного из аргументов a или b известен, то тип v будет определён по зависимости.
