Тесты или типы

Привет. На днях я искал, как сделать что-то в Idris, и наткнулся на неплохой пост, вольный перевод которого выглядит вполне уместным. Вольности и отсебятину, где необходимо, я буду обозначать ⟦вот такими закорючками в начале и в конце⟧.

Когда стоит использовать тесты, а когда — типы? Какую информацию и какие гарантии мы получаем в обмен на наши усилия по их написанию?

Мы рассмотрим простой и немного надуманный пример, выраженный на Python, C, Haskell и Idris. Мы также увидим, что можно сказать о реализации без каких-либо дополнительных знаний о ней, в каждом из случаев.

Мы не будем учитывать разнообразные чёрные ходы, позволяющие явно нарушать гарантии языка (например, расширения C, unsafePerformIO в Haskell, небезопасные приведения типов), иначе нельзя было бы сделать вообще никаких выводов, и этот пост получился бы довольно коротким. ⟦Кроме того, у того же хаскеля есть подмножество Safe Haskell, явно и транзитивно запрещающее использование этих и ряда других трюков, могущих нарушить целостность языка.⟧

Спецификация

Пусть дан список и некоторое значение. Необходимо вернуть индекс этого значения в списке или указать, что этого значения в списке нет.

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

Python

def x(y, z):
    # 10000 строк нечитаемого кода

Заметим сразу, что нам неинтересны непроверяемые ⟦и не влияющие на семантику⟧ свойства программы вроде именования переменных и текстовой документации, так что я намеренно не писал помогающий восприятию код. Нам интересно лишь то, что, при условии проходящих тестов и проверок типов, не может быть неправдой.

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

Анализ

Мало того, что без тестов и без типов получается хрупкий код, но и наша единственная возможность понять, что делает функция — документация. А так как документация проверяется людьми, а не машинами, она легко может оказаться устаревшей ⟦или изначально неверной⟧.

• Документация
  • ✗ Мы знаем ожидаемое поведение
    У нас нет ничего, что говорило бы нам о поведении этой функции. Ты ненавидишь свою бабушку. Ты монстр.
• Гарантии
  • ✓ Безопасность памяти
    Python — язык со сборкой мусора, снимающий с нас эту заботу. ⟦Впрочем, насколько я знаю, ничего не мешает внутри этой функции дёргать небезопасные библиотеки или C FFI.⟧

Python с тестами

def test_happy_path():
    assert x([1, 2, 3], 2) == 1

def test_missing():
    assert x([1, 2, 3], 4) is None

Теперь-то мы знаем, что наша функция работает, и в случае отсутствующего элемента результат — None?

Ну… Нет. Это всего лишь один пример. К сожалению, область определения нашей функции бесконечная, и никакое количество примеров не может являться доказательством корректной работы нашей функции. Больше тестов — больше уверенности, но никакое количество тестов не разрешит все сомнения.

Возможность того, что эта функция вернёт None для 4, но не для 5, звучит довольно бредово, и в этом конкретном случае это, скорее всего, и есть бред. Мы можем удовлетвориться нашим уровнем веры и остановиться на каком-то количестве примеров. Но, опять же, тогда пост получится коротким, так что давайте представим, что реализация не такая очевидная.

Так как тесты не могут доказать что-то в общем случае, а лишь показывают поведение на конкретных примерах, то тесты не могут показать отсутствие ошибок. Например, нет такого теста, который бы показал, что наша функция никогда не бросает исключение или никогда не входит в вечный цикл, или не содержит невалидных ссылок. Такое может только статический анализ.

Однако пусть даже примеры не очень хороши в роли доказательства, но они хотя бы составляют неплохую документацию. Из этих двух примеров мы можем вывести полную спецификацию ⟦при некоторых дополнительных априорных предположениях — те два примера также удовлетворяют, например, «контрспеке» «найти элемент в массиве и вернуть предыдущий, если он есть», на придумывание которой у меня ушло секунд десять⟧.

Анализ

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

• Документация
  • ✓ У нас есть пример использования
  • ✓ Мы знаем некоторые классы значений, которые будут корректно обработаны
  • ✗ Мы знаем все типы значений, которые будут корректно обработаны
    У нас нет ограничений на типы аргументов, так что, несмотря на наличие примеров того, что функция может обработать, мы не знаем, какие типы не были протестированы.
  • ✗ Мы знаем ожидаемое поведение
    ⟦Автор оригинальной статьи поставил здесь галочку, я же позволю себе поставить крестик, учитывая комментарий выше⟧
• Спецификация
  • ✓ Работает хотя бы в одном случае
  • ✗ Возвращённый индекс всегда является корректным индексом
  • ✗ Возвращённый индекс всегда указывает на подходящее значение
  • ✗ Отсутствующий элемент всегда возвращает None/Nothing
• Частые ошибки
  • ✗ Нет опечаток или некорректных имён
    Статический анализ может помочь, но, так как Python — динамический язык с возможностью переопределения разных вещей во время выполнения, мы никогда не может доказать отсутствие ошибок.
    В частности, может быть очень сложно или невозможно определить, является ли имя метода корректным, так как валидность вызова метода зависит от рантайм-типа объекта, на котором происходит вызов.
  • ✗ Нет неожиданного null
  • ✗ Ошибочный случай всегда обрабатывается
    В моём опыте это один из наиболее частых источников ошибок: в нашем примере функция возвращает None в случае отсутствующего элемента, но использующий эту функцию код может предположить, например, что она всегда будет возвращать число. Кроме того, это также может привести и к необработанному исключению.
• Гарантии
  • ✓ Безопасность памяти
  • ✗ Функция не может быть вызвана с неподходящим типом
  • ✗ Нет побочных эффектов
  • ✗ Нет исключений
  • ✗ Нет ошибок
  • ✗ Нет вечных циклов

Haskell

x y z = -- 10000 нечитаемых символов

Если вы незнакомы с синтаксисом: это определение функции x с параметрами y и z. В Haskell можно не указывать типы, так как они будут выведены из реализации ⟦если, конечно же, не используются различные продвинутые фишки из современных расширений системы типов⟧.

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

Анализ

Очевидно, мы можем десь сделать не так много выводов, но вот что стоит подметить:

• Документация
  • ✗ Мы знаем ожидаемое поведение
• Частые ошибки
  • ✓ Нет опечаток или некорректных имён
    Так как Haskell — компилируемый язык, все имена должны быть разрешены на этапе компиляции. Программа просто не соберётся при наличии этой ошибки.
  • ✓ Нет неожиданного null
    В Haskell просто нет null. Проблема решена!
• Гарантии
  • ✓ Безопасность памяти
  • ✓ Функция не может быть вызвана с неподходящим типом
  • ✓ Нет неожиданных побочных эффектов
    ⟦Автор оригинальной статьи не указал этот пункт, я же позволю себе заметить, что при наличии побочных эффектов выведенный тип этой функции будет указывать на их наличие, так что вызывающий код будет знать об их возможности.⟧

Haskell с указанием типов

x :: Eq a => [a] -> a -> Maybe Int
x y z = -- ...

Ранее мы говорили о достаточно попустительском отношении к безопасности бабушек: из тестов было понятно, что функция не собирается приносить никому вреда, но действительно ли бабушка в безопасности? Точно ли эта функция не посылает никаких матерных писем?

Haskell известен тем, что это чистый функциональный язык. Это не значит, что код не может иметь сайд-эффектов, но все сайд-эффекты должны присутствовать в типе. Мы знаем тип этой функции, мы видим, что он чистый, так что мы уверены, что эта функция не модифицирует никакого внешнего состояния.

Это очень интересное свойство и по другим причинам: так как мы знаем, что нет никаких сайд-эффектов, мы можем понять, что эта функция делает, основываясь только лишь на её сигнатуре! Достаточно поискать по этой сигнатуре на Hoogle и посмотреть на первый результат. Конечно, это не единственная возможная функция, которая бы имела такой тип, но тип даёт нам достаточно уверенности для целей документации.

Анализ

• Документация
  • ✓ Мы знаем ожидаемое поведение
  • ✗ У нас есть пример использования
  • ✓ Мы знаем некоторые классы значений, которые будут корректно обработаны
  • ✓ Мы знаем все типы значений, которые будут корректно обработаны
• Спецификация
  • ✗ Работает хотя бы в одном случае.
    При отсутствующих тестах или доказательствах мы не знаем, работает ли вообще наша функция так, как мы ожидаем!
  • ✗ Возвращённый индекс всегда является корректным индексом.
  • ✗ Возвращённый индекс всегда указывает на подходящее значение.
  • ✗ Отсутствующий элемент всегда возвращает None/Nothing.
• Частые ошибки
  • ✓ Нет опечаток или некорректных имён
  • ✓ Нет неожиданного null
  • ✓ Ошибочный случай всегда обрабатывается
    Если наша функция возвращает Nothing, то система типов позволяет убедиться, что этот случай корректно обрабатывается вызывающим кодом. Конечно, можно проигнорировать этот случай, но это необходимо сделать явно.
• Гарантии
  • ✓ Безопасность памяти
  • ✓ Функция не может быть вызвана с неподходящим типом
  • ✓ Нет побочных эффектов
  • ✗ Нет исключений
    Я разделяю исключения и ошибки, считая, что после исключений можно восстановиться, а после ошибок (например, частично определённых функций) — нет.
    По большей части исключения описываются в типах (например, в монаде IO). По-хорошему мы должны знать, что функция не бросит исключение, только лишь на базе её типа. Однако Haskell ломает это ожидание, разрешая бросать исключения из чистого кода.
    ⟦Кроме того, стоит отметить, что в Haskell ошибки вроде некорректного вызова частично определённых функций тоже представляются как исключения, которые можно отловить и обработать, так что различие между этими двумя категориями чуть менее очевидно.⟧
  • ✗ Нет ошибок
    Мы всё ещё можем использовать частично определённые функции, например, деление на ноль.
  • ✗ Нет вечных циклов

Haskell с тестами

Помните, ранее я сказал, что тесты не могут доказать отсутствие ошибок? Я соврал. Когда звёзды правильно сходятся, и если тесты совместить с типами, то это становится возможным! Первой звездой является конечность области определения нашей функции. Вторая — область определения должна быть не только конечной, но и не сильно большой, иначе подобный тест будет трудно реализовать на практике.

Например:

not :: Bool -> Bool
not x = ...

На входе может быть либо True, либо False. Достаточно протестировать эти два варианта, и вот он, Святой Грааль! Никаких исключений, вечных циклов, некорректных результатов, никаких ошибок. ⟦Впрочем, для чуть более сложной функции может быть непонятно, сколько времени отвести на тесты: если они долго выполняются, то попали ли мы в вечный цикл, или она просто тяжёлая? Проблема останова, чтоб её.⟧

На самом деле это тоже не совсем так в случае Haskell: в каждом Haskell-типе есть ещё и значение ⊥ (которое можно получить как undefined, error или в каком-то смысле как бесконечную рекурсию), но хаскелисты традиционно закрывают глаза и считают, что его не существует.

Внеклассное чтение: There are Only Four Billion Floats–So Test Them All!

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

Анализ
В этом случае тесты дополняют типы и затыкают некоторые дырки в системе типов Haskell. У нас гораздо больше уверенности в нашем коде по сравнению с использованием одних только тестов или же одних только типов.

C

/* C не умеет в полиморфизм, поэтому мы используем int */
int x(int *y, size_t n, int z) {
    /* 10000 строк нечитаемого кода */
}

Мы рассматриваем C из интереса к более старым системам типов. В частности, в C типы нужны скорее не программисту, а компилятору, чтобы помочь ему генерировать более быстрый код.

В нашем примере мы не знаем, что функция вернёт, если элемент не найден. Нам придётся опираться на традиции или на документацию (например, в этом случае это может быть значение -1).

Мы также могли бы иcпользовать out-аргументы: так мы можем возвращать ошибку и сохранять в этот out-аргумент возвращаемое значение. Это чуть более выразительный вариант, но нам всё ещё придётся опираться на документацию, чтобы понять, какие параметры считываются, а какие — записываются. В обоих случаях тяжело понять поведение, глядя на типы.

/* Та же функция, но с out-параметром */
error_t x(int *y, size_t n, int z, size_t *w) {
    /* 10000 строк нечитаемого кода */
}

Анализ
Система типов сама по себе не даёт нам так уж много гарантий. Мы, конечно, получаем какую-то информацию из этих типов, но достаточно сравнить её со случаем Haskell.

Idris

x : Eq x => List x -> x -> Maybe Int
x y z = ...

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

%default total

x : Eq x => Vect n x -> x -> Maybe (Fin n)
x y z = ...

Этот тип может быть прочитан как «дай мне список размера n и какое-то значение, и я верну тебе либо число, меньшее n, либо Nothing». Это гарантирует, что функция возвращает индекс, заведомо не выходящий за границы.

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

Анализ

• Спецификация
  • ✗ Работает хотя бы в одном случае.
  • ✓ Возвращённый индекс всегда является корректным индексом
  • ✗ Возвращённый индекс всегда указывает на подходящее значение
  • ✗ Отсутствующий элемент всегда возвращает None/Nothing
• Гарантии
  • ✓ Безопасность памяти
  • ✓ Функция не может быть вызвана с неподходящим типом
  • ✓ Нет побочных эффектов
  • ✗ Нет исключений
  • ✓ Нет ошибок
  • ✓ Нет вечных циклов

Idris с тестами

Так как язык типов Idris так же выразителен, как язык его термов ⟦(вернее, его доказуемо тотальная часть)⟧, различие между тестом и типом размывается:

ex : x [1, 2, 3] 2 = Just 1
ex = Refl

Эта функция имеет довольно странный тип x [1, 2, 3] 2 = Just 1. Этот тип означает, что для успешной проверки типов тайпчекер должен доказать, что x [1, 2, 3] 2 структурно равно Just 1. ⟦В данном случае доказательство тривиально, так как тайпчекеру достаточно нормализовать термы по обе стороны от знака равенства, что выполнится за конечное время из-за тотальности всех используемых функций, и что приведёт к единственному результату за счёт Чёрча-Россера. После этого можно воспользоваться рефлексивностью равенства, что и означает Refl.⟧

По факту мы написали тест на уровне типов.

Idris с доказательствами

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

В частности, мы можем доказать свойства, ранее бывшие для нас недосягаемыми:

-- Мы должны изменить констрейнт с Eq на DecEq
x : DecEq a => Vect n a -> (y : a) -> Maybe (Fin n)
x y z = ...

-- Это не исполняемый код, а доказательство всех интересующих нас свойств `x`
findIndexOk : DecEq a => (y : Vect n a) -> (z : a) -> 
              case x y z of
                Just i => index i y = z
                Nothing => Not (Elem z y)
findIndexOk y z = ...

Тип findIndexOk можно читать как «для любого типа a такого, что для него существует алгоритмически разрешимое сравнение (DecEq), для любого вектора y элементов типа a любой длины n и любого значения z типа a: если x y z возвращает индекс i, то по этому индексу лежит z, а если же x y z возвращает Nothing, то такого элемента в векторе вообще нет».

⟦Интересно, что автор исходной статьи даёт тип, чуть более слабый, чем приведённый выше.⟧

Теперь у нас всё схвачено! Какие же есть недостатки? Ну, писать все эти доказательства может быть довольно сложно.

Сравнение

Мнение

По моему мнению, само по себе использование современной системы типов наиболее эффективно с точки зрения отношения получаемой информации и гарантий к затраченным усилиям. Если хочется писать достаточно надёжный код, то типы можно приправить тестами. В идеале — в стиле QuickCheck.

С зависимыми типами грань между тестами и типами становится менее очевидной. Если вы пишете софт для Boeing или для кардиостимуляторов, то может оказаться полезным писать доказательства.

Автор: 0xd34df00d

Источник