Здравствуйте, Mamut, Вы писали:
K>>Во что не верится-то? В каком месте тут вера нужна? M>Во все то, что ты тут так радостно описываешь.
Это не ответ на мой вопрос.
M>Заметь: ты ограничиваешь ся строго заявлениями уровня «все будет хорошо»
Ну это точно неправда.
Я написал следующее:
нельзя будет сконструировать заказ с состоянием "Отправленный" и "Непроверенный как написано в 4-м пункте" одновременно, так что в случае забывания 4-го пункта будет ошибка компиляции. Ну, как нельзя забыть проверить значение типа Maybe Foo на пустоту и вызвать функцию bar заданную на Foo, потому что она на Maybe Foo не определена.
Повторяю вопрос: что тут конкретно требует веры?
M>В итоге у тебя будет развесистый тип, включающий в себя стопятьсот условий. Прекрасно. Чем это лучше любого другого решения? Как ты будешь проверять, что эти стопятьсот условий у тебя реализованы правильно?
Т.е. вы ожидаете что в "развесистом типе" все "стопятьсот" условий будут "ортогональными" и в случае ошибки нигде не вступят в противоречие?
M>Откуда взялись 1024 мест, известно только тебе
Оттуда же, откуда у вас "стопятьсот" условий взялось.
K>>Во-вторых если у вас достаточно сложная спецификация в типе закодирована, то в том случае, если у вас какие-то проблемы с самой спецификацией на типах — скорее всего возникнут противоречия в спецификации, которые тайпчекер сможет обнаружить.
M>Опять сказки про белого бычка.
Интересно как вы сможете нагородить бессмыслицы таким образом, чтоб эта бессмыслица еще и типизировалась. Без серьезных трудозатрат по обходу системы типов разными способами тут не обойтись.
M>Выше ты не слова не сказал про то, как находятся логические ошибки.
Тайпчек — это процесс нахождения логических ошибок.
M>Ты сказал ровно две вещи: M>- вместо 1024 мест будет одно M>- тайпчекер выявит проблемы спецификации M>1024 места ты придумал.
Это, например, места вызова функций, определенных на обсуждаемом "развесистом типе". Навряд ли у вас тип "развесистым" получится и при том таких мест будет немного.
M>Каким образом тайпчекер выявит проблемы спецификации — неизвестно.
Это как раз известно. Почитайте какой-нибудь ликбез по тайпчекерам. Typing Haskell in Haskell, например, да что угодно.
M>Я это, видимо, должен просто на веру принять.
Никто вас не заставляет ничего на веру принимать, не выдумывайте.
M>Видимо, те 40 условий, что ты предложил впихнуть в тип, моментально становятся правильными только из-за того, что ты описал в типе, ага
M>Каким образом? Каким образом стат. проверка типов поможет отослать правильное письмо, сделать правильный risk check и т.п., да еще в нужные моменты времени?
Поможет на ранних этапах выявить некоторые классы ошибок в коде, который "отсылает письмо", "делает правильный risk check" и т.п.
'You may call it "nonsense" if you like, but I'VE heard nonsense, compared with which that would be as sensible as a dictionary!' (c) Lewis Carroll
Re[27]: Haskell нужен! (в Standard Chartered Bank)
M>>Действительно. Давай сделаем тип UnprocessedNonPrePaidRiskClearedOrder, ProcessedNonPrePaidRiskClearedOrder, UnprocessedPrePaidRiskClearedOrder, ProcessedPrePaidRiskClearedOrder и еще два десякта таких же. Это же так удобно!
DM>Ну, если ты пишешь на Си или Го, то такая беда, да. В нормальных же языках полиморфизм позволит общие вещи описать лишь однажды, а разницу вынести, так что ненужного повторения много не будет.
«В нормальных языках», «полиморфизм». Ну можно на примере, а?
M>>Тут не нужны ни нетипизированная программа, ни тестовые данные. Потому что она в лоб решается так, как там описано:
K>Можно, например, определить функции проверки, обновлений, записывания не на одном и том же типе Order, а на разных типах различных стадий обработки Order. K>Тогда если пропустить проверку, перепутать местами этапы обработки, не обновить, не записать — будет ошибка компиляции.
Если все эти проверки спрятаны в банальном API-вызове order:update_amount, то смысл? Вот у нас эта проверка существует уже лет шесть. Менялась один раз, весной. Второй раз будет меняться вот буквально через неделю.
Главная проблема — не в мифических проблемах с типами, а в логике: на каком именно этапе сделать проверку, и какую именно проверку. Ну и написать тесты, проверяющие, что логика работает правильно
M>>Да не показано нигде. Идут сплошные сказки и рассказы про то, как все будет зашибись, и я в это должен верить Как магическая система типов все сома отловит, как невозможно будет написать неправильный код и т.п.
K>Вы что-то сильно разбушевались, как я посмотрю.
Я не разбушевался. Я прошу простых внятных ответов на мои вопросы.
K> сказки не рассказывал и не обещал, что "все будет зашибись".
Да неужели? Процитирую тебя:
Чтоб испортить этот бесплатный праздник [внезапно появившийся на пустом месте — М.] нужно уже какие-то усилия по обходу/затиранию типов прилагать, строково-ориентированным программированием, всякими кастами, реинтерпретацией памяти, рефлексией и другими веселыми вещами. Т.е. программист уже должен быть не просто ленивым, а активно злонамеренным.
Для типов есть легковесная верификация
Она не перестает быть логикой, она представляется в форме, которая хорошо подходит для автоматической проверки.
И т.п.
На практике, когда начинаешь говорить с людьми, которые дают внятные ответы с примерами того, что они имеют в виду, ВНЕЗАПНО оказывается, что нет: или типы становятся слишком сложными, или часть проверок все равно в рантайме и т.п.
M>>Извини, не верю. Учитывая, что ты даже не смог ни разу ответить на простой вопрос «как это все будет проверяться и дебажиться». K>Если вы игнорируете ответ, это еще не значит, что вам никто не ответил.
Если ответ состоит из расказов и сказок про то, как все будет великолепно, то да, я это проигнорирую.
K>Ну это точно неправда. K>Я написал следующее: K>
K>нельзя будет сконструировать заказ с состоянием "Отправленный" и "Непроверенный как написано в 4-м пункте" одновременно, так что в случае забывания 4-го пункта будет ошибка компиляции. Ну, как нельзя забыть проверить значение типа Maybe Foo на пустоту и вызвать функцию bar заданную на Foo, потому что она на Maybe Foo не определена.
K>Повторяю вопрос: что тут конкретно требует веры?
Опиши, как ты это себе представляешь, учитывая, что состяние «Отправленный и непроверенный как написано в 4-м пункте» — это только одно из условий, после чего этот заказ будет использоваться в следующей проверке, для которого нужен другой набор состояний.
в качестве примера. Это, кстати, еще не все условия.
M>>В итоге у тебя будет развесистый тип, включающий в себя стопятьсот условий. Прекрасно. Чем это лучше любого другого решения? Как ты будешь проверять, что эти стопятьсот условий у тебя реализованы правильно? K>Т.е. вы ожидаете что в "развесистом типе" все "стопятьсот" условий будут "ортогональными" и в случае ошибки нигде не вступят в противоречие?
То есть ты ожидаешь, что так не будет?
M>>Откуда взялись 1024 мест, известно только тебе K>Оттуда же, откуда у вас "стопятьсот" условий взялось.
Эти стопятосот условий описаны в одном API Вызывается оно из трех или четырех мест. Грубо говоря, order:set_amount(Order, Amount). Этот вызов возвращает или обновленный заказ или {error, Reason}.
С какого перепугу что-то надо править в 1024 местах вместо одного, известно только тебе одному.
K>Интересно как вы сможете нагородить бессмыслицы таким образом, чтоб эта бессмыслица еще и типизировалась. Без серьезных трудозатрат по обходу системы типов разными способами тут не обойтись.
Ты пока не смог показать, как ты собираешься городить осмыслицу
M>>Выше ты не слова не сказал про то, как находятся логические ошибки. K>Тайпчек — это процесс нахождения логических ошибок.
С какого перепугу? Тайпчек — это проверка, что все типы сходятся. К логическим ошибкам он не имеет никакого отношения.
K>Никто вас не заставляет ничего на веру принимать, не выдумывайте.
Ну ты лично написал с полдесятка сообщений, рассказывая, как все прекрасно
M>>Каким образом? Каким образом стат. проверка типов поможет отослать правильное письмо, сделать правильный risk check и т.п., да еще в нужные моменты времени? K>Поможет на ранних этапах выявить некоторые классы ошибок в коде, который "отсылает письмо", "делает правильный risk check" и т.п.
Ой. Уже внезапно не «проверка логики» и не «условия не будут противоречить», а «некоторый класс ошибок». Внезапно, да.
Здравствуйте, Mamut, Вы писали:
A>>Ограничение "нельзя менять amount у processed order" выглядит стабильным.
M>Увы, нет Начиная с "все спецификации ad-hoc" из оригинального сообщения и до последнего тикета, который таки позволяет увеличивать сумму заказа для pre-paid закаов согласно конфигурации магазина. И это связано с дополнительной логикой — что, если
Вот тут как раз и поможет компилятор — как раз с ad-hoc изменениями требований. Если раньше с processed order можно было делать все, что угодно, а потом вдруг "концепция поменялась" и amount у него больше менять нельзя — достаточно отразить это в определении типа, а дальше компилятор сам ткнет во все места, где код не соответствует новому определению, и попросит дописать соответствующие ифы вроде if (!processed) change_amount(), чтоб гарантировать, что у processed оредров никто amount менять не будет.
Без типов — придется просматривать руками все вызовы change_amount по всему проекту и пытаться понять, где у нас processed, где не processed, а где рыбу заворачивали.
Здравствуйте, Mamut, Вы писали:
A>>Думаю, что выражать через типы имеет смысл только достаточно стабильную часть логики, т.к. изменение типов может быть болезненной процедурой и затрагивать кучу мест в проекте.
M>Ой, как это? Мне тут рядом говорили, что придется менять не в 1024 местах, а только в одном месте
менять тип — да, в одном месте. Но код, не соответствующий изменившейся системе типов, возможно, придется менять в 1024 местах.
Фишка в том, что компилятор не даст схалтурить и пропустить какие-то места.
J>Без типов — придется просматривать руками все вызовы change_amount по всему проекту и пытаться понять, где у нас processed, где не processed, а где рыбу заворачивали.
Что мешает вставить ровно одну проверку на is_processed собственно в change_amount? Тем более, что везде, где «заворачивали рыбу» известно, что смена суммы может и не пройти.
Здравствуйте, Mamut, Вы писали:
M>С какого перепугу? Тайпчек — это проверка, что все типы сходятся. К логическим ошибкам он не имеет никакого отношения.
Нет, вот здесь у тебя ошибка в рассуждениях.
Тайпчек — это не проверка, что все типы сходятся (что бы это словосочетание ни означало).
Это проверка, что код соответствует типам.
Т.е. когда тайпчек заворачивает код sin("asd") — это не потому что типы не сходятся (теоретическая тарабарщина), а потому, что нельзя брать синус от строки (требование предметной области).
Брать синус от строки — это именно логическая ошибка (а вот какой-нть JS наверняка такой код пропустит и не поперхнется даже в рантайме, если вдруг нам повезло и строка у нас содержит символ нуля).
ЗЫ А теперь поставь вместо синуса и строки свои операции и ордера в разных состояниях.
J>>Без типов — придется просматривать руками все вызовы change_amount по всему проекту и пытаться понять, где у нас processed, где не processed, а где рыбу заворачивали.
M>Что мешает вставить ровно одну проверку на is_processed собственно в change_amount?
Зависит от того, что тебе нужно. Можно, конечно, все требования исключениями гарантировать. Нехай юзер пишет письма в суппорт с стек-дампами — типа "я тут кнопочку нажал, а оно мне вот, на три экрана" Тоже вариант.
M>Тем более, что везде, где «заворачивали рыбу» известно, что смена суммы может и не пройти.
Я не сомневаюсь в твоей способности загрузить меня деталями твоей программы.
J>Тайпчек — это не проверка, что все типы сходятся (что бы это словосочетание ни означало). J>Это проверка, что код соответствует типам.
ну это я имел в виду
J>Т.е. когда тайпчек заворачивает код sin("asd") — это не потому что типы не сходятся (теоретическая тарабарщина), а потому, что нельзя брать синус от строки (требование предметной области).
J>Брать синус от строки — это именно логическая ошибка (а вот какой-нть JS наверняка такой код пропустит и не поперхнется даже в рантайме, если вдруг нам повезло и строка у нас содержит символ нуля).
Охо-хо. Логическая ошибка — это когда ты считаешь пеню в размере 50% от стоимости товара, а не 0.5%. Логическая ошибка — это когда позволяешь поднимать сумму в заказе выше определенной суммы, забыв проверить одно из условий.
А не передача строки в вызов, который требует число.
J>ЗЫ А теперь поставь вместо синуса и строки свои операции и ордера в разных состояниях.
M>>Что мешает вставить ровно одну проверку на is_processed собственно в change_amount? J>Зависит от того, что тебе нужно. Можно, конечно, все требования исключениями гарантировать. Нехай юзер пишет письма в суппорт с стек-дампами — типа "я тут кнопочку нажал, а оно мне вот, на три экрана" Тоже вариант.
О да. Ведь всатвить проверку в одно место — а именно собственно в реализацию API-вызова — это именно генерировать все исключениями и возвращать пользователю именно стек-дампы
Вот с какого-то перепугу у нас пользователю ни одного стек-дампа не возвращается, все проверки происходят внутри одного API-вызова, но при этоя язык динамический. Невозможная магия, видать
M>>Тем более, что везде, где «заворачивали рыбу» известно, что смена суммы может и не пройти. J>Я не сомневаюсь в твоей способности загрузить меня деталями твоей программы.
Я не гружу тебя деталями своей программы. Это ты выставляешь какие-то идиотские требования к коду, типа «не, ну проверять is_processed надо же везде, где вызывается change_amount»
Здравствуйте, jazzer, Вы писали:
J> Если раньше с processed order можно было делать все, что угодно, а потом вдруг "концепция поменялась" и amount у него больше менять нельзя — достаточно отразить это в определении типа,
Вот это все настолько красиво звучит, что было бы здорово увидеть пример, как запросто отразить это в определении типа. А то пока что в моем понимании это будет "переколбасить всю систему типов и огрести по полной".
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Re[34]: Haskell нужен! (в Standard Chartered Bank)
Здравствуйте, genre, Вы писали:
G>Здравствуйте, jazzer, Вы писали:
J>> Если раньше с processed order можно было делать все, что угодно, а потом вдруг "концепция поменялась" и amount у него больше менять нельзя — достаточно отразить это в определении типа,
G>Вот это все настолько красиво звучит, что было бы здорово увидеть пример, как запросто отразить это в определении типа. А то пока что в моем понимании это будет "переколбасить всю систему типов и огрести по полной".
Ну да, огрести по полной, именно так, от компилятора, ты все правильно понял.
Здравствуйте, Mamut, Вы писали:
M>>>Что мешает вставить ровно одну проверку на is_processed собственно в change_amount? J>>Зависит от того, что тебе нужно. Можно, конечно, все требования исключениями гарантировать. Нехай юзер пишет письма в суппорт с стек-дампами — типа "я тут кнопочку нажал, а оно мне вот, на три экрана" Тоже вариант.
M>О да. Ведь всатвить проверку в одно место — а именно собственно в реализацию API-вызова — это именно генерировать все исключениями и возвращать пользователю именно стек-дампы
Так ведь дело-то в том, что проверку-то ты вставишь, а дальше-то что делать будешь с результатом этой проверки?
т.е. вот у тебя было
Order::change_amount(new_value) {
value = new_value;
}
и теперь ты "вставляешь ровно одну проверку":
Order::change_amount(new_value) {
check(is_processed); //????
value = new_value;
}
что в check должно происходить? исключение? ведь надо же как-то наверх сообщить, что облом?
Или ты вставляешь ее так:
Order::change_amount(new_value) {
if (is_processed)
value = new_value;
else//????
}
что у нас в else? Ничего? Или возврат кода ошибки, типа удалось или нет изменить?
bool Order::change_amount(new_value) {
if (!is_processed) return false;
value = new_value;
return true;
}
Ну так это те же исключения, вид сбоку.
Плюс на is_processed еще много чего может быть завязано. Например, в каком виде показывать ордер — задизейбленной формой, в которой уже ничего нельзя менять, или нормальной, где менять все можно. Или дизейблить надо не всю форму, а только поле amount и кнопку, которая зовет change_amount — чтоб нельзя было ее позвать дял такого ордера.
Т.е. в идеале хотелось бы иметь код, в котором для processed ордеров просто-напросто нет вызовов change_amount — потому что они бессмысленны для таких ордеров (ну примерно как синус для строки).
Здравствуйте, Mamut, Вы писали:
J>>Без типов — придется просматривать руками все вызовы change_amount по всему проекту и пытаться понять, где у нас processed, где не processed, а где рыбу заворачивали. M>Что мешает вставить ровно одну проверку на is_processed собственно в change_amount? Тем более, что везде, где «заворачивали рыбу» известно, что смена суммы может и не пройти.
Так ты определись какие preconditions у change_amount.
Если необходимость is_processed == true входит в предусловия, то любое его нарушение это баг в программе. Если такой баг обнаружен runtime check'ом, то нужно клеить ласты ASAP.
Отражение состояния processed в типе, позволит гарантировать отсутствие такого бага в работающей программе. В то время как если проверка происходит в runtime, то даже 100% покрытие строк кода unit-тестами не даст такую гарантию (в более менее сложной программе).
Если же такого предусловия нет, и есть постусловие вида "может изменить, а может и нет" — то непонятно зачем сюда пытаться впихнуть статические проверки.
Здравствуйте, Mamut, Вы писали:
M>>>Действительно. Давай сделаем тип UnprocessedNonPrePaidRiskClearedOrder, ProcessedNonPrePaidRiskClearedOrder, UnprocessedPrePaidRiskClearedOrder, ProcessedPrePaidRiskClearedOrder и еще два десякта таких же. Это же так удобно! DM>>Ну, если ты пишешь на Си или Го, то такая беда, да. В нормальных же языках полиморфизм позволит общие вещи описать лишь однажды, а разницу вынести, так что ненужного повторения много не будет. M>«В нормальных языках», «полиморфизм». Ну можно на примере, а?
Не нужно вручную создавать тип с каждой комбинацией состояний, достаточно чего-то типа:
template<bool processed, Payment payment>
struct order {};
using processed_and_prepaid = order<true, Payment::prepaid>;
using unprocessed_and_paid = order<false, Payment::paid>;
// ...
order<true, Payment::prepaid> и order<false, Payment::paid> это разные типы, хотя шаблон типа описывается один раз.
Re[37]: Haskell нужен! (в Standard Chartered Bank)
J>что в check должно происходить? исключение? ведь надо же как-то наверх сообщить, что облом?
О ужас. Это же такая нерешенная никем задача!
J>Ну так это те же исключения, вид сбоку.
J>Т.е. в идеале хотелось бы иметь код, в котором для processed ордеров просто-напросто нет вызовов change_amount — потому что они бессмысленны для таких ордеров (ну примерно как синус для строки).
Действительно. Который, наверное, просто тихо фейлится, не сообщая никому о том, что amount не изменился по какой-то никому не известной причине
J>>>Без типов — придется просматривать руками все вызовы change_amount по всему проекту и пытаться понять, где у нас processed, где не processed, а где рыбу заворачивали. M>>Что мешает вставить ровно одну проверку на is_processed собственно в change_amount? Тем более, что везде, где «заворачивали рыбу» известно, что смена суммы может и не пройти.
EP>Так ты определись какие preconditions у change_amount.
ЧТо значит pre_conditions? У нас есть условия, при которых мы можем изменить сумму заказа.
EP>Отражение состояния processed в типе, позволит гарантировать отсутствие такого бага в работающей программе. В то время как если проверка происходит в runtime, то даже 100% покрытие строк кода unit-тестами не даст такую гарантию (в более менее сложной программе). EP>Если же такого предусловия нет, и есть постусловие вида "может изменить, а может и нет" — то непонятно зачем сюда пытаться впихнуть статические проверки.
Я не знаю, что такое предусловия, постусловия и прочая. У нас есть условия, при которых мы можем изменить сумму заказа. Мне тут рассказывают, как все прекрасно можно решить типами. Показывают, как «можно решить», только все эти примеры валятся, как карточные домики, при простейшем рассмотрении
order<true, Payment::prepaid> и order<false, Payment::paid> это разные типы, хотя шаблон типа описывается один раз. M>И как это дальше использовать. Ну, в реальной жизни, где идет несколько проверок подряд.
Каких проверок? На processed и на payment? Например показать что функция работает только с processed и prepaid:
void foo(order<true, Payment::prepaid> x)
{
// use x
}
Если нужно обработать другие варианты — добавляются соответствующие перегрузки.
Начиная с "все спецификации ad-hoc" из оригинального сообщения и до последнего тикета, который таки позволяет увеличивать сумму заказа для pre-paid закаов согласно конфигурации магазина. И это связано с дополнительной логикой — что, если 
