Здравствуйте, Mamut, Вы писали:
EP>>Вот твой изначальный пример: EP>>это можно трактовать как "можно уменьшать и увеличивать сумму заказа" — это функция change_amount, у которой есть предусловие "заказ не помечен как отправленный", которая безусловно изменяет сумму. Тебе как раз и показывали примеры форсирующие это предусловие в compile-time: M>Я перенес это «предусловие» внутрь функции change_amount.
Нарушение предусловия это баг в программе, программа находится в том состоянии в котором не должна была по логике вещей, и как она туда попала неизвестно, лучше всего пристрелить такую программу как взбесившуюся собаку. Почитай наконец что такое precondition.
Предусловия можно проверять, и как-то энфорсить, но отнюдь не обязательно. Например assert'ы энфорсящие предусловия часто используют только в отладочных режимах.
Система типов позволяет энфорсить некоторые предусловия в compile-time, но не все. Я даже больше скажу, далеко не все предусловия можно проверить в runtime — попытка такой проверки попросту может поломать инварианты, и сделать невозможным достижение постусловий.
M>Что изменилось? Ничего. Все те же «предусловия» надо продолжать проверять прежде, чем произойдет собственно изменение значения.
Поменялся контракт/интерфейс. Вместо change_amount_unconditionally стало try_change_amount. То что раньше было предусловием, стало обыкновенным перекрёстком в коде. То что раньше было недопустимым состоянием — запуск change_amount с невыполненными условиями — стало штатным режимом работы.
M>Можно увидеть на деле то, что описано в корневом сообщении этого топика? Я за пять минут написал свое решение. Ни один из апологетов типов не осилил написать это решение
Я сразу сказал, что в данной постановке это не имеет смысла:
EP>Если же для запуска функции нет необходимости делать проверки, change_amount сама всё что нужно проверяет внутри, и более того её запуск с невыполненными условиями не является ошибкой, а вполне штатным режимом — то пытаться переписать все эти внутренние проверки на типы, не вижу смысла, это никак не отразится на местах вызова этой функции.
M>только отмазки, рассказы про то, как все будет хорошо,
Твои фантазии.
M>и наугад вырванные отдельные куски условий с заявлениями «видишь, как все хорошо»?
Это куски из других задач, с другой постановкой. Почему тут приводятся, читай рядом с самими кусками, например:
EP>order<processed, prepaid, not_risk, amount_rise_allowed>, либо просто order<state>
Можно увидеть это на примере решения задачи, которую я привел? Ну, на основе твоих заявлений:
— на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time.
— как можно больше логики кодировать в типах и проверять компилятором.
— И чем выразительней эта система [типов] и чем удачнее применяется, тем больше проблем выявляется при компиляции.
M>>Короче, понятно. Все сказки про «целые классы ошибок» и «цепочки условий» и «логику» на практике упираются ровно в одно: как бы не сложить метры с киллограммами. Этот «целый класс ошибок» является очень маленьким классом ошибок.
EP>Так ты определились, либо "целые классы ошибок" это сказки, либо нет и тебе просто не нравится количество этих классов, а конкретно их концентрация в одном примере из твоего опердня
Мне не нравится, что высокопафосные заявления про, например, "на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time." скатываются в банальное «ну, главное чтобы килограммы с метрами не складывались»
Этот весь «класс ошибок» является весьма маленьким.
Тебе не нравится пример из опердня, приведи ссылку на код не из опердня
M>>Можно увидеть на деле то, что описано в корневом сообщении этого топика? Я за пять минут написал свое решение. Ни один из апологетов типов не осилил написать это решение
EP>Я сразу сказал, что в данной постановке это не имеет смысла: EP>
EP>>Если же для запуска функции нет необходимости делать проверки, change_amount сама всё что нужно проверяет внутри, и более того её запуск с невыполненными условиями не является ошибкой, а вполне штатным режимом — то пытаться переписать все эти внутренние проверки на типы, не вижу смысла, это никак не отразится на местах вызова этой функции.
Да, но ничего не изменилось. Цепочка условий и прочая и прочая так и остались, просто сместилась точка вызова
M>>только отмазки, рассказы про то, как все будет хорошо,
EP>Твои фантазии.
M>>и наугад вырванные отдельные куски условий с заявлениями «видишь, как все хорошо»?
EP>Это куски из других задач, с другой постановкой. Почему тут приводятся, читай рядом с самими кусками, например: EP>
примерно ноль. Ну, вернее разница лишь в том, что задача в этом топике — это развернутое описание второго пункта. Все твои бурные фантазии про пред-пост-над-под-из-за-условия — лишь твои бурные фантазии.
Здравствуйте, Mamut, Вы писали:
EP>>order<processed, prepaid, not_risk, amount_rise_allowed>, либо просто order<state> M>Можно увидеть это на примере решения задачи, которую я привел? Ну, на основе твоих заявлений:
Повторюсь в очередной раз, для этой задачи это не имеет смысла.
M>- на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time.
Да.
M>- как можно больше логики кодировать в типах и проверять компилятором.
Да, желательно.
M>- И чем выразительней эта система [типов] и чем удачнее применяется, тем больше проблем выявляется при компиляции.
Всё верно.
Вся эта полемика уже сводится к:
"
A: Мультиметр полезная штука для некоторых задач — позволяет измерять напряжение, силу тока, сопротивление. Чем качественнее прибор — тем точнее результат.
B: Я вот тут гвозди забиваю. Например вот так — БАХ, БАХ. Покажи чем мне тут поможет этот мультиметр.
A: Для этой задачи не имеет смысла.
B: АГА, шах и мат! "качественнее прибор — точнее результат", "некоторых задач" — всё это сказки про белого бычка!
"
EP>>Так ты определились, либо "целые классы ошибок" это сказки, либо нет и тебе просто не нравится количество этих классов, а конкретно их концентрация в одном примере из твоего опердня M>Мне не нравится, что высокопафосные заявления про, например, "на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time." скатываются в банальное «ну, главное чтобы килограммы с метрами не складывались»
Так действительно, при наличии compile-time аргументов их можно использовать в сложных условиях. Например если есть compile-time массив, его можно отсортировать, делать двоичный поиск, и на основании результата разрешать или запрещать вызов конкретной функции. С чем не согласен-то?
M>Этот весь «класс ошибок» является весьма маленьким.
Уж точно не серебряная пуля от всех ошибок.
M>Тебе не нравится пример из опердня, приведи ссылку на код не из опердня
EP>Повторюсь в очередной раз, для этой задачи это не имеет смысла.
Предложи задачу, для которой имеет
EP>Да. EP>Да, желательно. EP>Всё верно.
Но при этом «для этой задачи не имеет смысла» Причем оно внезапно перестало иметь смысл ровно после того, как все те же множественные условия, о которых ты говорил, остались на месте, только стали не выдуманные тобой вызовы с *-условиями, а стал один вызов
EP>Вся эта полемика уже сводится к:
Ложные аналогии такие ложные
M>>Мне не нравится, что высокопафосные заявления про, например, "на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time." скатываются в банальное «ну, главное чтобы килограммы с метрами не складывались»
EP>Так действительно, при наличии compile-time аргументов их можно использовать в сложных условиях.
Определи понятие «сложные условия» и почему условия в моей задачи, видимо, недостаточно сложные Или — о ужас — данные о заказе не compile-time, из-за этого ничего поделать нельзя? Ну извини, реальный мир он такой — подавляющее большинство данных получаются не в compile-time
EP>Например если есть compile-time массив, его можно отсортировать, делать двоичный поиск, и на основании результата разрешать или запрещать вызов конкретной функции. С чем не согласен-то?
1. Нафига?
2. Пример того, где это используется, в студию
M>>Тебе не нравится пример из опердня, приведи ссылку на код не из опердня EP>Чем тебе не нравится пример с аффинным пространством? Конкретный пример std::chrono — time_point и duration. EP>http://en.cppreference.com/w/cpp/chrono
Вау. Не прошло и недели и стапятидесяти сообщений, как внезапно кто-то из апологетов родил хоть что-то похожее на реальный пример. Не знаю, при чем тут аффинные пространства, из того, что вижу — это энфорсинг типов. Ну, то самое «не складывать килограммы с метрами». Отлавливается первым же залетным тестом
Ну да, при рефакотринге будет приятно. В реальных задачах будет занимать мизерную часть проблем.
Здравствуйте, Mamut, Вы писали:
M>Этот весь «класс ошибок» является весьма маленьким.
Правильно я понимаю, что ты за динамическую типизацию вообще? Потому что аргументы уж больно похожи: типы спасают только от сложения яблок с килограммами, а такие ошибки допускают только слабоумные, тесты писать всё равно надо, так что типы не дают ничего.
По моему, относительно активно за "всю логику на типах" агитировал аж один человек и тот хаскелист, так что не удивительно. Все остальные гораздо осторожнее высказывались. Лично мне на динамических языках писать не особо комфортно, больше нравится когда компилятор помогает. Вот собственно и всё.
Ну и от языка зависит. Решения на С++ вряд ли будут смотреться сильно изящно, там для простого "strong typedef" надо напрягаться, так что большинство просто на это забивает. В других языках с этим лучше, но так чтобы прямо вся логика на типах и это было удобно и элегантно не видел.
Имхо, оптимальное решение лежит где-то посредине, а ты пытаешься доказать бесполезность типизации, причём в основном, эмоциями.
M>>Этот весь «класс ошибок» является весьма маленьким. DE>Правильно я понимаю, что ты за динамическую типизацию вообще?
Нет. Я готов быть за что угодно, что мне внятно покажут и расскажут.
DE>Потому что аргументы уж больно похожи: типы спасают только от сложения яблок с килограммами, а такие ошибки допускают только слабоумные, тесты писать всё равно надо, так что типы не дают ничего.
But I discovered that in the presence of SelfTestingCode, most bugs that static types would have were found just as easily by the tests. Since the tests found much more than type errors, you needed them in either a static or dynamically typed language, so having the static typing gave you little gain.
DE>Имхо, оптимальное решение лежит где-то посредине, а ты пытаешься доказать бесполезность типизации, причём в основном, эмоциями.
Нет. Я пытаюсь выбить из апологетов типизации хоть что-то реальное, а не последовательные сказки
про то, как типизация помогает, спасает, проверят и прочая и прочая и прочая. Любые наводящие вопросы разбиваются о стену новых «верь мне, компилятор все проверит» и т.п. Ну вот ярчайший пример
как раз подойдёт. Добавить в кортеж "Order" признаки "received", "checked", "approved" и так далее — и потребовать, чтобы заказы были допущены к исполнению только в случае, если они были проверены (т.е. у них стоит соответствующий флажок). Проверки сделать через сопоставление с образцом.
Это не отличается от проверок с помощью типов, но, правда, есть один НЮАНС!
В ирлонгах отсутствует изменяемое состояние, поэтому ставить флажки не получитьса. Надо будет создавать каждый раз новый кортеж...
как раз подойдёт. Добавить в кортеж "Order" признаки "received", "checked", "approved" и так далее — и потребовать, чтобы заказы были допущены к исполнению только в случае, если они были проверены (т.е. у них стоит соответствующий флажок). Проверки сделать через сопоставление с образцом.
Можно код полностью, пожалуйста? А то «добавь тут, добавь там, допущены к исполнению» — это как-то сверх-абстрактно
O>Это не отличается от проверок с помощью типов, но, правда, есть один НЮАНС! O>В ирлонгах отсутствует изменяемое состояние, поэтому ставить флажки не получитьса. Надо будет создавать каждый раз новый кортеж...
approve({order, {data, D}, {flags, F}}) when order_is(F, checked) ->
%
% До этого места дойдём только если в кортеже {order, {data, ...}, {flags, ...}}
% есть кортеж {flags, ...} и в нём есть элемент checked, то есть если он выглядит
% как {flags, ..., checked, ..., ..., ...}
%
.
А вызывать её будем так:
case approve(Order) of
{ok, ...} ->
...
_ ->
exit(badOrderstState)
end.
По аналогии с операторами в C, переключающими и проверяющими битовые флажки.
Только здесь при добавлении/отключении флажка придётся заново создавать новый кортеж Order.
Здравствуйте, Mamut, Вы писали:
J>>И стопятьсот сообщений от тебя про белого бычка, тупо игнорирующих все, что тебе говорят (и это сообщение — тоже яркий тому пример: ты тупо проигнорировал мои слова наверху, и так почти со всем).
M>Проигнорорвал какие слова? Давай я приведу твои слова.
Ну и в очередной раз ты просто процитировал мои слова без какого-либо конструктивного ответа на них. Спасибо за еще одну иллюстрацию.
, что можешь написать решение в лоб за пять минут, будто кто-то здесь этого не может, и будто кто-то утверждал, что типы позволят писать решение за четыре минуты.
В общем, классические приемы демагогии в полный рост, можно прямо в учебник вставлять. Особенно виртуозно тебе удаются подмена тезиса и ингорирование аргументов, аплодисменты.
Здравствуйте, Mamut, Вы писали:
M>Мне просто действительно интересно. Многие утверждают, что типы помогают (чуть ли не) во всем, вплоть до того, что «тайпчекер проверяет именно логику».
M>У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить.
Ты бы еще предложил задачу "посчитать md5" и спросил как ее решить "типами".
M>>У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить. A>Ты бы еще предложил задачу "посчитать md5" и спросил как ее решить "типами".
J>В общем, классические приемы демагогии в полный рост, можно прямо в учебник вставлять.
С твоей стороны? Безусловно. Я так и не увидел ни одного мало-мальски внятного примера на хоть одно из твоих заявлений. А ты утверждаешь, что я неконструктивен. Ну-ну.
M>>Можно код полностью, пожалуйста? А то «добавь тут, добавь там, допущены к исполнению» — это как-то сверх-абстрактно O>Флажки будет проверять функция: O>А вызывать её будем так: O>По аналогии с операторами в C, переключающими и проверяющими битовые флажки. O>Только здесь при добавлении/отключении флажка придётся заново создавать новый кортеж Order.
А, так стало понятнее По сути, это более наглядно переписанный мой пример. Согласен
Вот тут как раз и поможет компилятор — как раз с ad-hoc изменениями требований.
Вот появилась задача с ad-hoc требованиям, основанная на реальной задаче из кода самого настоящего банка. Специально написал, чтобы проверить, как все ваши заявления работают при столкновении с реальной задачей.
A>это чистая математика (логика), тут даже алгоритма как такового нет, просто длинное булево выражение.
Если ты когда-нибудь собирал мозаичные пазлы, то должен был заметить, что различная форма фрагментов рисунка позволяет избежать большинства ошибок и резко ускорить выполнение задачи. Типы в любой логике выполняют примерно туже самую роль.
как можно больше логики кодировать в типах и проверять компилятором.
Для типов есть легковесная верификация, в случае их отсутствия не все так радужно. Она [логика] не перестает быть логикой, она представляется в форме, которая хорошо подходит для автоматической проверки.
Аплогеты типов, вы уже определитесь со своим набором рассказов про типы А то вы опровергаете слова друг друга
Здравствуйте, Mamut, Вы писали:
M>Если эта задача настолько проста, что же апологеты типов не могут ее решить, несмотря на стопятьсот красивых текстов о том, как типы все решают?
А смысл решать даже пусть теперь известно откуда выковырянные задачи? Мне такие задачи напоминают демонстрации от евангелистов. Берём примитивную задачу и показываем как круто она делается с помощью скажем Model First. Затем по максимуму снижаем акцент с "примитивная задача круто делается" и по максимум завышем его на "круто делается с помощью Model First". В результате получаем распиаренную технологию, которая к разработке реальных приложений не имеет никакого отношения.
Ты пытаешься сделать тоже самое. Показать на примитивной задаче ненужность типов. При этом делая акцент не на примитивности, а на ненужности.
IT>>Если ты когда-нибудь собирал мозаичные пазлы, то должен был заметить, что различная форма фрагментов рисунка позволяет избежать большинства ошибок и резко ускорить выполнение задачи. Типы в любой логике выполняют примерно туже самую роль. M>Демагогия.
Ты слегка перепутал демагогию и аналогию. Демагогия — это способ ввести аудиторию в заблуждение. Аналогия, если она приводится в качестве пояснения, а не в качестве доказательства, помогает лучше понять предмет с помощью уже известных понятий. Будешь знать.
Но продолжим аналогию. Ты фактически утверждаешь, что картинку можно просто разрезать на квадратики и не париться с пазлами и приводишь в качестве примера картинку из четырёх таких квадратиков. Ну хорошо, в этом случае наверное можно и не парится. Но что ты будешь делать с картитинкой в 1000 элементов? Если это будут квадратики, а не пазлы, то тебе потребуется на порядок больше времени.
Типы — это дополнительный уровень верификации кода на самых ранних этапах возникновения проблемы. Те же юнит-тесты ловят последствия, типы позволяют устранить причину. Мне вообще странно слышать подобные разговоры от людей с опытом. То, что вы у себя в конторе научились есть кактус и при этом не сильно колоться, говорит лишь о вашем упёрстве и пониженном болевом пороге. Это очень круто. Примерно так же круто, как в цирке глотать шпаги или совать голову в пасть хищнику. И если бы вы со своим кактусом выступали в цирке, то я бы аплодировал стоя. Но в жизни то это нафига нужно?
Если нам не помогут, то мы тоже никого не пощадим.
Здравствуйте, Mamut, Вы писали:
M>>>У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить. A>>Ты бы еще предложил задачу "посчитать md5" и спросил как ее решить "типами".
M>Приведи другой пример
а что именно ты хочешь? полиморфизм?
возьми задачу где есть сущности разных типов, например парсер выражений, рисователь картинок, генератор отчетов, — что-то где есть несколько объектов с разным поведением.
тогда у тебя так или иначе будут разные структуры данных с прибитым к ним кодом.
или тебе надо статическую проверку типов?
ну это банальное "T& x; x.y()" vs "T* x; if (x) x->y()" в С++
или signed vs unsigned,
или optional<T> и прочие паттерн-матчинги, монады и вот это всё
EP>>Да. EP>>Да, желательно. EP>>Всё верно. M>Но при этом «для этой задачи не имеет смысла»
Да, и что из этого?
M>Причем оно внезапно перестало иметь смысл ровно после того, как все те же множественные условия, о которых ты говорил, остались на месте, только стали не выдуманные тобой вызовы с *-условиями, а стал один вызов
Состояние ранее являвшееся ошибкой, стало вполне штатным режимом работы, и это повлияло на возможные варианты реализации этого в коде. И что тебя удивляет?
EP>>Вся эта полемика уже сводится к: M>Ложные аналогии такие ложные
Я вижу это именно так. Если ты видишь это по-другому, можешь дополнить/исправить аналогию.
M>>>Мне не нравится, что высокопафосные заявления про, например, "на типах можно задать какие угодно условия, главное чтобы аргументы условий были доступны compile-time." скатываются в банальное «ну, главное чтобы килограммы с метрами не складывались» EP>>Так действительно, при наличии compile-time аргументов их можно использовать в сложных условиях. M>Определи понятие «сложные условия» и почему условия в моей задачи, видимо, недостаточно сложные
Так сразу же:
EP>>Например если есть compile-time массив, его можно отсортировать, делать двоичный поиск, и на основании результата разрешать или запрещать вызов конкретной функции. С чем не согласен-то? M>1. Нафига?
Пример сложных условий, с нетривиальными вычислениями.
M>Или — о ужас — данные о заказе не compile-time, из-за этого ничего поделать нельзя? Ну извини, реальный мир он такой — подавляющее большинство данных получаются не в compile-time
Runtime данные можно переводить в compile-time, причём данные любой сложности, об этом я неоднократно говорил в предыдущем топике, и даже приводил конкретный код. Вопрос упирается в code-bloat.
Перевести несколько bool из runtime в compile-time — не проблема. А вот например перевод unsigned price — скорей всего будет непрактичным.
EP>>Чем тебе не нравится пример с аффинным пространством? Конкретный пример std::chrono — time_point и duration. EP>>http://en.cppreference.com/w/cpp/chrono M>Вау. Не прошло и недели и стапятидесяти сообщений, как внезапно кто-то из апологетов родил хоть что-то похожее на реальный пример. Не знаю, при чем тут аффинные пространства,
Это и есть пример аффинного пространства, где duration это вектор, а time_point — точка.
M>из того, что вижу — это энфорсинг типов. Ну, то самое «не складывать килограммы с метрами».
Более сложный пример: на типах можно задать грамматику DSL, и разрешать только те выражения, которые проходят проверку. Пример — Boost.Proto.
M>Отлавливается первым же залетным тестом
Mars Climate Orbiter тесты не спасли. Хотя, по всей видимости, тестировалось всё более пристрастно чем типичный опердень.
M>Ну да, при рефакотринге будет приятно. В реальных задачах будет занимать мизерную часть проблем.
Считай перед вызовом каждой функции расставляются виртуальные assert'ы, которые отрабатывают на этапе компиляции.
В динамических же языках эти assert'ы подразумеваются, но никак не энфорсятся. И соответственно чем больше программа, тем больше вероятность что какая-то из ошибок подобного рода будет пропущена. Если вероятность пропуска/фейла одного такого assert'а 0.01, то уже для 230 мест вероятность пропуска хотя бы одного будет 0.9.
И даже 100% покрытие строчек кода тестами не даёт гарантии что все ошибки этого класса найдены.
Если нам не помогут, то мы тоже никого не пощадим.
