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

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

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

  • многие рассматривали ранее, на правах напоминания

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

  • над типами определены операции “сложения” и “умножения”
  • Сумма типов – дизъюнктное объединение значений входящих в неё типов
  • Произведение типов – множество кортежей, элементы – значения входящих в него типов
  • Тип стрелки (функции) a -> b связывают с возведением в степень, \(b^a \sim a \to b\)

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

Мощность типа
Число различных значений, допустимых типом. Для типа \(\alpha\) обозначается \(\abs{\alpha}\)
  • Мощность () – \(1\)
  • Мощность Bool – \(2\)
  • и т.п.
  • Тип с мощностью 0:
data Void = Void Void

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

data Void -- определено в Data.Void
  • Мощность суммы типов: \(\abs{α + β} = \abs{α}+\abs{β}\)
  • Мощность произведения типов: \(\abs{α · β} = \abs{α}·\abs{β}\)
  • Мощность стрелки: \(\abs{α\to β} = \abs{β}^\abs{α}.\)
f :: Bool -> Void
g :: Bool -> ()
h :: Bool -> Bool
q :: () -> Int
  • Число возможных реализаций f – 0
  • Число возможных реализаций 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 и т.п.
  • Род Constraint – слева от =>, т.е. Class a :: Constraint, где Class – класс типа с одним аргументом (расширение ConstraintKinds)
  • система родов достаточно бедная
  • DataKinds делает все пользовательские типы также и родами
  • data MyBool = MyTrue | MyFalse ⇒ род MyBool, населённый типами MyTrue и MyFalse
  • Перед названием автоматически созданных типов ставится одинарная кавычка, i.e. 'MyTrue, чтобы разрешить неоднозначность

Встроенные типы:

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

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

Какие являются функторами?

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)

Для ответа – понятие вариантности.

Виды вариантности:

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

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

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

(из библиотеки invariant)

  • Вариантность полностью определяется положением переменной типа в определении.
  • Отрицательные позиции они порождают контравариантность
  • Положительные – ковариантность
  • Если переменная и в положительных и в отрицательных позициях, то тип инвариантный
  • В алгебраических типах, отрицательная позиция – в аргументе функции.
  • Вариантность производных алгебраических типов алгебраически – минус на минус даёт плюс, плюс на минус даёт минус.
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)

--               ^ отрицательная


--              ^^^^^^^^^ на отрицательной
                                    -- ковариантный
data T1 a = T1 (Int -> a)
instance Functor T1 where
  fmap f (T1 x) = T1 (f . x)

data T2 a = T2 (a -> Int)
instance Contravariant T2 where
  contramap f (T2 x) = T2 (x . f)

data T3 a = T3 (a -> a)
instance Invariant T3 where
  invmap f g (T3 x) = T3 (f . x . g)

data T4 a = T4 ((Int -> a) -> Int)
instance Contravariant T4 where
  contramap f (T4 x) = T4 (\g -> x (f . g))

data T5 a = T5 ((a -> Int) -> Int)
instance Functor T5 where
  fmap f (T5 x) = T5 (\g -> x (g . f))
  • для распространённых типов с несколькими переменными – специальные термины
Бифунктор (Bifunctor)
Тип, ковариантный в двух аргументах
В base в модуле Data.Bifunctor
Профунктор (Profunctor)
Тип, контравариантный в первом аргументе и ковариантный во втором
В пакете profunctors.
  • отметим, что многопараметрические классы типов требуют расширения MultiParamTypeClasses.

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

  • По сути, функции на уровне типов
  • Расширение TypeFamilies
  • Включает также открытые семейства типов и семейства данных.

Синтаксис:

type family F x y where
  F x y = -- ...
  -- ...
type family And (x :: Bool) (y :: Bool) :: Bool where
  And True True = True
  And _ _ = False
  • важное различие: семейства типов в общем нельзя применять частично
  • функции на уровне типов – не каррированные
  • следствие – нельзя определить функции высшего порядка (такие как Map)
  • Это ограничение можно обойти, см. https://github.com/Lysxia/first-class-families

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

  • расширение FunctionalDependencies
  • функциональные зависимости между параметрами классов типов
class Foo a b c | a b -> c where
  -- ...
  • Аннотация может иметь несколько определений, несколько переменных в правых частях
class Bar a b c d e | a b -> c d, e -> a where
  -- ...
  • функциональные зависимости можно включить для семейств типов
  • расширение TypeFamilyDependencies
  • в левой части ФЗ семейства типов может быть только результат
  • поэтому ФЗ только одна
type family Id a = r | r -> a -- ...
type family Foo a b = r | r -> a b -- ...
type family Bar a b = r | r -> b -- ...

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 можно обойти это ограничение
  • По умолчанию тайпчекер запрещает даже объявление таких типов
  • Отключить проверку можно расширением AllowAmbiguousTypes.

До появления TypeApplications использовался

data Proxy a = Proxy

Например, в Typeable есть функция

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

(упрощённая сигнатура)

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

type NotProxy a = ()

someFunc :: Show a => NotProxy a -> String
someFunc = _
  • формально a находится справа от =>
  • но синонимы типов (включая семейства типов) разрешаются до проверки однозначности
  • на самом деле компилятор проверяет однозначность для someFunc :: Show a => () -> String
  • даже если бы этой проверки не было, в месте вызова someFunc () не было бы никаких указаний на тип a.
  • синоним type NotProxy a = () отличается от типа data Proxy a = Proxy.
  • Любой тип Proxy a изоморфен типу ()
  • Но объявление data Proxy a объявляет новый конструктор типа Proxy
  • NotProxy не объявляет тип.

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

Выражения слева от => имеют род 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)
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)

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

  • функции могут быть полиморфными
  • функции могут передаваться в качестве аргументов
  • но аргументы функции не могут иметь полиморфный тип!
  • Причина – проверка типов при наличии полиморфизма высшего ранга алгоритмически неразрешима
  • ограничение можно отключить расширением 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
  • Identity a - монада
  • можно ожидать что forall r. (a -> r) -> r – монада

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