Type-level Haskell

В прошлом уроке сигнатуры начали говорить: HasLog r сообщает, какой срез окружения трогает функция. Сегодня делаем следующий шаг: типы перестают только описывать данные и начинают вычислять. Phantom types вешают на значения метки, которых нет в памяти. GADTs учат конструкторы приносить доказательства. DataKinds переселяет значения на уровень типов, type families заводят там функции, а TypeApplications даёт всем этим управлять руками. В финале соберём мини-Servant на сорок строк: типизированный роутер, у которого тип обработчика вычисляется из типа API. После него сигнатуры настоящего Servant перестанут быть магией. И честно обсудим, где у этой мощи граница для прода.

Ты уже программировал на типах

Хорошая новость: всё это ты уже делал, только на другом языке. В разделе про TypeScript есть два урока про программирование на типах, фундамент и глубже. Там мы выяснили: система типов TS это полноценный язык со значениями (типы), функциями (дженерики), ветвлением (условные типы), рекурсией и сопоставлением с образцом (infer). В Haskell живёт тот же язык, но диалект другой:

Идея	TypeScript (раздел 04-ts)	Haskell
литеральный тип	'hello', 42	DataKinds: "hello" :: Symbol, 42 :: Nat
функция на типах	type Wrap<T> = { value: T }	конструктор типов, type family
ветвление	T extends U ? X : Y	уравнения закрытого семейства
сопоставление с образцом	infer	переменные в левых частях уравнений
список типов	кортеж [H, ...R]	'[Int, Bool], образец x ': xs
рекурсия	рекурсивный условный тип	рекурсивное семейство
сужение в рантайме	защитник x is T	GADT-матч приносит a ~ Int
брендирование	string & { __brand: 'UserId' }	phantom type, newtype
типизация самих типов	нет, всё проверяется при применении	kind-система

Последняя строка таблицы и есть главное различие. Type-level TypeScript это динамический язык: передай в утилитный тип что угодно, и ошибка вылезет где-то на применении, глубоко внутри. Type-level Haskell типизирован сам: у каждого типа есть свой тип (он называется kind), и мусор отбрасывается на границе, с понятной ошибкой. Второе различие тоже важное: в TS значения и типы живут в одном синтаксическом мире, литерал 42 сам по себе годится в тип. В Haskell миры разделены жёстко, и чтобы затащить значения в типы, нужен явный мост. Его строит DataKinds, и до него мы дойдём. А начнём с фундамента, которого в TS нет.

Kinds: типы для типов

Открой GHCi и спроси не :t, а :k:

ghci> :k Int
Int :: Type
ghci> :k Maybe
Maybe :: Type -> Type
ghci> :k Either
Either :: Type -> Type -> Type
ghci> :k Either String
Either String :: Type -> Type
ghci> :k Functor
Functor :: (Type -> Type) -> Constraint

Kind это тип типа. Int населён значениями, его kind это Type. Maybe сам по себе значений не имеет, это функция над типами: дай ему Int, получишь Maybe Int. Его kind Type -> Type, и ты уже встречал эту запись в уроке про функторы: инстанс Functor бывает только у конструкторов kind-а Type -> Type. Каррирование работает и здесь: Either String это частично применённый конструктор.

Заметь, что произошло. Мы поднялись на этаж выше, и там обнаружилась точно такая же дисциплина, как внизу: выражения (типы), функции (конструкторы), и система типов над ними (kind-ы). Попробуй собрать бессмыслицу:

ghci> :k Maybe Maybe
error: Expecting one more argument to Maybe
       Expected a type, but Maybe has kind Type -> Type

В TS аналогичная ошибка всплыла бы в момент использования, где-нибудь в пятой строке трассировки условных типов. Здесь её ловит kind-чекер на границе. Запомни этот этаж: весь урок мы будем заселять его новыми жильцами.

Phantom types: метка без багажа

Самый дешёвый type-level приём не требует ни одного расширения. 23 сентября 1999 года станция Mars Climate Orbiter сгорела в атмосфере Марса: один модуль считал импульс в ньютон-секундах, другой в фунт-секундах, и число 4.45 раза в сутки тихо съедало траекторию. Цена опечатки: 327 миллионов долларов. Тип Double у обоих модулей был одинаковый, в этом и беда.

Фантомный тип решает это меткой, которая существует только на этапе компиляции:

newtype Force unit = Force Double

data NewtonSeconds
data PoundSeconds

burn :: Force NewtonSeconds -> IO ()
burn (Force f) = fireThrusters f

Параметр unit объявлен слева, но справа не встречается: внутри всегда голый Double, рантайм-представление не меняется ни на байт. Зато Force PoundSeconds в burn уже не пролезет: компилятор отвергнет вызов, станция долетит. Типы NewtonSeconds и PoundSeconds пустые, без единого конструктора: значения нам не нужны, нужны только имена.

Этот приём давно живёт в экосистеме:

• ST s из урока про контейнеры: фантомный параметр s помечает поток мутаций, и rank-2 тип runST :: (forall s. ST s a) -> a не даёт изменяемой ссылке утечь наружу. Фантом плюс квантор как замок.
• пакет tagged: Tagged t a, универсальная метка для чего угодно.
• Proxy из Data.Proxy, о нём чуть позже: фантом в чистом виде, значение-носитель типа.

Связка со smart constructors из урока про ADT даёт классику прикладного кода, валидацию в типе:

newtype Input s = Input Text

data Raw
data Sanitized

sanitize :: Input Raw -> Maybe (Input Sanitized)

renderComment :: Input Sanitized -> Html

renderComment физически невозможно вызвать с непроверенной строкой: единственный способ получить Input Sanitized это пройти через sanitize. Сравни с брендированием в TS, string & { __brand: 'UserId' } из урока про мост: идея та же, ярлык на этапе компиляции, ноль следов в рантайме.

Но есть зазор: что мешает написать Force Bool или Input Int? Ничего. Параметр unit принимает любой тип kind-а Type, метки у нас никак не перечислены. Фантомам не хватает собственного kind-а. Хочется сказать компилятору: вот ровно две единицы измерения, вот ровно два статуса, всё остальное мусор. Для этого придётся сначала научиться доказательствам, а потом переселить значения в типы.

GADTs: конструктор приносит доказательство

Вспомни интерпретатор lishp. Его eval возвращал Either LispError Value, и заметная часть ошибок была типовая: сложили число со строкой, в if попало не булево. Мы ловили их в рантайме, потому что AST был нетипизированный: Value это один большой ADT, и Add мог держать что угодно. Построим теперь язык, в котором кривое выражение нельзя даже сконструировать:

{-# LANGUAGE GADTs #-}

data Expr a where
  IntE  :: Int  -> Expr Int
  BoolE :: Bool -> Expr Bool
  Add   :: Expr Int  -> Expr Int -> Expr Int
  If    :: Expr Bool -> Expr a   -> Expr a -> Expr a

Это GADT, обобщённый алгебраический тип данных. Синтаксис непривычный: каждый конструктор записан своей полной сигнатурой, как функция. И в этом вся суть: обычный ADT обязан возвращать ровно Expr a, а GADT-конструктору разрешено уточнить параметр. IntE строит именно Expr Int, BoolE именно Expr Bool, а Add требует два Expr Int и никаких других.

Кривые термы умерли на этапе компиляции:

ok :: Expr Int
ok = Add (IntE 1) (If (BoolE True) (IntE 2) (IntE 3))

-- bad = Add (IntE 1) (BoolE True)
-- error: Couldn't match type Bool with Int
--        Expected: Expr Int, Actual: Expr Bool

А теперь интерпретатор, ради которого всё затевалось:

eval :: Expr a -> a
eval (IntE n)   = n
eval (BoolE b)  = b
eval (Add l r)  = eval l + eval r
eval (If c t e) = if eval c then eval t else eval e

Прочитай сигнатуру ещё раз: Expr a -> a. Не Either LispError a, не Maybe a. Тотальная функция без единой ошибки. Как компилятор вообще это принимает? В ветке IntE n мы возвращаем n :: Int, хотя обещали a. Хитрость в том, что матч на GADT-конструктор приносит компилятору доказательство: раз значение построено через IntE, значит a это Int, уравнение a ~ Int действует внутри ветки. Сравни с защитниками типов из TS: x is string сужает тип значения, а GADT-матч уточняет переменную типа в сигнатуре. Вот этого в TS нет совсем: размеченное объединение не докажет компилятору ничего про дженерик-параметр функции.

Раз конструктор волен не упоминать переменную в результате, её можно и спрятать. Это второй подарок синтаксиса GADT, экзистенциальные типы:

data Loggable where
  MkLoggable :: Show a => a -> Loggable

batch :: [Loggable]
batch = [MkLoggable 42, MkLoggable "deploy", MkLoggable (Just True)]

flush :: [Loggable] -> IO ()
flush = mapM_ (\(MkLoggable x) -> print x)

Список с виду гетерогенный, но честный: про каждый элемент известно ровно одно, у него есть Show. В экосистеме GADTs на каждом шагу. AST самого GHC растёт по стадиям через них (приём trees that grow из урока про устройство GHC). Free и Freer монады, к которым идём в следующем уроке, это GADT, где конструктор запоминает эффект вместе с типом продолжения. И typed AST в духе нашего Expr живёт в каждом серьёзном eDSL, от SQL-билдеров до аппаратных описаний.

DataKinds: значения переезжают в типы

Возвращаемся к зазору из раздела про фантомы: метки Raw и Sanitized ничем не перечислены, Input Int компилируется. Решение звучит дерзко: давай продвинем обычный ADT на этаж выше.

{-# LANGUAGE DataKinds, KindSignatures #-}

data Status = Draft | Published

newtype Post (s :: Status) = Post { body :: Text }

publish :: Post 'Draft -> Post 'Published
publish (Post b) = Post b

DataKinds берёт объявление data Status = Draft | Published и удваивает его. Внизу всё как раньше: тип Status, значения Draft и Published. Но теперь Status это ещё и kind, а 'Draft и 'Published это типы этого kind-а. Апостроф напоминает: это продвинутый конструктор, а не тип. Значений у 'Draft нет и не будет, это чистая метка. Зато аннотация (s :: Status) теперь заставляет kind-чекер охранять фантом: Post Int отлетает с ошибкой Expected kind Status, but Int has kind Type. Перебор стал невозможен по построению, ровно как мы любим со времён урока про моделирование домена.

Вместе с DataKinds GHC даёт три встроенных kind-а из GHC.TypeLits, и вот они уже совсем взрослые:

• Symbol, строки в типах: "users" :: Symbol;
• Nat, натуральные числа в типах: 42 :: Nat, с типовой арифметикой +, *, <=;
• списки и кортежи типов: '[Int, Bool] :: [Type], помнишь кортежи-списки из TS-урока? Вот их близнец.

Symbol даёт убийственно простой паттерн для денег:

newtype Money (currency :: Symbol) = Money Rational

add :: Money c -> Money c -> Money c
add (Money a) (Money b) = Money (a + b)

price :: Money "USD"
price = Money 99

fee :: Money "EUR"
fee = Money 5

-- add price fee
-- error: Couldn't match type "EUR" with "USD"

Валюта не хранится ни в одном байте, не сериализуется, не сравнивается в рантайме. Она существует только для компилятора, и этого достаточно, чтобы доллары с евро не складывались. А теперь соединим DataKinds с GADT и получим самый знаменитый пример type-level Haskell, вектор со статически известной длиной:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Nat = Z | S Nat   -- продвигается: kind Nat, типы 'Z и 'S n

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

vhead :: Vec ('S n) a -> a
vhead (VCons x _) = x

vhead принимает только вектор длины хотя бы один: Vec 'Z a не матчится с Vec ('S n) a, и вызов vhead VNil отлетает на компиляции. Сравни с head [] из урока про списки, который падает в рантайме: класс ошибок целиком вымер. Заметь и чего в vhead нет: ветки для VNil. Компилятор сам видит, что она невозможна, и не требует её.

Числа в типах хочется обратно в рантайм: напечатать маршрут, выделить буфер. Мост в обратную сторону строят классы KnownSymbol и KnownNat:

ghci> :set -XDataKinds -XTypeApplications
ghci> import GHC.TypeLits
ghci> import Data.Proxy
ghci> symbolVal (Proxy @"users")
"users"
ghci> natVal (Proxy @42)
42

Proxy здесь это просто способ ткнуть пальцем в тип: значение у него одно и бессодержательное, весь смысл в параметре. А symbolVal достаёт строку из словаря класса KnownSymbol, того же механизма словарей, что мы разобрали в уроке про тайпклассы. Запомни эту пару, через двадцать минут она будет печатать маршруты нашего роутера.

В TS, кстати, весь этот раздел не нужен: там литералы и так живут в типах, 'hello' и 42 сразу типы. Расплата известна: у TS нет kind-этажа, и проверять сами типовые выражения нечем. Haskell платит синтаксисом за продвижение, но получает типизированный type-level.