[1 of 1] Compiling Point2D
( Point2D. hs, interpreted )
Ok, modules loaded: Point2D.
*Point2D> let v =
V2 1 2
*Point2D> v ^+^ v
V2 2 4
*Point2D> 3 *^ v ^+^ v
V2 4 8
*Point2D> negateV $ 3 *^ v ^+^ v
V2 (-4) (-8)
Семейства функций дают возможность организовывать вычисления на типах. Посмотрим на такой клас-
сический пример. Реализуем в типах числа Пеано. Нам понадобятся два типа. Один для обозначения нуля,
а другой для обозначения следующего элемента:
{-# Language TypeFamilies, EmptyDataDecls #-}
module Nat where
data Zero
data Succ a
Значения этих типов нам не понадобятся, поэтому мы воспользуемся расширением EmptyDataDecls, ко-
торое позволяет определять типы без значенеий. Значениями будут комбинации типов. Мы определим опе-
рации сложения и умножения для чисел. Для начала определим сложение:
type family Add a b :: *
type instance Add a Zero
= a
type instance Add a (Succ b)
= Succ (Add a b)
Первой строчкой мы определили семейство функций Add, у которого два параметра. Определение семей-
ства типов начинается с ключевой фразы type family. За двоеточием мы указали тип семейства. В данном
случае это простой тип без параметра. Далее следуют зависимости типов для семейства Add. Зависимости
типов начинаются с ключевой фразы type instance. В аргументах мы словно пользуемся сопоставлением с
образцом, но на этот раз на типах. Первое уравнение:
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. Семейства типов фактически позволяют нам определять функции на типах. Это
ведёт к тому, что алгоритм вывода типов становится неопределённым. Если типы правильные, то компиля-
тор сможет это установить, но если они окажутся неправильными, может возникнуть такая ситуация, что