В функциональном программировании, как можно достичь модульности через математические законы?

Я прочитал в этом вопросе, что функциональные программисты склонны использовать математические доказательства, чтобы гарантировать, что их программа работает правильно. Это звучит намного проще и быстрее, чем модульное тестирование, но, исходя из опыта OOP / Unit Testing, я никогда не видел, чтобы это было сделано.

Можете ли вы объяснить это мне и привести пример?

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

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

datatype tree = Empty | Node of (tree * int * tree)

Это вводит новый тип с именем tree, значения которого могут входить ровно в две разновидности (или классы, которые не следует путать с концепцией ООП класса) - Emptyзначение, которое не несет никакой информации, и Nodeзначения, которые содержат 3-кортеж, первый и последний элементы trees и средний элемент которых является int. Ближайшее приближение к этому объявлению в ООП будет выглядеть так:

public class Tree {
    private Tree() {} // Prevent external subclassing

    public static final class Empty extends Tree {}

    public static final class Node extends Tree {
        public final Tree leftChild;
        public final int value;
        public final Tree rightChild;

        public Node(Tree leftChild, int value, Tree rightChild) {
            this.leftChild = leftChild;
            this.value = value;
            this.rightChild = rightChild;
        }
    }
}

С оговоркой, что переменные типа Tree никогда не могут быть null.

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

fun height(Empty) =
        0
 |  height(Node (leftChild, value, rightChild)) =
        1 + max( height(leftChild), height(rightChild) )

Мы определили heightфункцию по кейсам - есть одно определение для Emptyдеревьев и одно определение для Nodeдеревьев. Компилятор знает, сколько классов деревьев существует, и выдает предупреждение, если вы не определили оба случая. Выражение Node (leftChild, value, rightChild)в сигнатуре функции связывает значения 3-кортежа переменных leftChild, valueи , rightChildсоответственно , таким образом , мы можем обратиться к ним в определении функции. Это похоже на объявление локальных переменных, таких как это на языке ООП:

Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();

Как мы можем доказать, что мы реализовали heightправильно? Мы можем использовать структурную индукцию , которая состоит из: 1. Доказать, что heightэто правильно в базовом случае (ах) нашего treeтипа ( Empty) 2. Предполагая, что рекурсивные вызовы heightверны, доказать, что heightэто верно для неосновного (и) случая (ов) ) (когда дерево на самом деле Node).

На шаге 1 мы видим, что функция всегда возвращает 0, когда аргумент является Emptyдеревом. Это правильно по определению высоты дерева.

Для шага 2 функция возвращается 1 + max( height(leftChild), height(rightChild) ). Предполагая, что рекурсивные вызовы действительно возвращают рост дочерних элементов, мы видим, что это также правильно.

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

РЕДАКТИРОВАТЬ: Так как этот ответ поднялся до вершины, я хотел бы добавить менее тривиальный пример доказательства и немного подробнее рассмотреть структурную индукцию. Выше мы доказали, что если heightвозвращает , его возвращаемое значение является правильным. Мы не доказали, что оно всегда возвращает значение. Мы также можем использовать структурную индукцию, чтобы доказать это (или любое другое свойство). Опять же, на шаге 2 мы можем предположить, что свойства являются рекурсивными вызовами, если все рекурсивные вызовы работают с прямым потомком объекта. дерево.

Функция может не вернуть значение в двух ситуациях: если она выдает исключение, и если она зацикливается вечно. Сначала давайте докажем, что если не сгенерировано никаких исключений, функция завершается:

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

2. Докажите, что функция заканчивается в неосновных случаях ( Node). Там три вызовов функций здесь: +, maxи height. Мы знаем это +и maxзаканчиваем, потому что они являются частью стандартной библиотеки языка, и они определены таким образом. Как упоминалось ранее, мы можем предположить, что свойство, которое мы пытаемся доказать, является истинным для рекурсивных вызовов, если они работают с непосредственными поддеревьями, поэтому вызовы также должны heightзавершаться.

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

1. Докажите, что heightне генерирует исключения в базовом случае ( Empty). Возвращение 0 не может выдать исключение, поэтому мы закончили.
2. Докажите, что heightне вызывает исключение в неосновном случае ( Node). Предположим еще раз, что мы знаем +и maxне бросаем исключения. И структурная индукция позволяет нам предполагать, что рекурсивные вызовы также не будут генерироваться (потому что работают с непосредственными дочерними элементами дерева.) Но подождите! Эта функция является рекурсивной, но не хвостовой . Мы могли бы взорвать стек! Наше попытанное доказательство обнаружило ошибку. Мы можем исправить это, изменив heightхвостовую рекурсию .

Я надеюсь, что это показывает, что доказательства не должны быть страшными или сложными. Фактически, всякий раз, когда вы пишете код, вы неофициально создаете доказательство в своей голове (в противном случае вы не будете уверены, что просто реализовали функцию.) Избегая нулевого значения, ненужных мутаций и неограниченного наследования, вы можете доказать, что ваша интуиция исправить довольно легко. Эти ограничения не так суровы, как вы думаете:

• null это языковой недостаток, и избавиться от него безусловно хорошо.
• Мутация иногда неизбежна и необходима, но она нужна гораздо реже, чем вы думаете, особенно если у вас есть постоянные структуры данных.
• Что касается конечного числа классов (в функциональном смысле) / подклассов (в смысле ООП) по сравнению с их неограниченным количеством, то это слишком большой вопрос для одного ответа . Достаточно сказать, что здесь есть компромисс между дизайном - доказуемость правильности и гибкость расширения.

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

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

2. Некоторые функциональные языки (особенно из семейства ML) имеют чрезвычайно выразительные системы типов, которые могут дать гораздо более полные гарантии того, что система типов в стиле C (но некоторые идеи, такие как дженерики, также стали распространенными в основных языках). Когда программа проходит проверку типа, это своего рода автоматическое доказательство. В некоторых случаях это позволит обнаружить некоторые ошибки (например, забыть базовый случай в рекурсии или забыть обработать определенные случаи в сопоставлении с образцом).

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

   Мне нравятся как очень либеральные, так и очень ограниченные языки, и у обоих есть свои трудности. Но дело не в том, что кто-то будет «лучше», а просто удобнее для разных задач.

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

• Тестирование накладывает верхнюю границу на правильность: если тест не пройден, программа неверна, если тесты не пройдены, мы уверены, что программа обработает проверенные случаи, но все равно могут быть обнаруженные ошибки.

  int factorial(int n) {
    if (n <= 1) return 1;
    if (n == 2) return 2;
    if (n == 3) return 6;
    return -1;
  }
  
  assert(factorial(0) == 1);
  assert(factorial(1) == 1);
  assert(factorial(3) == 6);
  // oops, we forgot to test that it handles n > 3…
  

• Доказательства устанавливают нижнюю границу правильности: может оказаться невозможным доказать определенные свойства. Например, может быть легко доказать, что функция всегда возвращает число (это то, что делают системы типов). Но может быть невозможно доказать, что число всегда будет < 10.

  int factorial(int n) {
    return n;  // FIXME this is just a placeholder to make it compile
  }
  
  // type system says this will be OK…
  

Слово предупреждения может быть в порядке здесь:

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

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

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

Вот пример из реализации дерева AVL:

--- A generator for arbitrary Trees with integer keys and string values
aTree = arbitrary :: Gen (Tree Int String)


--- After insertion, a lookup with the same key yields the inserted value        
p_insert = forAll aTree (\t -> 
             forAll arbitrary (\k ->
               forAll arbitrary (\v ->
                lookup (insert t k v) k == Just v)))

--- After deletion of a key, lookup results in Nothing
p_delete = forAll aTree (\t ->
            not (null t) ==> forAll (elements (keys t)) (\k ->
                lookup (delete t k) k == Nothing))

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

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

p_delete_nonexistant = forAll aTree (\t ->
                          forAll arbitrary (\k -> 
                              k `notElem` keys t ==> delete t k == t))

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

Я не совсем понимаю, что означает связанный ответ «достичь модульности с помощью математических законов», но я думаю, что у меня есть представление о том, что имеется в виду.

Проверьте Функтор :

Класс Functor определяется следующим образом:

 class Functor f where
   fmap :: (a -> b) -> f a -> f b

Это не тестовые случаи, а пара законов, которые должны быть выполнены.

Все экземпляры Functor должны подчиняться:

 fmap id = id
 fmap (p . q) = (fmap p) . (fmap q)

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

instance  Functor Maybe  where
    fmap _ Nothing       = Nothing
    fmap f (Just a)      = Just (f a)

Проблема состоит в том, чтобы убедиться, что ваша реализация удовлетворяет законам. Как ты это делаешь?

Один подход заключается в написании тестовых случаев. Основное ограничение этого подхода состоит в том, что вы проверяете поведение в конечном количестве случаев (удачи, исчерпывающе тестируете функцию с 8 параметрами!), И поэтому прохождение тестов не может гарантировать ничего, кроме того, что тесты пройдены.

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

Я не могу провести вас через фактическое формальное доказательство того, что приведенный выше Functorпример удовлетворяет законам, но я постараюсь дать общее представление о том, как это доказательство может выглядеть:

1. fmap id = id
   • если мы имеем Nothing
     • fmap id Nothing= Nothingпо части 1 реализации
     • id Nothing= Nothingпо определениюid
   • если мы имеем Just x
     • fmap id (Just x)= Just (id x)= Just xпо части 2 реализации, затем по определениюid
2. fmap (p . q) = (fmap p) . (fmap q)
   • если мы имеем Nothing
     • fmap (p . q) Nothing= Nothingпо части 1
     • (fmap p) . (fmap q) $ Nothing= (fmap p) $ Nothing= Nothingдвумя приложениями части 1
   • если мы имеем Just x
     • fmap (p . q) (Just x)= Just ((p . q) x)= Just (p (q x))по части 2, то по определению.
     • (fmap p) . (fmap q) $ (Just x)= (fmap p) $ (Just (q x))= Just (p (q x))двумя приложениями части второй

«Остерегайтесь ошибок в приведенном выше коде; я только доказал, что это правильно, а не пробовал». - Дональд Кнут

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

В идеальном мире компьютерные ученые и математики также совершенны и тоже не делают ошибок.

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