четверг, 19 января 2012 г.

[prog] Пояснение/дополнение к предыдущему посту

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

Итак, в одном из примеров автор статьи хотел показать способность системы типов вылавливать баги:

let rec destutter l = 
  match l with 
  | []             -> [] 
  | x :: y :: rest -> 
    if  x = y then destutter (y :: rest) 
    else  x :: destutter (y :: rest) 

Эта функция не обрабатывает вариант, когда в исходном списке l всего один элемент. И эту ошибку обнаруживает компилятор, подсказывая программисту, что остался необработанным вариант _::[], которого не было в паттерн-матчинге.

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

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

Нет, не дает. Поскольку мы могли ошибиться где-то в ветвях паттерн-матчинга. Например, вместо if x = y написали бы if x <> y. Или же в ветви else вместо x::destutter(y::rest) указали бы destutter(y::rest). Ведь такого рода ошибки система типов не контролирует.

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

Т.е. выловленная компилятором ошибка, на мой взгляд, вовсе не уменьшило количество тестов, которые должен был бы написать разработчик. Именно поэтому помощь со стороны системы типов в данном месте – это счастливый случай, на который не приходится рассчитывать в будущем. А, посему, нет разницы, перестаем ли мы надеяться на счастливые случаи в Python-е или же в OCaml-е.

Я убежден, что системы типов (т.е. то, что ставится во главу угла евангелистами от функциональщины) должны уменьшать количество проверок, которые должен делать программист. Не суть важно, в unit-тестах или же в виде assert-ов или if-ов в основном коде программы.

Взять в качестве примера самый простой void safety (т.е. отсутствие обращения к нулевому указателю). В C/C++ и Java можно передать в функцию аргумент по указателю (в Java по ссылке) и этот аргумент запросто может оказаться нулевым. Даже если в комментариях к функции сто раз будет написано, что ноль туда передавать нельзя. И разработчику такой функции, если он не хочет допустить краха приложения, придется вставлять проверку на равенство аргумента нулю. Эта так самая лишняя проверка, лишняя работа и еще один шанс допустить ошибку в программе, от которой действительно избавляет разработчика система типов.

Ведь если язык поддерживает понятие nullable и non-nullable ссылок (в Eiffel они называются attached и detachable), то тогда разработчик функции может явно указать, что аргумент функции не может быть нулевым. И компилятор ему это будет гарантировать! Следовательно, разработчик будет освобожден от написания лишних проверок и тестов, поскольку это уже не нужно.

Вот если бы автор критикуемой мной статьи привел пример такого рода помощи со стороны системы типов, я бы тогда не стал говорить об отсутствии разницы между программированием на Python-е и OCaml-е.

14 комментариев:

  1. я понял разницу

    однако я считаю полезным в языке не только явные гарантии, но и подталкивание программиста к правильному поведению -- в данном случае, к разбору вариантов; при этом полнота разбора вариантов зачастую именно *гарантируется* компилятором

    ОтветитьУдалить
  2. и то, что помощь компилятора значительно обесценивается, если она не гарантирована в четких и ясных для понимания пределах -- это да

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

    ОтветитьУдалить
  4. хотя, возвращаясь к этому примеру, тут все же гарантия есть

    допустим, нам надо выкинуть не пары, а все подряд идущие равные элементы, оставив 1

    мы пишем функцию

    f( [] ) = []
    f( [x] ) = [x]
    f( x : yy ) = x : f(drop_all_equal x yy)

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

    но честно скажу -- я не знаю, какие тесты можно *не писать* к этой функции, поскольку "компилятор гарантирует"

    ОтветитьУдалить
    Ответы
    1. допустим, нам надо выкинуть не пары, а все подряд идущие равные элементы, оставив 1

      Примеры выше это самое и делают.

      Удалить
  5. ну или так:

    f( [] ) = []
    f( [x] ) = [x]
    f( x : yy ) = x : f(yy `minus_heading_seq_of` x)

    ОтветитьУдалить
  6. а вот уу `minus_heading_seq_of` х по-моему нагляднее задавать императивно "пока можно откусить х от уу, делай это!", а не разбором вариантов

    ОтветитьУдалить
    Ответы
    1. По моему разбор наглядней, особенно если переписать вариант на окамл вот так:

      let rec destutter = function
      | [] -> []
      | x :: [] -> x :: []
      | x :: y :: rest when x = y -> destutter (y :: rest)
      | x :: rest -> x :: destutter rest

      практически декларативное описание алгоритма.

      Удалить
    2. Даже проще, строка из-за которой сыр бор тут вообще лишняя:

      let rec destutter = function
      | [] -> []
      | x :: y :: rest when x = y -> destutter (y :: rest)
      | x :: rest -> x :: destutter rest

      последняя строка нормально отработает и для одноэлементного списка.
      В общем подтверждение моего эмпирического правила, стараться не использовать 'if' заменять его паттерн матчингом.

      Удалить
    3. @Rustam:

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

      let rec destutter = function
      | [] -> []
      | x :: [] -> x :: []
      | x :: x :: rest -> destutter (x :: rest)
      | x :: rest -> x :: destutter rest

      ?

      Удалить
    4. Не, такое не пройдет, это будет как попытка назначить x два разных значения.

      Удалить
  7. @Евгений
    Я убежден, что системы типов (т.е. то, что ставится во главу угла евангелистами от функциональщины)

    Erlang, Scheme, Pure :)

    ОтветитьУдалить
    Ответы
    1. Да ладно, чой-то я не помню, чтобы евангелисты Erlang-ом размахивали ;) Erlang уже давно обычная рабочая лошадка (что-то вроде RoR, но в другой нише) на которой тихо и спокойно работают.

      А вот Scheme -- это вотчина других евангелистов, уже от Lisp-а всемогущего :)))

      Удалить
    2. Ну Scheme это как раз отход от императивного лиспа в сторону функциональщины :)
      А эрланг да уже как-то исчезает из флеймов.

      Удалить