LiquidHaskell

Ну что, пора пустить жиденького — как в «Терминаторе 2», где появляется робот из жидкого металла. Тип $\mathtt{Int}$ гарантирует форму, но молчит о содержании: что число не ноль, что список не пуст, что индекс в границах. LiquidHaskell навешивает на обычные типы Haskell логические предикаты — уточняющие типы (refinement types) — и проверяет их при компиляции SMT-решателем (Z3). Аннотации-«декораторы» живут в специальных комментариях $\mathtt{\{\text{-}@\;\ldots\;@\text{-}\}}$, поэтому код остаётся обычным Haskell и собирается обычным GHC. Синтаксис декораторов:

— «значения типа $\tau$, для которых верен предикат $p$». Базовый пример — деление, которое невозможно вызвать с нулём:

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ safeDiv :: Int -> NonZero -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y

ok  = safeDiv 10 2    -- проходит: что 2 /= 0, решатель видит сам
bad = safeDiv 10 0    -- ошибка компиляции: 0 не влезает в NonZero

Под капотом это подтипирование — сравнение двух уточнённых типов, у каждого свой предикат: $p$ у аргумента, $q$ у параметра. Тип $\{\, v:\tau \mid p \,\}$ — подтип $\{\, v:\tau \mid q \,\}$, когда любое значение, удовлетворяющее $p$, удовлетворяет и $q$, — эту импликацию и проверяет SMT-решатель. Для вызова $\mathtt{safeDiv}\;10\;2$ у аргумента $p$ $\equiv (v = 2)$ — синглтонный тип литерала, у параметра $\mathtt{NonZero}$ — $q$ $\equiv (v \neq 0)$, импликация $v$ $= 2$ $\Rightarrow v$ $\neq 0$ верна:

Предикатам доступны меры (measures) — простые функции над данными, которые LiquidHaskell умеет разворачивать в логике. Классика — $\mathtt{head}$, который перестаёт быть частичным:

{-@ measure len @-}
len :: [a] -> Int
len []     = 0
len (_:xs) = 1 + len xs

{-@ head' :: {v:[a] | len v > 0} -> a @-}
head' :: [a] -> a
head' (x:_) = x    -- ветка [] не нужна: она невозможна по типу

Рекурсию LiquidHaskell проверяет на завершимость — ищет убывающую метрику (по умолчанию — первый числовой аргумент). Тип $\mathtt{Nat}$ в сигнатуре — встроенный в LiquidHaskell алиас $\{\, v:\mathtt{Int} \mid v$ $\geq 0 \,\}$, объявленный так же, как наш $\mathtt{NonZero}$. Факториал из раздела про Y-комбинатор здесь тотален:

{-@ fac :: Nat -> Nat @-}
fac :: Int -> Int
fac 0 = 1
fac n = n * fac (n - 1)   -- n убывает и не уходит ниже нуля — решатель доволен

В режиме рефлексии на декораторах доказывают настоящие теоремы: свойство записывается типом, доказательство — программой. Это соответствие Карри — Ховарда:

{-@ LIQUID "--reflection" @-}
import Language.Haskell.Liquid.ProofCombinators

{-@ reflect double @-}
double :: Int -> Int
double x = x + x

{-@ doubleIsTwice :: x:Int -> { double x == 2 * x } @-}
doubleIsTwice :: Int -> Proof
doubleIsTwice x = double x === x + x === 2 * x *** QED

Это шаг в сторону типов, зависящих от термов, но не полноценные зависимые типы, как в Agda: предикаты ограничены разрешимыми теориями SMT (линейная арифметика, равенство, множества), зато всё проверяется автоматически, без ручных доказательств.