Расширения:

{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE NoStarIsType             #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE TypeFamilyDependencies   #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE FunctionalDependencies   #-}

Общие импорты:

import Data.Kind
import GHC.TypeLits
import Data.Type.Equality
import Data.Proxy
import Prelude hiding (odd, even)

Классы типов как утверждения конструктивной логики

Ограничения в левой части “контекстной стрелки” => можно рассматривать как условия, в правой – как следствия, т.е. контекстную стрелку можно рассматривать как логическую импликацию. Тогда классы типов объявляют предикаты, а экземпляры классов типов – аксиомы (без условий) и теоремы (с условиями) на объявленных предикатах.

Таким образом, механизм классов типов Haskell можно рассматривать как ограниченный логический язык.

Рассмотрим задачу:

В преступлении подозреваются 4 лица: A, B, C, D. Следствие установило следующие факты: 1. Если виновен A, то виновен и B. 2. Если виновен B, то С виновен или A невиновен. 3. Если D невиновен, то А виновен и C невиновен. 4. Если D виновен, то и А виновен.

Введём типы для логических переменных A, B, C, D:

data A
data B
data C
data D

Или, используя DataKinds введём род Suspect населённый (пустыми) типами A, B, C, D (далее полагается этот вариант)

data Suspect = A | B | C | D

Теперь введём предикат P a, соответствующий “виновности” аргумента a:

class P (a :: Suspect)

Запишем условие (1) в виде теоремы, создав экземпляр класса P. Формально \(P(A)\vdash P(B)\)

instance P A => P B

Запишем условие (2) в виде теоремы. Для этого условие (2) необходимо выразить в терминах импликации, в левой части которой одиночный предикат, конъюнкция, или дизъюнкция, а в правой либо одиночный предикат, либо конъюнкция. Отрицание в рамках логической системы классов типов не выражается.

Тогда, формально, \[P(B) \vdash (P(C) \vee \neg P(A))\]

Пользуясь стандартными законами алгебры логики, получаем:

\[\lnot P(B) \vee (P(C) \vee \neg P(A))\] \[\lnot P(B) \vee P(C) \vee \neg P(A)\] \[\lnot P(B) \vee \neg P(A) \vee P(C)\] \[\lnot (P(B) \land P(A)) \vee P(C)\] \[(P(B) \land P(A)) \vdash P(C)\]

instance (P B, P A) => P C

Запишем (3) в виде теоремы.

\[\lnot P(D)\vdash (P(A) \land \lnot P(C))\] \[P(D) \vee (P(A) \land \lnot P(C))\] \[(P(D) \vee P(A)) \land (P(D) \vee \lnot P(C))\] \[(P(D) \vee P(A)) \land (P(C) \vdash P(D))\]

Условие таким образом разделяется на два, которые независимо истины: \(P(A) \vee P(D)\) и \(P(C) \vdash P(D)\). Первую часть условия выразить в терминах классов типов проблематично, поэтому пока запомним его, но не будем записывать. Вторая часть записывается тривиально:

instance P C => P D

Наконец, 4 условие тривиально:

instance P D => P A

Несмотря на то, что мы опустили часть условия \(P(A) \vee P(D)\), посмотрим что думает компилятор. Чтобы затребовать от компилятора решение ограничений мы должны использовать выражение с соответствующим ограничением. Введём такое выражение:

sol :: P a => ()
sol = ()

Теперь можно запросить у компилятора тип выражений sol @A, sol @B, sol @C, sol @D: если предикат P для соответствующего типа ложный, компилятор вернёт ошибку.

_ = sol @A
_ = sol @B
_ = sol @C
_ = sol @D

Компилятор не возвращает ошибку, т.е. он считает, что предикат верный для всех типов A, B, C, D. Проверим, что пропущенное нами условие выполняется: \(P(A) \vee P(D)\) действительно, если предикат верен для \(A\) или \(D\), то это условие выполняется. Оказывается, для получение решения оно не необходимо. Получаем ответ: все виновны.

Выражение отношений через классы и семейства типов

Рассмотрим стандартный пример для языка Prolog: есть лица Anne, Bridget, Caroline, Donna, Emily, состоящие в родственных связях, выражаемых предикатом child:

child(anne,bridget).
child(bridget,caroline).
child(caroline,donna).
child(donna,emily).

Задача в том, чтобы получить предикат descend, истинный, если предикатом child образуется цепочка:

child(X,Y) ⊢ descend(X,Y).
child(X,Z), descend(Z,Y) ⊢ descend(X,Y).

Определим семейство Person (используя DataKinds):

data Person = Anne | Bridget | Caroline | Donna | Emily

Определим предикат Child. Поскольку этот предикат является по сути унарной функцией, введём такую функцию с помощью закрытого семейства типов:

type family Child' a where
  Child' Anne     = Bridget
  Child' Bridget  = Caroline
  Child' Caroline = Donna
  Child' Donna    = Emily

Введём теперь предикат Child на основе этой функции:

class Child a b | a -> b
instance  (Child' a ~ b) => Child a b

Отметим, что мы используем синтаксис FunctionalDependencies чтобы пометить, что b однозначно определяется из a, и в экземпляре требуем, чтобы Child a b выполнялся только если Child' a = b.

Мы можем написать функцию получения родителя, например

parent :: Child a b => Proxy b
parent = Proxy

тогда узнать родителя скажем Caroline можно запросив тип parent @Caroline:

_ :: Proxy Donna = parent @Caroline

(мы ожидаем что результат Donna поэтому здесь явно указан тип)

Теперь мы можем написать предикат Descend:

class Descend (a :: Person) (b :: Person)

При попытке сформулировать условия для экземпляров нас однако ждёт неприятность:

instance Child x y => Descend x y
instance (Child x z, Descend z y) => Descend x y

Компилятор сообщает об ошибке: Duplicate instance declarations. Причина в том, что экземпляры определяются только по правой части, и только после этого проверяется левая. Поскольку правые части здесь одинаковые, компилятор считает их дублирующимися. Обойти это ограничение можно введя дополнительный параметр – здесь поскольку вариантов два, этот параметр имеет тип Bool и соответствует “прямому наследованию” (т.к. в первом экземпляре наследование прямое, а во втором – нет):

class Descend' (a :: Person) (b :: Person) (direct :: Bool)
instance Child x y => Descend' x y True
instance (Child x z, Descend z y) => Descend' x y False

Теперь мы можем выразить Descend через Descend':

instance (Descend' x y (Child' x == y)) => Descend x y

Введём вспомогательную функцию для получения результата:

descend :: Descend a b => ()
descend = ()

Теперь истинность или ложность предиката Descend можно определить, запросив тип descend. Если предикат ложный, компилятор вернёт ошибку. Следующие утверждения истины:

_ :: () = descend @Anne @Bridget
_ :: () = descend @Anne @Caroline
_ :: () = descend @Anne @Emily

А эти ложны:

_ :: () = descend @Emily @Anne
_ :: () = descend @Anne @Anne

Единственный нюанс в том, что сообщение об ошибке не слишком понятное:

No instance for (Descend' 'Emily 'Anne (Child' 'Emily == 'Anne))
  arising from a use of ‘descend’

Чтобы получить более понятное сообщение, можно использовать “магическое” семейство типов TypeError в определении Child':

type family Child' a where
  Child' Anne     = Bridget
  Child' Bridget  = Caroline
  Child' Caroline = Donna
  Child' Donna    = Emily
  -- новая строчка
  Child' _ = TypeError (Text "No descend")

Тогда вместо неудобного сообщения об ошибке компилятор выведет No descend. Тип TypeError определён в модуле GHC.TypeLits. Есть операторы для форматирования вывода, подробное описание в документации.

Числа Пеано и простые предикаты на них

Мы можем ввести род, изоморфный натуральным числам:

data Peano = Z | S Peano

Эта конструкция называется конструкцией Пеано, поскольку основана на системе аксиом натуральных чисел, сформулированной Джузеппе Пеано в XIX веке.

Z соответствует нулю, а S – это оператор следования. Тогда числа представляются в виде:

type P0 = Z
type P1 = S Z
type P2 = S (S Z)
type P3 = S (S (S Z))
type P4 = S (S (S (S Z)))
type P5 = S (S (S (S (S Z))))
-- ...

Мы можем ввести простые предикаты над этими числами:

class Even (n :: Peano)
class Odd (n :: Peano)

и простые конструктивные теоремы на этих предикатах. Аксиоматически примем, что 0 – чётное:

instance Even P0

Теперь, определим что чётные и нечётные чередуются. Следующее за нечётным – чётное:

instance Odd n => Even (S n)

Следующее за чётным – нечётное:

instance Even n => Odd (S n)

Введём вспомогательные функции и проверим что это работает:

even :: Even n => ()
even = ()

odd :: Odd n => ()
odd = ()

_ :: () = odd @P1
_ :: () = even @P2
_ :: () = odd @P3
_ :: () = even @P4

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

class Add a b c | a b -> c

Здесь мы вводим предикат Add(a,b,c), где c – результат сложения a + b и говорим, что c функционально зависит от a, b.

Значения определяются аксиоматически, сложение с 0 даёт то же число:

instance Add Z b b

Сложение с большим на 1 даёт результат больше на 1:

instance Add a b c => Add (S a) b (S c)

Отметим, что здесь мы фиксируем первый аргумент и по нему же выполняем рекурсию. Эквивалентно можно было бы определить

instance Add a Z a
instance Add a b c => Add a (S b) (S c)

Но вот комбинировать эти варианты не получится. Действительно, из аксиомы Add a Z a никак не следует верность теоремы instance Add a b c => Add (S a) b (S c), поскольку аргументы предиката на разных местах. Коммутативность сложения компилятору неизвестна. Впрочем, можно её ввести, но чтобы компилятор мог разрешить неоднозначности, придётся использовать IncoherentInstances:

instance Add a b c => Add (S a) b (S c)
instance {-# INCOHERENT #-} Add b Z b
instance {-# OVERLAPPABLE #-} Add a b c => Add b a c

Прагма OVERLAPPABLE означает, что если возможно выбрать более конкретный экземпляр, будет выбран он. Прагма INCOHERENT в случае неоднозначности выбирает в случае неоднозначности произвольный экземпляр, помеченный как INCOHERENT. Обычно этих прагм стараются избегать, поскольку они часто приводят к неожиданному поведению.

Проверим однако что всё работает, запросим тип add @P2 @P3:

_ :: Proxy P5 = add @P2 @P3

(здесь тип результата P5 указан явно, но компилятор может его вывести)

Понятно, что вместо класса типов можно было бы использовать закрытое семейство типов:

type family Add' (x :: Peano) (y :: Peano) :: Peano where
  Add' Z y = y
  Add' (S x) y = S (Add' x y)

_ :: Proxy P5 = Proxy @(Add' P2 P3)

Сильно типизированные гетерогенные списки

Для объявления гетерогенных списков нам потребуется GADTs. Информацию о типе элементов будем хранить в списке на уровне типов:

data HList (ts :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t : ts)

HNil конструирует пустой список, поэтому соответствующий список на уровне типов также пуст. HCons добавляет элемент типа t в начало списка, поэтому тип t добавляется также в начало списка на уровне типов.

Объявим HCons как оператор:

infixr 5 `HCons`

для краткости также введём синоним:

(/:) = HCons
infixr 5 /:

Теперь мы можем конструировать списки с элементами разных типов:

example, example2 :: HList [Int, String, Float]
example = 1 /: "test" /: 1.0 /: HNil
example2 = 2 /: "test" /: 1.0 /: HNil

Теперь чтобы сравнить списки нам потребуется определить экземпляр Eq. Для GADTs мы не можем использовать deriving, но мы можем определить его вручную:

instance Eq (HList '[]) where
  HNil == HNil = True

instance (Eq t, Eq (HList ts)) => Eq (HList (t : ts)) where
  (HCons x xs) == (HCons y ys) = x == y && xs == ys

Для второго случая мы можем также использовать StandaloneDeriving:

deriving instance (Eq t, Eq (HList ts)) => Eq (HList (t : ts))

Для случая HNil оно однако не сработает.

Это однако несколько неудобно: хотелось бы иметь один экземпляр и желательно автоматически выводимый. По сути два экземпляра нам нужны чтобы потребовать Eq t для всех элементов списка типов. Сделаем это явно. Для этого объявим функциональный предикат All используя закрытое семейство типов и тип Constraint:

type All :: (Type -> Constraint) -> [Type] -> Constraint
type family All c ts where
  All c '[] = ()
  All c (t : ts) = (c t, All c ts)

Здесь использовано расширение StandaloneKindSignatures для читаемости, эквивалентно:

type family All (c :: Type -> Constraint) (ts :: [Type]) :: Constraint where
  All c '[] = ()
  All c (t : ts) = (c t, All c ts)

Теперь мы можем записать один экземпляр:

instance All Eq ts => Eq (HList ts) where
  HNil == HNil = True
  (HCons x xs) == (HCons y ys) = x == y && xs == ys

или затребовать у компилятора вывести его:

deriving instance All Eq ts => Eq (HList ts)

Аналогично можно определить экземпляр Show.

Списки фиксированной длины

Определим тип списка, который на уровне типа фиксирует длину. Используем введённые выше числа Пеано для длины:

data Vec (n :: Peano) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

infixr 5 `VCons`

Мы можем объявить автоматический экземпляр Show для этого типа:

deriving instance Show a => Show (Vec n a)

Также для этого типа можно определить функции map, concat, экземпляр Functor и т.п.:

mapVec :: (a -> b) -> Vec n a -> Vec n b
mapVec _ VNil = VNil
mapVec f (x `VCons` xs) = f x `VCons` mapVec f xs

concatVec :: Vec n a -> Vec m a -> Vec (Add' n m) a
concatVec VNil ys = ys
concatVec (VCons x xs) ys = x `VCons` concatVec xs ys

instance Functor (Vec n) where
  fmap = mapVec

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

Определим функцию получения n-го элемента списка. Для лучшей типобезопасности, введём тип конечного индекса, индексированного максимальной длиной:

data Fin (n :: Peano) where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n) -- index+1
     -- ^^^^ index

Смысл этого определения достаточно прост: для любого числа Пеано n, нулевой индекс требует хотя бы один элемент, т.е. ∀ n. m >= S n, прочие индексы строятся индуктивно: если есть индекс для вектора длины n, то есть следующий индекс для вектора длины S n.

Определим несколько конечных индексов:

f0 = FZ
f1 = FS f0
f2 = FS f1
f3 = FS f2
f4 = FS f3
f5 = FS f4

Теперь мы можем безопасно индексировать вектор:

index :: Fin n -> Vec n a -> a
index FZ (VCons x _) = x
index (FS n) (VCons _ xs) = index n xs

Проверим:

infixr #
x # y = VCons x y

index5 = index f5 (1 # 2 # 3 # 4 # 5 # 6 # VNil)
-- ошибка типизации:
-- index5' = index f5 (1 # 2 # 3 # VNil)

Конечно, на практике этот тип не слишком полезен, поскольку индекс должен быть известен на момент компиляции. Чтобы таким образом использовать индекс времени выполнения, нужны зависимые типы, в Haskell их пока нет. Их можно эмулировать используя библиотеку singletons, но это выходит за рамки данного курса.

Упраженения

Упражнение 1

Реализуйте функцию

zipVec :: Vec n a -> Vec n b -> Vec n (a, b)

Упражнение 2

Реализуйте экземпляр Applicative (Vec n)

Указание (сначала попробуйте самостоятельно; нажмите чтобы показать):

class ConstructVec (n :: Peano) where
  constructVec :: (Fin n -> a) -> Vec n a

Упражнение 3

Определите автоматический экземпляр Show (HList ts) используя синтаксис StandaloneDeriving, т.е. deriving instance ...

Упражнение 4

Реализуйте функцию

zipHList :: HList xs -> HList ys -> HList (Zip xs ys)

где

type Zip :: [Type] -> [Type] -> [Type]

это функция zip на уровне типов (которую тоже необходимо определить)

Указание (сначала попробуйте самостоятельно; нажмите чтобы показать):

type family Zip xs ys where
  Zip (x:xs) (y:ys) = (x, y) : Zip xs ys
  -- прочие паттерны ...

Упражнение 5 (*)

Является ли Vec n a монадой? Если да, напишите экземпляр.

Указание (сначала попробуйте самостоятельно; нажмите чтобы показать):