?

Log in

No account? Create an account

Об оптимальном языке программирования - БЭСМ-6

2015, Feb 19

20:49:00 - Об оптимальном языке программирования

Previous Entry Share Next Entry

Прочитал интересную серию статей Paul Callaghan в PragPub (https://pragprog.com/magazines, выпуски с 38 по 49, кроме 44, а существенная для этого текста часть — с 45-го), и сделал для себя некий существенный вывод, к которому эта серия — прекрасная иллюстрация. Оным выводом и хочу поделиться.

Раз мы говорим "оптимальный", то встают вопросы "по какому критерию?" и "при каких краевых условиях?" У меня пока не получается четко разделить. Краевым условие точно будет "достаточно надежная программа", а вот критерием оптимальности оказывается неочевидная комбинация из затрат времени и внимания на ее написание или модификацию (модификация через год-два — это важно) и степени моей уверенности в том, что программа достаточно надежна. Собственно, одна из умных мыслей, явно сформулированных Каллаганом — это как раз про степень уверенности.

Как нетрудно догадаться, даже краевое условие весьма размытое и для разных проектов различно, не говоря уже о критерии оптимальности. Я бы с удовольствием перевел степень уверенности в разряд краевых условий, чтобы измерять только время (для достижения заданной степени уверенности), тогда можно было бы померить, но... на практике время тоже лимитировано, и если за это время не удается достичь желаемой уверенности, полученная уверенность окажется ниже желаемой. Возможно, существенно ниже. Здравствуй, невроз.

Сразу озвучу совсем уж сухой остаток. На данный момент развитие средств программирования таково, что оптимум называется Haskell. Может быть, еще какие-то сходные языки, не уверен. Ключевые моменты: богатая система типов и статическая их проверка. Только вместе. Но. Более богатые, чем хаскель, средства (зависимые типы) пока оказываются намного ниже оптимума.

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

За четыре года работы на хаскеле над достаточно большой, сложной и довольно плохо поставленной задачей (несколько радикальных переосмыслений ситуации, несколько крупных рефакторингов кода) через компилятор успешно прорвалось меньше десятка ошибок, из которых только одна по своей природе отличалась от "перепутал знак в формуле или ветки в if". И эта одна не ловилась бы никакими тестами. Как черный ящик там все работало, только память текла. Не очень сильно причем. Может, на нее никто никогда бы не наступил, тренажеры все же регулярно обесточивают. Остальные моментально ловились ручным тестированием. Ни одного автоматизированного теста у программы нет. Ни одной ошибки, которую они могли бы поймать, а минимальное ручное тестирование не поймало, в процессе эксплуатации обнаружено не было. Даже ошибок вида "сложили градусы с радианами", применяя хаскель, вполне можно избежать. Причем не путем запрета, а путем автомагического преобразования. Пакет dimensional, кто понимает.

Параллельно мне пришлось делать сайт. Я выбрал в качестве движка Ruby on Rails. Ну, так получилось... Сайт вроде работает, и трогать его я боюсь. А поскольку он требует крупного рефакторинга (рефакторинг модели бизнес-процесса, для сайта это даже рефакторингом уже назвать нельзя, на уровне программы функциональность меняется), то сейчас я взялся переделывать его на хаскель (движок yesod), чтобы не бояться трогать. Рельсы, конечно, лучше развиты в плане готового, но без дикого количества тестов трогать такой продукт не стоит. Проверено, мин есть. А автоматизированное тестирование веб-сайта, особенно с жабоскриптами — сами понимаете...

Небо и земля. То есть дойти до хаскеля точно стоит.

А дальше? Опять же параллельно, один коллега, несколько разочаровавшись в хаскеле как в серебряной пуле, потыкался в Agda. И даже написал на ней программу. И она даже работает. Но тоже серебряной пули не нашел. Я тоже краем глаза глянул, но писать программы не пробовал. А вот Каллаган в своей статье попробовал... Теперь — иллюстрация.

Интересующая меня в этом тексте часть начинается с того, что он берет учебную задачу, весьма простую, но уже не вполне тривиальную. Дан текст в виде строки, надо его разбить на строки не больше заданной длины, понятно, забивая каждую строку по возможности до упора. Если какое-то слово оказывается длиннее, его надо порезать, а если влезает, то не надо.

Поскольку задача пришла несколько снаружи, из серии постов другого человека, большого специалиста по tests-driven development, то Каллаган начал с TDD-подхода. Получил код из 11 строк, который успешно проходил все 6 исходных тестов, но был коряв и содержал слегка замаскированную ошибку, которую он сам быстро поймал ручным тестированием и добавил седьмой тест. Впрочем, в этом коде он потом нашел еще одну ошибку.

Каллаган не заострял на этом внимания, а я заострю. Набор тестов, предложенных большим специалистом по TDD, оказался плохим сходу. Развивая наблюдение дальше, можно сделать вывод, что TDD, пока набор тестов вменяемого размера, дает очень плохую уверенность. Кто работал со мной в Криптокоме, тот помнит, какой у нас был объем тестов, дававший пристойную уверенность, и сколько времени занимал их прогон. Коллеги в Транзасе рассказывали, что когда они ввели в работу Smalltalk, поначалу у них, как положено, был набор автоматизированных тестов на основной код тренажера. Все равно недостаточный, но вскоре его прогон начал занимать столько времени, что все стали отключать запуск тестов. И уже много лет этот код не тестируется, на него дышать боятся, и тем не менее, периодически ломают. Починить сломанное обычно может ровно один человек в отделе. Остальные — в лучшем случае не сломать.

Окей, говорит Каллаган, что-то мне этот код самому тоже не нравится. Давайте попробуем функциональный подход к задаче, а тесты будем использовать для проверки, а не для драйва :) Функциональный подход он, кстати (это другая весьма интересная мысль) определил как подход "от данных". Помните "алгоритмы + структуры данных = программы", что считается краткой формулировкой процедурного подхода и отвергнуто объектно-ориентированными гражданами? Тут акцент смещен: структуры данных плюс их обработка.

Функциональный подход дал ему очень хороший результат, причем даже без введения типов, специфичных для задачи — вполне библиотечных строк и списков строк ему хватило. Получился код на 16 строк, если расписывать его экстремально развесисто, и на 9, если по-человечески, по которому за минуту его внимательного видно, что он работает правильно. Из этих 9 строк 7 — кастомная функция слияния фрагментов слов в строку до заданной длины (три ветки выполнения, рекурсия и одно вспомогательное определение). Остальные две — совершенно очевидные пайпы из простейших библиотечных функций обработки списков и строк. Возможно, кастомную функцию тоже можно сформулировать как foldr, но вряд ли она от этого станет более внятной.

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

А вот дальше — самое интересное. Иллюстрация к тому, что дальше оптимум пройден.

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

Тут-то мне и стало особенно интересно. Потому что демонстрация прелестей зависимых типов обычно не идет дальше безопасного head. Кто программировал на хаскеле, тот знает, что библиотечные head и tail выкидывают ошибку времени выполнения, если входной список пуст. Весьма жесткую ошибку, они считаются аналогами Null Pointer Exception для хаскеля. Причем если tail еще мог бы как-то выкрутиться, то head не может никак — у него тип [a] -> a, и если список пуст, ему валидное значение для возврата тупо неоткуда взять. Так вот, демонстрация зависимых типов начинается (и заканчивается) определением семейства векторов конечной длины, которые на уровне проверки типов (т.е. времени компиляции, а не выполнения) имеют известную длину, и определением head таким образом, что он работает только на векторах длины на 1 больше некоторой другой длины. На потенциально бесконечных списках и списках неизвестной длины — не могут.

А на самом деле система с зависимыми типами — это всегда система с доказательством программы. "Программа успешно скомпилировалась" в них означает "мы доказали про нашу программу некоторые свойства, выраженные в ее типе". См. соответствие Карри-Ховарда. Доказали строго — так, что нам поверила машина. А она рукомашеству не верит.

Хаскель, на самом деле, тоже проверяет доказательство. Поскольку соответствие Карри-Ховарда. Только у хаскеля, во-первых, выразительные возможности системы типов бедноваты, а во-вторых, есть unsafePerformIO :)

Каллаган, как честный ежик, попытался решить на Idris ту же задачу. Очень простую, но не вполне тривиальную. И...

Свойство "ничего в тексте не переставляет" он, похоже, даже сформулировать за 4 месяца не осилил. Доказать свойство про длину очевидного, понятного с первого прочтения, хаскельного кода — тоже. Сформулировать осилил, а доказать — уже нет.

Дальше он попытался написать программу иначе, так, чтобы справиться с доказательством. Что, в общем, не бессмысленно — как тупой перевод на хаскель программы с Java возможен, но не полезен для нервного здоровья, так и тут было бы вполне логично, если правильный способ писать программу на Idris отличается от такового на Haskell.

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

И это человек с бэкграундом в виде написания пруфчекера.

Отсель мораль. Затраты на получение бОльшей уверенности, чем предоставляет хаскель — астрономические. Если вы пишете софт, который будет работать автономно в дальнем конце Солнечной системы лет через 20 после запуска, то они могут окупиться. Тогда собирайте команду ОЧЕНЬ хороших программистов с ОЧЕНЬ хорошим математическим бэкграундом, берите заказ у NASA лет на 10 работы (не одного человека а всей команды), пишите очевидный код, и упирайтесь его доказывать. Не пытайтесь писать код, который будет легче скормить пруфчекеру, но который будет не очевиден — это тупиковый путь.

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

Origin: http://filin.dreamwidth.org/9762.html, comment count unavailable comments

Comments:

[User Picture]
From:slobin
Date:2015, Feb 19, 18:25:39 (UTC)
(Link)
// Свойство "ничего в тексте не переставляет" он, похоже, даже сформулировать за 4 месяца не осилил.

Хи-хи! А он сформулировал свойство "хрен с ним, пускай переставляет, но хотя бы не теряет и не вносит отсебятины"? Просто на сугубо учебных задачках "верифицировать алгоритм сортировки" самое трудное -- сказать, что итоговая последовательность состоит из тех же самых значений, что и исходная. Порядок -- это как бы тривиально.

// у него был забытый в одном из двух мест reverse — довольно частая ошибка у начинающих программистов на хаскеле

То есть в хаскеле до сих пор нормально пользоваться nconc-reverse идиомой? Это же жуть, это мне ещё в 80-х казалось реликтом эпохи экономии каждого машинного слова! За что я люблю современные "скриптовые" языки -- за то что в норме во всех твоих рабочих, служебных и вспомогательных подпоследовательностях порядок всегда совпадает с исходным. Такой инвариант, который ты даже и не пытаешься нарушить. Жизнь как-то сразу становится гораздо проще.

Или ты как раз имел в виду, что списки разворачивают только начинающие программисты, а опытные делают это как-то по другому?

... Смертельная доза обучения ...
(Reply) (Thread)
[User Picture]
From:besm6
Date:2015, Feb 19, 19:45:39 (UTC)
(Link)
> То есть в хаскеле до сих пор нормально пользоваться nconc-reverse идиомой?

Эээ, при чем тут nconc? Хаскель же иммутабелен.

Нет, он там последний пробел в строке искал. reverse, нашел первый пробел, поделил, и оба фрагмента reverse обратно.

Но на самом деле иногда бывает удобнее, делая преобразование списка в список, более сложное, чем map или простой fold, таскать промежуточный список, в который пихаешь с носа, а перед выдачей результата делаешь ему reverse.

Но чаще да, опытный программист нагло пользуется ленивостью и гонит напрямую. А еще чаще - подбирает комбинацию библиотечных функций...
(Reply) (Parent) (Thread)
[User Picture]
From:thesz
Date:2015, Feb 20, 09:44:57 (UTC)
(Link)
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf - верификация алгоритма сортировки от и до. На всякий случай.

Я часто пользуюсь разворачиванием списка для текущих нужд. Оптимизировать надо после.
(Reply) (Parent) (Thread)
[User Picture]
From:slobin
Date:2015, Feb 20, 19:44:10 (UTC)
(Link)
1) Спасибо, почитаю. 2) Я уже понял, что мы с Раном про разное. Я думал, что это про идиому "добавлять элементы в начало списка, а потом развернуть". Это, на мой взгляд, как раз очень низкоуровневая оптимизация. Но оказалось, что речь идёт про "развернуть список, чтобы найти что-то с конца". Мне это почему-то никогда не казалось естественным, но да, моё возражение здесь не годится. Просто моя голова таким способом не думает. Я скорее посмотрю, нет ли в библиотеке соответствующей rsomething, и если нет -- напишу свою и так и назову. Но я не стану доказывать, что так лучше, просто я так привык. :-)

... Привет от Лианта! ...

(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Feb 22, 07:30:44 (UTC)
(Link)
Большое спасибо за ссылку. Исключительно конструктивный взрыв мозга.
(Reply) (Parent) (Thread)
[User Picture]
From:thesz
Date:2015, Feb 23, 22:53:31 (UTC)
(Link)
Ага.

Это авторы Эпиграм. У автора Idris есть более простая и практичная вещь - http://eb.host.cs.st-andrews.ac.uk/writings/fi-cbc.pdf

Оно содержит простое объяснение, как избегать взаимных блокировок и оказалось полезным даже без зависимых типов.
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Feb 27, 19:30:08 (UTC)
(Link)
Спасибо, почитал. Еще не совсем до конца дочитал, но все же.

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

Осталось ощущение, как Каллаган говорил, smell, что что-то в ней криво. Что-то типа "для своих гарантий очень уж громоздкое употребление". И сразу ограничивается случаем, когда ресурсы известны на стадии проверки. Что как бы намекает, что в случае, когда неизвестны, получается еще более громоздко.

Сама идея о том, как избегать взаимных блокировок, мне попадалась и раньше. Интересно было бы решение, ненавязчивое по употреблению, в духе STM, но уверенно отрабатывающее на стадии проверки типов. А у него, судя по всему, так не получается - и громоздко, и он говорит о том, что иногда приходится строить доказательства в рантайме.
(Reply) (Parent) (Thread)
[User Picture]
From:nasse
Date:2015, Feb 19, 18:40:17 (UTC)
(Link)
Любопытно как...
(Reply) (Thread)
[User Picture]
From:beldmit
Date:2015, Feb 25, 17:44:41 (UTC)
(Link)
Тесты эта программа проходит, но они ей, по крайней мере эти, тупо не нужны. Чтение кода дает на порядок больше уверенности в ее правильной работе, чем эти тесты.

Чтение кода требует включения мозга. Запуск тестов – нет. И это сильно экономит глюкозу.
(Reply) (Thread)
[User Picture]
From:besm6
Date:2015, Feb 25, 18:19:41 (UTC)
(Link)
Запустить тесты, конечно, дешево по глюкозе, но их же сначала написать надо.
(Reply) (Parent) (Thread)
[User Picture]
From:beldmit
Date:2015, Feb 25, 20:51:01 (UTC)
(Link)
Если мы говорим о долгосрочной перспективе поддержки, то это всё равно экономнее по глюкозе.
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Feb 25, 21:56:48 (UTC)
(Link)
Да щазз... Для долгой поддержки объем эффективно работающих тестов черного ящика на глазок квадратичен по отношению к объему тестируемого кода. И три четверти из них содержат ошибки.

Если язык таков, что большая часть кода чистая (в смысле pure), и можно его побить на мелкие функции (и тестировать не весь черный ящик, а покомпонентно, за счет referential integrity, обеспеченной чистотой), то можно добиться линейной зависимости, но множитель все равно будет сильно больше 1.

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

А если писать меньше тестов, то они будут неэффективны как раз в долгой поддержке.

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

Ту пару мест, где я не буду уверен, что тайпчекер меня за руку поймает, прогоню в REPL на скорую руку, и оно будет работать долго и счастливо.
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 06:06:51 (UTC)
(Link)
>Свойство "ничего в тексте не переставляет" он, похоже, даже сформулировать за 4 месяца не осилил.
Не очень понятно, что там осиливать: разбиение с последующей склейкой эквивалентны id (или, другими словами, разбиение со склейкой дадут тот же текст). С очевидным уточнением, касающимся двойных пробелов и наличия символов, отличных от пробельных.
(Reply) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 14:22:46 (UTC)
(Link)
Во-во. С очевидным уточнением, касающимся... Сформулировать на типах. Так, чтобы задача "проверить, правильно ли сформулирован тип" не оказалась сложнее исходной.

Кстати, призовая игра на формулировку эквивалентности: при его постановке задачи некоторые слова исходного текста могут разбиться на несколько слов, причем в результате нет информации о том, какие именно. А склеивать без пробелов для проверки эквивалентности нельзя - в условии "ничего не переставляет" исходные промежутки между словами существенны. Поэтому в склейке могут оказаться дополнительные промежутки между словами, которых не было в оригинале. Где именно - предсказать можно, но это задача, почти эквивалентная исходной.
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 16:20:49 (UTC)
(Link)
А так, пожалуй, ещё проще: получится что-то вроде
(s : String) -> ( (removeWhitespaces s) = (concat (split s) ) )

Это, скорее всего, не совсем то, что Вы хотите, но (судя по условию задачи) то, что действительно нужно.
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 17:23:03 (UTC)
(Link)
Увы. При входе "a b c" и ширине 3 (правильный выход - "a b\nc") левая часть будет "abc", а правая - "a bc". При этом "a bc" и "ab c" (при ширине, допустим, 4, когда все влезло в строку) не должны быть эквивалентны.
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 17:57:48 (UTC)
(Link)
Ну это вообще не возражение:
(s : String) -> ( (removeWhitespaces s) = (removeWhitespaces (concat (split s) ) ) )
Я больше боюсь, что в зависимых типах так писать нельзя (не владею я этой областью знаний, могу глупость написать).
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 18:31:09 (UTC)
(Link)
А до конца дочитать коммент, на который отвечаем?

>> При этом "a bc" и "ab c" (при ширине, допустим, 4, когда все влезло в строку) не должны быть эквивалентны.

В качестве реального примера - "another wise clause" и "an otherwise clause" - далеко не одно и то же.

Edited at 2015-06-06 06:44 pm (UTC)
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 18:49:30 (UTC)
(Link)
??? Не понял. Почему и кто не должен быть эквивалентным? Выходы функции split для разной ширины колонки могут (даже должны) отличаться, но мы же обсуждаем свойство "ничего не переставляет в процессе".
Тут в левой и правой части будет "abc", всё нормально.

На самом деле, конечно, моё свойство пропускает перестановки пробельных символов. Но насколько это важно — в отрыве от других функций и задач совершенно непонятно. Более того, какие свойства реально нужны — зависит от этих других функций и задач. Поэтому я бы на первом этапе написал то, что написал выше, и успокоился. Хотя, пожалуй, после нашего обсуждения я бы и "правильное" свойство взялся написать, но это действительно 30-40 строк текста, и как его доказывать — тоже не вполне понятно.
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 19:17:46 (UTC)
(Link)
Да. Мы обсуждаем свойство "ничего не переставляет в процессе". В частности, не переставляет между собой части слов и межсловные промежутки. Поэтому утверждение "ничего не переставляет" не должно считать одинаковыми "a bc" и "ab c" (переставлены "b" и промежуток).

Понятно, что правильное утверждение в принципе можно сформулировать. Но я утверждаю, что _сформулировать_ его (на типах) и _проверить, что оно сформулировано правильно_ (т.е. программа с этим типом будет решать именно нужную задачу) - задачи примерно той же сложности, что решить исходную задачу (в лоб) и проверить, что она решена верно (вручную). Если не сложнее. Вот в чем проблема.
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 20:03:30 (UTC)
(Link)
Не вижу необходимости проверять, что утверждение сформулировано правильно. Ведь типы лично я тоже иногда с большим трудом могу правильно выписать. Но в тех случаях, где тип мне очевиден, а функция муторная, я этот тип пишу и часто это помогает разобраться, т.к. тупой компилятор тыкает более умного, но менее внимательного меня, носом в ошибку. Иногда тип пишу неправильно, и в процессе разбора это выясняю. Трагедии в этом нет — исправляю тип и продолжаю. А вообще я даже тип в 95% функций не пишу — тех аннотаций, которые написали авторы библиотек, достаточно, чтобы компилятор мог мне помогать.
Так и с утверждениями должно быть — например, в 95% случаев я не буду писать никаких утверждений про свои функции, но не смогу криво скомбинировать чужие функции, для которых авторы библиотек утверждения сделали. Надо — написал утверждение. Если в процессе выяснилось, что утверждение ошибочно — исправил. Уверенности в правильности нет, но согласованно напутать в коде и утвеждении без наличия реального непонимания очень сложно.
(между прочим, правильно ли сформулировано утверждение, даже заказчик часто может сказать только после недельной работы с программой)
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 22:30:44 (UTC)
(Link)
Тут какая засада: машина думать не может. Как только она на каком-то шаге не смогла получить доказательство - все, до свидания, программа дальше не компилируется. Собственно, именно потому, что машина думать не может, языки программирования с зависимыми типами, в отличие от хаскеля, практически не умеют выводить типы. Только проверять указанные, а если тип не указан, вообще отказываются работать.

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

Если мы о задаче все равно рассуждаем, помавая руками, то это, действительно, не трагедия - пока типы простые и структура программы обозрима. Уверенность, конечно, будет далека от полной, но для типичных задач этого достаточно. А вот с ростом сложности задачи контроль теряется очень быстро. Мы можем быть уверены в решении задачи, но совершенно не понимаем, какой, либо наоборот, можем понять, какая задача решается, но не можем понять, успешно ли. Причем первого достичь на порядок труднее, чем второго.

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

Ситуации, когда код прозрачный, а тип громоздкий по делу, бывают, но крайне редко.
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 19:11:30 (UTC)
(Link)
Ё!!! Всё ж ещё проще!
Надо, чтобы split возвращала не список строк, а список пар строк (оставленные и выброшенные пробелы). Дальше продолжать или очевидно?

Если тип пар в результате не нравится, то это будет вспомогательная функция split', а нужная нам определяется как split s = map fst (split' s)
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 19:27:03 (UTC)
(Link)
Ну, это уже логичнее.

Но тут возникнет та проблема, которую я в посте упоминал не слишком явно. Как только мы выкидываем ненужную для использования результата информацию - мы немедленно с нею теряем и доказательство того, что программа работает правильно. И если мы хотим использовать нашу программу в большей программе и иметь автоматическое доказательство, нам эту информацию выкидывать нельзя. Так что фиг нам map fst...
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 19:48:55 (UTC)
(Link)
Я так понимаю, формулировка свойства Вас более-менее устроила. У меня же изначально было недоумение, что там формулировать 4 месяца (у нас с Вами ушло "полдня под пиво", а мы всё же не спецы в теме).

Не понимаю, какая информация выкинута. Модифицировать результат я предложил в "дидактических" целях (кажется, так понятее). Но свойство-то я изначально придумал вот какое: "существует такой список пар l, что ... и (split s) = (map fst l)". Теоретически, не вижу причин, по которым оно не будет автоматически выводиться из свойств вспомогательной функции split'.
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 20:11:49 (UTC)
(Link)
У него-то стояла задача не только сформулировать, но и написать программу с этим типом. Если начать ее писать, то быстро выяснится, что там не все так просто...

С выкинутой информацией. В свойстве "существует такой список пар, что ..." выкинута информация о том, как его добыть. А поскольку все доказательства в машине строго конструктивные, то нет примера - нет доказательства существования.

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

А байку про систему доказательства, которой предложили самостоятельно найти пример, мне в свое время травили. Сложность самостоятельного поиска имела порядок роста 2^{2^n} (еще с каким-то множителем при n), и уже при n=3 машина, как следует подумав, говорила "извините, память кончилась". Когда к этому месту подошел программист, и доказательство явно закодировал, сложность упала до n^3. Такая вот цена выкидывания подтверждающих примеров...
(Reply) (Parent) (Thread)
[User Picture]
From:os80
Date:2015, Jun 6, 20:48:08 (UTC)
(Link)
То, что с написанием программы возиться можно долго — понятно, но у Вас написано, что он и сформулировать свойство (похоже), "ниасилил". Чему я и удивился.

>выкинута информация о том, как его добыть
Не верю. Если Вы не выкинули исходную строку, то надо применить к ней split' и насладиться полученным списком пар. А если Вы её выкинули, то по сравнению с чем функция split ничего не переставляет?
(Reply) (Parent) (Thread)
[User Picture]
From:besm6
Date:2015, Jun 6, 22:07:46 (UTC)
(Link)
Ну, я ему в мозг не заглядывал - ниасилил он вообще, или ниасилил формулировку, под которую смог бы, как ему казалось, написать программу. С точки зрения задачи цикла статей разницы нет.

Про "выкинуть". Я говорю о том, что в типе функции split нет информации, (практически) позволяющей _машине_ утверждать, что она обладает заявленным свойством. В типе функции split', вероятно, есть, но тогда, чтобы машина могла этим свойством пользоваться, придется везде применять не split, а split', тип которой гораздо толще. Что, собственно, в обсуждаемой статье и наблюдается, но с другим свойством. А дальше экспоненциальное раздувание типа, как только мы хотим получить доказательство еще парочки свойств...

Насколько я понимаю, если пользоваться proof assistant'ом, а не просто языком с зависимыми типами, то там все же мухи отдельно, котлеты отдельно, хотя мухи и котлеты взаимосвязаны. И там все же можно доказать про программу какую-нибудь лемму, не трогая саму программу. Не любую лемму, конечно (для чего-то будет проще уже переписать программу), но рост сложности в зависимости от желания уверенности уже не экспоненциальный. А если у нас только зависимые типы и простой (зато достаточно быстро работающий) тайпчекер, то получается такая вот сложностная фигня.

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

Возможно, proof assistant позволяет большую уверенность, но цена вопроса - стоимость разработки, причем даже не столько в деньгах, сколько во времени. Если мы пишем программу для "Вояджера", оно, возможно, окупится, а уже даже для марсохода - не факт.
(Reply) (Parent) (Thread)