haskell-notes

*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 <*

Страницы: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162