Программирование на уровне типов

Современный Haskell поддерживает различные техники программирования на уровне типов. Программирование на уровне типов – по сути, написание программ, которые будут выполнены на этапе проверки типов компилятором. Одна из техник метапрограммирования. Практически, используется для более точного описания предметной области – таким образом, чтобы некорректные термы были непредставимыми – и формальной верификации корректности.

В этой лекции мы обсудим некоторые расширения Haskell, которые делают программирование на уровне типов достаточно гибким для практических целей.

Основные понятия

Многие из этих понятий мы рассматривали ранее, но здесь они вновь понадобятся, поэтому на правах напоминания.

Алгебраические типы

Мы называем систему типов Haskell алгебраической, поскольку над типами определены алгебраические операции “сложения” и “умножения”. Сумма типов – это тип, представляющий дизъюнктное объединение элементов множеств значений входящих в неё типов. Произведение типов – это тип, представляющий множество кортежей, имеющих элементами значения входящих в него типов.

Дополнительно отметим, что тип стрелки (функции) a -> b часто связывают с возведением в степень, \(b^a \sim a \to b\)

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

Мощность типов

Мощность типа
Число различных значений, допустимых типом. Для типа \(\alpha\) обозначается \(\abs{\alpha}\)

Мощность типа () – \(1\), поскольку у типа () ровно одно значение – (). Мощность типа Bool – \(2\), поскольку у типа Bool ровно \(2\) значения и т.п.

Есть ли тип с мощностью \(0\)? Да, но его выражение в терминах стандартного Haskell98 несколько неожиданно:

data Void = Void Void

Это работает поскольку в соответствии с этим определением, чтобы сконструировать хотя бы одно значение типа Void, нам нужно иметь значение типа Void, а его ещё нет.

Haskell 2010 допускает определение Void вида

data Void

(это определение есть в стандартной библиотеке в модуле Data.Void начиная с GHC 7.10)

Результат одинаковый – тип с мощностью \(0\).

Мощность суммы типов – сумма мощностей входящих в сумму типов. \(\abs{α + β} = \abs{α}+\abs{β}\). В Haskell канонический тип-сумма – Either

Мощность произведения типов – произведение мощностей входящих в сумму типов. \(\abs{α · β} = \abs{α}·\abs{β}\). В Haskell канонический тип-произведение – пара (,)

Мощность стрелки – мощность правого операнда в степени мощности левого операнда: \(\abs{α\to β} = \abs{β}^\abs{α}.\)

Чтобы убедить себя в верности последнего утверждения, рассмотрим примеры

f :: Bool -> Void
g :: Bool -> ()
h :: Bool -> Bool
q :: () -> Int

Число возможных реализаций f – 0, поскольку нет способа вернуть значение типа Void.

Число возможных реализаций g – 1, поскольку есть только один способ вернуть () и это игнорировать аргумент.

Число возможных реализаций h – 4. Действительно,

  1. h = const True
  2. h = const False
  3. h = id
  4. h = not

Число возможных реализаций q – \(\abs{\mathrm{Int}}\).

Идея мощности типов подводит нас к идее изоморфизма.

Изоморфизм типов

Изоморфизм
обратимое однозначное преобразование между двумя типами

Между двумя типами одинаковой мощности всегда можно определить хотя бы один изоморфизм. Более того, между типами мощности \(n\) существует \(n!\) различных потенциальных изоморфизмов. Типы, между которыми определён изоморфизм будем называть изоморфными.

Род типа

Аналогично тому как в “обычном” программировании на Haskell нас интересуют термы и типы, в программировании на уровне типов нас интересуют типы и рода. Рода типов обсуждались ранее, но кратко повторимся, что род – это “тип типа”, термы имеют типы рода Type, конструкторы типов имеют род Type -> Type и т.п. в зависимости от числа аргументов.

В предыдущем изложении мы умолчали о том, какой род имеют выражения, находящиеся справа от =>. У выражений вида Class a, где Class – класс типа с одним аргументом, род Constraint. Однако чтобы иметь возможность воспользоваться этим фактом, необходимо расширение языка ConstraintKinds.

Как можно заметить, система родов в Haskell достаточно бедная. Это можно исправить расширением DataKinds. Это расширение делает все пользовательские типы также и родами, т.е. для объявлений вида data MyBool = MyTrue | MyFalse автоматически создаётся род типов kind MyBool, населённый типами MyTrue и MyFalse. Чтобы различить значения от типов, перед названием автоматически созданных типов ставится одинарная кавычка, i.e. 'MyTrue; в случаях когда не возникает неоднозначности, её можно опустить.

Встроенные типы естественно тоже получают отражение на уровне родов, но с некоторыми оговорками.

  • String соответствует роду Symbol. Литералы строк на уровне типов имеют род Symbol, не являются списками символов, операция конкатенации – AppendSymbol в модуле GHC.TypeLits, сравнение – CmpSymbol там же, прочие операции не определены.
  • Натуральные числа соответствуют роду Nat, прочие числа (отрицательные, дробные, etc) на уровень типов не отражаются. Определены операции +, *, ^, -, Div, Mod, Log2 и сравнение CmpNat.
  • Списки соответствуют роду [a] и типам '[] :: [a] и '(:) :: a -> [a] -> [a], где после :: указан род, и a – переменная рода. Надо отметить, что для конструктора пустого списка на уровне типов, '[], кавычка обязательна (ввиду пересечения с конструктором типа списка)
  • Кортежи соответствуют родам (a, b) и т.п. в зависимости от числа элементов. Конструкторы типов рода кортежей соответственно '(,) и т.п. Надо отметить, что для конструкторов кортежей на уровне типов кавычка обязательна (за крайне редким исключением)

Вариантность

Связанная с системой типов тема – вариантность. Хотя в дальнейшем изложении она не потребуется, полезно иметь о ней представление, поэтому затронем эту тему здесь.

Рассмотрим несколько типов. Какие из них являются функторами?

data T1 a = T1 (Int -> a)
data T2 a = T2 (a -> Int)
data T3 a = T3 (a -> a)
data T4 a = T4 ((Int -> a) -> Int)
data T5 a = T5 ((a -> Int) -> Int)

Ответ на этот вопрос помогает найти понятие вариантности. Вариантность зависит от вида типа T :: Type -> Type:

Ковариантность
Любая функция a -> b может быть единообразно преобразована к виду T a -> T b
Контравариантность
Любая функция a -> b может быть единообразно преобразована к виду T b -> T a
Инвариантность
Любая функция a -> b неможет быть единообразно преобразована к типам T a, T b

Определение ковариантности – это по сути и есть определение Functor. Строго говоря, в теории категорий Functor называется ковариантным функтором.

Для контравариантных типов можно определить конртавариантный функтор

class Contravariant f where
  contramap :: (a -> b) -> f b -> f a

(определение из библиотеки contravariant)

Для инвариантных типов можно определить “инвариантный функтор”, но только если типы функции изоморфны:

class Invariant f where
  invmap :: (a -> b) -> (b -> a) -> f a -> f b

Вариантность типа (точнее конструктора типа) полностью определяется положением переменной типа в определении. Позиции называются отрицательными, если они порождают контравариантность, положительными – если ковариантность. Если переменная встречается и в положительных и в отрицательных позициях, то тип инвариантный.

В рамках алгебраических типов, отрицательная позиция всего одна – в аргументе функции. Вариантность производных алгебраических типов вычисляется алгебраически – минус на минус даёт плюс, плюс на минус даёт минус.

data T1 a = T1 (Int -> a) -- ковариантный
                    -- ^ положительная позиция
data T2 a = T2 (a -> Int) -- контравариантный
             -- ^ отрицательная позиция
data T3 a = T3 (a -> a) -- инвариантный
--отрицательная ^    ^ положительная
data T4 a = T4 ((Int -> a) -> Int) -- контравариантный
--                      ^ положительная
--              ^^^^^^^^^ на отрицательной
data T5 a = T5 ((a -> Int) -> Int) -- ковариантный
--               ^ отрицательная
--              ^^^^^^^^^ на отрицательной
instance Functor T1 where
  fmap f (T1 x) = T1 (f . x)
instance Contravariant T2 where
  contramap f (T2 x) = T2 (x . f)
instance Invariant T3 where
  invmap f g (T3 x) = T3 (f . x . g)
instance Contravariant T4 where
  contramap f (T4 x) = T4 (\g -> x (f . g))
instance Functor T5 where
  fmap f (T5 x) = T5 (\g -> x (g . f))

Есть некоторые специальные термины для распространённых типов с несколькими переменными. Тип, ковариантный в двух аргументах называется бифунктором (Bifunctor), тип, контравариантный в первом аргументе и ковариантный во втором называется профунктором (Profunctor). Классы профункторов определены в пакете profunctors. Бифункторы есть в base в модуле Data.Bifunctor. Следует отметить, что многопараметрические классы типов требуют расширения MultiParamTypeClasses.

Закрытые семейства типов

Закрытые семейства типов – это, по сути, функции на уровне типов. Расширение языка называется TypeFamilies, оно включает также открытые семейства типов и семейства данных.

Синтаксис закрытых семейств типов:

type family F x y where
  F x y = -- ...
  -- ...

Например, определим аналог конъюнкции для рода Bool. Для этого укажем явные аннотации родов:

type family And (x :: Bool) (y :: Bool) :: Bool where
  And True True = True
  And _ _ = False

У семейств типов и функций на уровне значений есть одно важное различие: семейства типов в общем нельзя применять частично. Иными словами, функции на уровне типов – не каррированные. Как следствие, на уровне типов таким образом нельзя определить функции высшего порядка (такие как Map). Это ограничение можно обойти, но это выходит за рамки данного изложения1.

Функциональные зависимости

Используя расширение FunctionalDependencies можно добавить к классам типов аннотацию функциональных зависимостей между параметрами:

class Foo a b c | a b -> c where
  -- ...

Такая аннотация говорит, что достаточно знать a и b, и параметр c полностью ими определяется.

Вообще говоря, функциональные зависимости выполняют роль, аналогичную открытым семействам типов.

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

Если у класса есть аннотация ФЗ, компилятор запретит объявление противоречащих этой аннотации экземпляров, но сможет вывести правые части ФЗ из левых.

Кроме того, функциональные зависимости можно включить для семейств типов при помощи расширения TypeFamilyDependencies. Ограничение в том, что в левой части ФЗ семейства типов может быть только результат, и поэтому ФЗ только одна:

type family Id a = r | r -> a -- ...

TypeApplications

Использование программирования на уровне типов часто требует подсказок для тайпчекера. “Канонический” способ это делать – вставлять аннотации типов выражений. Это однако достаточно неудобный и многословный вариант. Более простой вариант – использование расширения TypeApplications, позволяющего явно фиксировать значения переменных типа в месте вызова. Для этого имена фиксируемых типов указываются с префиксом @ после вызова функции как дополнительные аргументы, например:

> :type fmap
fmap :: Functor f => (a -> b) -> f a -> f b
> :type fmap @[] -- фиксиурем f = []
fmap :: (a -> b) -> [a] -> [b]

Переменные типов фиксируются в том порядке, в котором они встречаются в сигнатуре. Кроме того, фиксацию можно явно пропустить подставив на соответствующее место “улитку” @_:

> :type fmap @[] @Int -- фиксиурем f = [], a = Int
fmap :: (Int -> b) -> [Int] -> [b]
> :type fmap @_ @_ @String -- фиксиурем b = String
fmap :: Functor _1 => (_2 -> String) -> _1 _2 -> _1 String

Следует отметить, что система типов Haskell требует чтобы все переменные типов встречались справа от => (поскольку иначе тайпчекер не сможет их вывести на основе типов аргументов). Используя TypeApplications можно обойти это ограничение, но по умолчанию тайпчекер запрещает даже объявление таких типов (в сообщениях компилятора они называются ambiguous). Отключить эту проверку можно расширением AllowAmbiguousTypes.

Исторически (до появления TypeApplications) методом обхода этого ограничения являлся тип

data Proxy a = Proxy

который использовался в качестве фиктивного параметра. Например, в классе Typeable (реализующим механизмы динамической типизации) есть функция (сильно упрощённая сигнатура2)

typeRep :: Typeable a => Proxy a -> TypeRep

Семейства типов и синонимы типов могут сделать некоторые типы неочевидно “неоднозначными” (ambiguous). Например,

type NotProxy a = ()

someFunc :: Show a => NotProxy a -> String
someFunc = _

Несмотря на то что формально переменная a находится справа от =>, компилятор вернёт ошибку, если не включено расширение AllowAmbiguousTypes. Дело в том, что синонимы типов (включая семейства типов) разрешаются до проверки однозначности, поэтому на самом деле компилятор проверяет однозначность для someFunc :: Show a => () -> String. Действительно, даже если бы этой проверки не было, в месте вызова someFunc () не было бы никаких указаний на тип a.

Важно понимать отличие синонима type NotProxy a = () от типа data Proxy a = Proxy. Очевидно, что любой тип Proxy a изоморфен типу (). Однако объявление data Proxy a объявляет новый конструктор типа Proxy, в то время как NotProxy не объявляет тип. Как следствие, вызов вида

someFunc (() :: NotProxy Int)

является неоднозначным, поскольку NotProxy Int ≡ (), в то время как

someFunc' (Proxy :: Proxy Int)

где

someFunc' :: Show a => Proxy a -> String

является однозначным.

Эквивалентность типов

Выражения слева от => имеют род Constraint. Собственно такие выражения могут быть

  1. Полностью применёнными классами типов, например Show a
  2. Кортежами типов рода Constraint, например (Show a, Read a)
  3. Выражениями эквивалентности a ~ b, где ~ – оператор эквивалентности.

Технически, (~) :: k -> k -> Constraint, хотя в текущей реализации оператор ~ “магический”. Также его можно рассматривать как двухпараметрический класс class (~) a b, экземпляры которого есть только для случаев a = b, например instance (~) Int Int и т.п. В любом случае, ~ позволяет говорить об эквивалентности типов, скрывающихся за переменными типов в левой части =>.

someValue  :: Int
someValue' :: (a ~ Int) => a

Технически, эти определения эквивалентны.

Обобщённые алгебраические типы данных (GADTs)

GADTs – это расширение системы типов, позволяющее явно указывать сигнатуры для конструкторов данных. Рассмотрим несколько простых примеров:

data MyBool = MyTrue | MyFalse
data MyBool' where
  MyTrue :: MyBool'
  MyFalse :: MyBool'

Здесь определение не привносит ровно ничего нового, но более явно (и более многословно) определяет тип конструкторов.

data Expr = LitInt Int
          | LitFloat Double
          | Add Expr Expr
          | FAdd Expr Expr
data Expr where
  LitInt   :: Int -> Expr
  LitFloat :: Double -> Expr
  Add      :: Expr -> Expr -> Expr
  FAdd     :: Expr -> Expr -> Expr

Здесь тоже ничего нового. Следует, однако, заметить, что это определение не вполне типобезопасно – можно например сконструировать FAdd (LitInt 1) (LitFloat 2.0). Синтаксис GADTs позволяет параметризовать тип Expr типами аргументов:

data Expr a where
  LitInt   :: Int -> Expr Int
  LitFloat :: Double -> Expr Double
  Add      :: (Expr Int) -> (Expr Int) -> (Expr Int)
  FAdd     :: (Expr Double)
           -> (Expr Double)
           -> (Expr Double)

Строго говоря, GADTs не привносит ничего нового по сравнению с эквивалентностью типов – выражение выше просто синтаксический сахар для

data Expr a
  = a ~ Int    => LitInt Int
  | a ~ Double => LitFloat Double
  | a ~ Int    => Add (Expr Int) (Expr Int)
  | a ~ Double => FAdd (Expr Double) (Expr Double)

(правда это определение требует расширения ExistentialQuantification)

Полиморфизм высшего ранга

В стандартном Haskell, функции могут быть полиморфными. Также функции могут передаваться в качестве аргументов. Однако аргументы функции не могут иметь полиморфный тип! Причина у этого ограничения достаточно простая – задача проверки типов при наличии полиморфизма высшего ранга (т.е. при наличии полиморфных функций принимающих полиморфные аргументы) алгоритмически неразрешим. Но это ограничение можно снять расширением RankNTypes.

Например:

f :: (a -> a) -> Int
f g = g 5

Такое определение не сработает, поскольку a должен в таком варианте определяться в месте вызова f, и у компилятора нет никаких причин полагать что a ~ Int.

f :: (forall a . a -> a) -> Int
f g = g 5

Такое определение требует чтобы аргументом f была полиморфная функция – и исходя из сигнатуры это может быть только функция id.

Интересно отметить, что тип a изоморфен типу forall r. (a -> r) -> r, т.е. существует изоморфизм

cont :: a -> (forall r. (a -> r) -> r)
cont x f = f x

runCont :: (forall r. (a -> r) -> r) -> a
runCont c = c id

Использование значений типа forall r. (a -> r) -> r известно как стиль передачи продолжений (continuation passing style, CPS) – иными словами, программирование с использованием обратных вызовов (callback-ов).

Тип forall r. (a -> r) -> r изоморфен a, который в свою очередь изоморфен Identity a, поэтому можно ожидать что первый является монадой.

newtype Cont a = Cont (forall r. (a -> r) -> r)

instance Functor Cont where
  fmap f (Cont x) = Cont (\g -> x (g . f))
instance Applicative Cont where
  pure x = Cont ($ x)
  (Cont f) <*> x = f id <$> x
instance Monad Cont where
  (Cont x) >>= f = Cont $ \g -> case f (x id) of
    Cont y -> y g

По сути, использование оператора >>= без do-нотации использует CPS, передавая продолжение вторым аргументом >>=.

  1. Основной подход – дефункционализация – используется в библиотеке https://github.com/Lysxia/first-class-families↩︎

  2. На самом деле сигнатура выглядит так:

    typeRep ::
  forall k (proxy :: k -> *) (a :: k).
  Typeable a =>
  proxy a -> TypeRep

    это сделано чтобы вместо Proxy можно было использовать любой изоморфный тип.↩︎