верим результаты. Для этого мы создадим специальный класс, который будет переводить значения-типы в
обычные целочисленные значения:
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