Unknown - haskell-notes

typefamily Adda b :: *

type instance Adda Zero

=a

type instance Adda ( Succb)

= Succ( Adda b)

Первой строчкой мы определили семейство функций Add, у которого два параметра. Определение семей-

ства типов начинается с ключевой фразы typefamily. За двоеточием мы указали тип семейства. В данном

случае это простой тип без параметра. Далее следуют зависимости типов для семейства Add. Зависимости

типов начинаются с ключевой фразы type instance. В аргументах мы словно пользуемся сопоставлением с

образцом, но на этот раз на типах. Первое уравнение:

type instance Adda Zero

=a

Говорит о том, что если второй аргумент имеет тип ноль, то мы вернём первый аргумент. Совсем как в

обычном функциональном определении сложения для натуральных чисел Пеано. а во втором уравнении мы

составляем рекурсивное уравнение:

type instance Adda ( Succb)

= Succ( Adda b)

Точно также мы можем определить и умножение:

typefamily Mula b :: *

type instance Mula Zero

= Zero

type instance Mula ( Succb)

= Adda ( Mula b)

При этом нам придётся подключить ещё одно расширение UndecidableInstances, поскольку во втором

уравнении мы подставили одно семейство типов в другое. Этот флаг часто используется в сочетании с рас-

ширением TypeFamilies. Семейства типов фактически позволяют нам определять функции на типах. Это

ведёт к тому, что алгоритм вывода типов становится неопределённым. Если типы правильные, то компиля-

тор сможет это установить, но если они окажутся неправильными, может возникнуть такая ситуация, что

компилятор зациклится и будет бесконечно долго искать соответствие одного типа другому. Теперь про-

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

обычные целочисленные значения:

class Nata where

toInt ::a -> Int

instance Nat Zero where

toInt =const 0

instance Nata => Nat( Succa) 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> letx =undefined ::( Mul( Succ( Succ( Succ Zero))) ( Succ( Succ Zero)))

*Nat>toInt x

6

Видно, что с помощью класса Natмы можем извлечь значение, закодированное в типе. Зачем нам эти

странные типы-значения? Мы можем использовать их в двух случаях. Мы можем кодировать значения в типе

или проводить более тонкую проверку типов.

Помните когда-то мы определяли функции для численного интегрирования. Там точность метода была

жёстко задана в тексте программы:

dt :: Fractionala =>a

dt =1e-3

-- метод Эйлера

int :: Fractionala =>a ->[a] ->[a]

int x0 ~(f :fs) =x0 :int (x0 +dt *f) fs

В этом примере мы можем создать специальный тип потоков, у которых шаг дискретизации будет зако-

дирован в типе.

data Streamn a =a :& Streamn a

Параметр n кодирует точность. Теперь мы можем извлекать точность из типа:

dt ::( Natn, Fractionala) => Streamn a ->a

dt xs =1 /(fromIntegral $toInt $proxy xs)

whereproxy :: Streamn a ->n

proxy =undefined

int ::( Natn, Fractionala) =>a -> Streamn a -> Streamn a

int x0 ~(f :&fs) =x0 :&int (x0 +dt fs *f) fs

Теперь посмотрим как мы можем сделать проверку типов более тщательной. Представим, что у нас есть

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

матриц число столбцов одной матрицы должно совпадать с числом колонок другой матрицы. Мы можем