M>>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять и дебажить логику в типах? N>Проверка типов эквивалентна доказательству правильности. Дебажить вообще не нужно, если можно формально доказать правильность.
О. Опять много умных слов ни о чем.
N>Другое дело, что система типов должна покрывать всю верифицируемую логику, что при существующих инструментах для большинства приложений слишком затратно.
Ну то есть в реальной жизни, особенно там, где, цитирую
Often working from verbal, ad hoc evolving spec. And at best from informal functional specs.
этой верификации не будет никогда.
Так что остается вопрос: как господа-апологеты типов, заявляющие, что «проверка типов эквивалентна доказательству правильности» решают проблему неправильно реализованной логики на типах.
M>>- Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты? N>Сайд-эффекты легко типизируются, см монады. Проблема опять же в слабых средствах, но работы ведутся.
Опять сказки и истории.
То есть, резюмируя:
— как вы дебажите типы? — Не, их дебажить не надо... при выполнении одного сложного и на практике почти нигде не реализуемого условия....
— как вы переносите в типы логику, зависящую от сайд эффектов? — Не, ну ты монады посмотри... хотя средства слабые...
Здравствуйте, Mamut, Вы писали:
M>Могу повторить вопрос. Простейшие же. M>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять
Compile-time unit-тестами — static_assert'ы на типы-результаты (click); автоматическая проверка того, что неправильный код действительно не компилируется и vice versa (click
Например отладочным выводом промежуточных типов.
M>- Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты?
При желании всё возможно. Например: сортировка runtime-данных через мемоизацию результатов сравнения в compile-time графе-типе (click
). То есть запихнуть много runtime данных (упомянутые тобой конфигурации и т.п.) в тип возможно, но это чревато generated code bloat.
Пытаться же запихнуть всю-всю логику в типы — контрпродуктивно, само собой нужен баланс. Как уже неоднократно отмечали выше — типы помогают обнаруживать только некоторые классы ошибок.
Неплохим примером является кодирование единиц измерения и размерности в тип. Например Mars Climate Orbiter распался в атмосфере Марса из-за того, что разные модули по ошибке использовали разные единицы измерения.
Здравствуйте, Mamut, Вы писали:
M>Often working from verbal, ad hoc evolving spec. And at best from informal functional specs. M>этой верификации не будет никогда.
Это вообще другая проблема. Формализация "informal functional specs" это из области AI. Система типов тут не поможет.
M>Так что остается вопрос: как господа-апологеты типов, заявляющие, что «проверка типов эквивалентна доказательству правильности» решают проблему неправильно реализованной логики на типах.
Никак. Если понятия "правильно" нет, то и проблемы нет.
M>- как вы дебажите типы? — Не, их дебажить не надо... при выполнении одного сложного и на практике почти нигде не реализуемого условия....
Если нужна полная верификация, то да. Частичная есть почти везде и весьма полезна, например отсутствием необходимостью писать тесты (ака "дебажить") фиксации типов, инициализацию или проверки границ.
Re[15]: Haskell нужен! (в Standard Chartered Bank)
M>>Могу повторить вопрос. Простейшие же. M>>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять
EP>Compile-time unit-тестами — static_assert'ы на типы-результаты (click); автоматическая проверка того, что неправильный код действительно не компилируется и vice versa (click
M>>и дебажить логику в типах? EP>Например отладочным выводом промежуточных типов.
Ну то есть, по сути, ничем не отличается просто от отладочного вывода в программе, так?
M>>- Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты?
EP>При желании всё возможно. Например: сортировка runtime-данных, через мемоизацию в compile-time графе (click
). То есть запихнуть много runtime данных (упомянутые тобой конфигурации и т.п.) в тип возможно, но это чревато generated code bloat.
Мемоизация — это тоже не ново, и используется много где. Понятно, что все ненамемоизируешь
EP>Пытаться же запихнуть всю-всю логику в типы — контрпродуктивно, само собой нужен баланс. Как уже неоднократно отмечали выше — типы помогают обнаруживать только некоторые классы ошибок.
Ну, я именно про это изначально и говорил. Тут мне только начали заливать баки, что типами можно практически все — от сложной логики
Ты пока единственный, кто ответил по существу вопроса
EP>Неплохим примером является кодирование единиц измерения и размерности в тип. Например Mars Climate Orbiter распался в атмосфере Марса из-за того, что разные модули по ошибке использовали разные единицы измерения.
Размерность в типе — тоже не ново. Даже в динамических языках такие вещи стараются делать в виде всяких tagged values.
Здравствуйте, novitk, Вы писали:
N>Это вообще другая проблема. N>Никак. Если понятия "правильно" нет, то и проблемы нет. N>Если нужна полная верификация, то да. Частичная есть почти везде и весьма полезна, например отсутствием необходимостью писать тесты (ака "дебажить") фиксации типов, инициализацию или проверки границ.
Сказки про супермегатипы, которые позволят и сложную логику абсолютно правильно реализовать, и сайд-эффекты описать оказались только сказками, потому что «вообще другая проблема» и «никак».
А «фиксация типов, инициализация и проверки границ» — это достаточно маленький класс проблем.
Здравствуйте, Mamut, Вы писали:
M>А «фиксация типов, инициализация и проверки границ» — это достаточно маленький класс проблем.
"Маленький" это оценочно. К примеру я работая в системе/банке конкурирующей с Мю/SC предпочел бы слезть с динамики, но нирваны конечно не будет.
M>>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять
EP>Compile-time unit-тестами — static_assert'ы на типы-результаты (click); автоматическая проверка того, что неправильный код действительно не компилируется и vice versa (click
Кстати, о юнит-тестах. Программисты – ленивые скотины, которые реализуют минимально рабочий минимум, и тесты у них такие же. В итоге все падает из-за того, что не обработан какой-нибудь пограничный случай.
M>>А «фиксация типов, инициализация и проверки границ» — это достаточно маленький класс проблем. N>"Маленький" это оценочно. К примеру я работая в системе/банке конкурирующей с Мю/SC предпочел бы слезть с динамики, но нирваны конечно не будет.
ну, у нас Erlang. Как я говорил уже, ошибка типа недавно была первая за год. Именно баги вылазят в логике: типа «забыли отослать письмо», «при переходе заказа из состяния X в состяние Y для системы Z в Германии неправильно высчитывается процент, начисляемый пользователю» и т.п.
Был случай, когда нескольким тысячам заказов был выставлен неверный статус из-за неправильной конфигурации (скажем, вместо 14 дней было поставлено 7 дней).
Как это все можно отловить типами, как мне тут некоторые сказочники рассказывают? Да никак.
Здравствуйте, Mamut, Вы писали:
M>>>Могу повторить вопрос. Простейшие же. M>>>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять EP>>Compile-time unit-тестами — static_assert'ы на типы-результаты (click); автоматическая проверка того, что неправильный код действительно не компилируется и vice versa (click
На новизну и не претендую — просто одно из средств тестирования "логики на типах".
M>>>и дебажить логику в типах? EP>>Например отладочным выводом промежуточных типов. M>Ну то есть, по сути, ничем не отличается просто от отладочного вывода в программе, так?
Да, простой отладочный вывод, только часто выводит не сама программа, а компилятор, без запуска программы.
Итого: юнит-тесты "логики на типах" есть, отладочный вывод есть. Этого вполне достаточно.
Бывают даже интерактивные оболочки:
M>>>- Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты? EP>>При желании всё возможно. Например: сортировка runtime-данных, через мемоизацию в compile-time графе (click
). То есть запихнуть много runtime данных (упомянутые тобой конфигурации и т.п.) в тип возможно, но это чревато generated code bloat. M>Мемоизация — это тоже не ново, и используется много где. Понятно, что все ненамемоизируешь
На новизну не претендую. Но всё же подчеркну, что здесь мемоизация в самом типе, а не в переменной / значении_типа.
Результирующий тип зависит от входных значений. А раз есть тип, то можно сделать какие угодно проверки и манипуляции в compile-time (хотя сам тип был получен посредством цепочки runtime-проверок).
Это я всё к тому, что какие угодно динамические конфигурации можно запихнуть в compile-time тип. Другое дело что всё упирается в цену, а-ля generated code-bloat.
EP>>Неплохим примером является кодирование единиц измерения и размерности в тип. Например Mars Climate Orbiter распался в атмосфере Марса из-за того, что разные модули по ошибке использовали разные единицы измерения. M>Размерность в типе — тоже не ново. Даже в динамических языках такие вещи стараются делать в виде всяких tagged values.
В динамических языках проблема очевидно в том, что не факт что все соответствующие проверки сработают на этапе разработки. Даже имея 100% покрытие тестами всех строчек кода — нет такой гарантии.
Здравствуйте, jazzer, Вы писали:
J>Total Haskell code base: >2M lines, >150 contributors (~20 core), >110k commits. J>Haskell code everywhere: real time pricing, risk management, data analysis, regulatory systems, desktop and web GUIs, web services, algo pricing, end-user scripting, and as plugins to C++, Java, C#, Excel. J>Windows, Linux, clusters and grids. On servers and desktops in >30 countries.Интересно.
Интересно. Я тоже работаю на один западный инвестиционный банк и у нас тоже построена (строится) примерно такая же инфраструктура с real time pricing, risk management, data analysis, regulatory systems, desktop and web GUIs, web services, algo pricing, end-user scripting, and as plugins to C++, Java, C#, Excel. Правда пока еще она меньшего размера (сколько точно строчек кода не знаю, но думаю, что до 2М еще не дотягиваем), но уже пользуется огромной популярность. И вместо Хаскела мы используем другой скриптовый язык.
И вот мне кажется, что дело здесь не в том, какой язык использовать — Хаскел, Эрланг или что-то еще. А в том, что у бизнес-пользователей подобных компания есть огромная потребность в своего рода DSL, который позволит им писать различные ad-hoc скрипты, what-if сценарии, автоматизировать задачи для больших наборов данных, получать доступ к промежуточным данным расчетов и т.д. Эти люди (аналитики, трейдеры, риск менеджеры) и раньше делали нечто подобное, но использовали для этого различные не очень удобные подручные средства, а-ля Excel таблицы с VB макросами. Появление же firm-wide DSL, которые предоставляет доступ к основным ф-циям их систем, к источникам данным, к библиотекам для финансовых расчетов, реально совершает революцию в их работе. Понятно, что они не хотят изучать С++ или Java, ставить Visual Studio и т.д. Строгий контроль типов им тоже, по большому счету, по барабану. Но вот использовать скриптовый язык для решения повседневных задач, они вполне могут и даже хотят. И чем проще, тем лучше. Чем меньше будет синтаксических наворотов, тем лучше.
Так что я бы переформулировал заголовок не как "Haskell нужен", а как "DSL нужен".
Здравствуйте, Джеффри, Вы писали:
Д>Так что я бы переформулировал заголовок не как "Haskell нужен", а как "DSL нужен".
ИМХО внешний большой DSL на нативной платформе, как Мю, не нужен. Делать отладчик, профайлер, среду, библиотеки/биндинги на каждый чих это очень и очень дорого. Гораздо выгодней взять Питон/Скалу/F# и прикрутить к ним удобную db, реактивность, мемоизацию и CI. Трейдеры и риск менеджеры копаться в коде все равно не будут, но если сделать удобно есть надежда понравиться квантам.
Здравствуйте, novitk, Вы писали:
N>ИМХО внешний большой DSL на нативной платформе, как Мю, не нужен. Делать отладчик, профайлер, среду, библиотеки/биндинги на каждый чих это очень и очень дорого. Гораздо выгодней взять Питон/Скалу/F# и прикрутить к ним удобную db, реактивность, мемоизацию и CI. Трейдеры и риск менеджеры копаться в коде все равно не будут, но если сделать удобно есть надежда понравиться квантам.
Да, я согласен, это может быть и не полноценный DSL со своим синтаксисом, компилятором и т.д. Главное, что с точки зрения конечного пользователя, это выглядит как DSL. То есть язык, который позволяет ему манипулировать объектами из его предметной области. Минимум — IT-шных штучек, максимум — бизнес-логики.
Что мы сделали — взяли простой скриптовый язык, написали к нему библиотеку с ф-циями специфичными для нашей системы и понятными для пользователей (типа, create_trade, price_trade, add_to_portfolio и т.д.), а также добавили доступ к базе данных. По сути это все — среда и сама библиотека ставится одной MSI-кой, язык сам по себе примитивный, достаточно пары примеров и пользователь уже начинает использовать его сначала в режиме командной строки, а потом и писать свои скрипты. Со временем добавили доступ к другим системам и источникам данных, интеграцию с Excel и т.д.
Самое интересно, что как раз риск менеджеры и трейдеры с огромным энтузиазмом взялись копаться в коде и писать свои скрипты. Кванты в основном задействованы для написания библиотечных ф-ций. А уже комбинируют эти ф-ции в единое целое, как строительные блоки, сами конечные пользователи.
Re[20]: Haskell нужен! (в Standard Chartered Bank)
Здравствуйте, Mamut, Вы писали:
M>Как это все можно отловить типами, как мне тут некоторые сказочники рассказывают? Да никак.
Ты завязывай с ветряными мельницами-то. Кто тебе тут обещал "это все отловить"?
Клапауций говорил "некоторые классы ваших логических ошибок".
Я изначально написал "смещение этой границы, чтобы как можно больше логики кодировать в типах", т.е. не всю, а сколько получится.
Re[21]: Haskell нужен! (в Standard Chartered Bank)
M>>Как это все можно отловить типами, как мне тут некоторые сказочники рассказывают? Да никак.
DM>Ты завязывай с ветряными мельницами-то. Кто тебе тут обещал "это все отловить"?
Ну как. Тот же Клапауций тут вещает про «перенести все в инициализаторы», а novitik расскзаывает, как сайд-эффекты типизируются монадами
DM>Клапауций говорил "некоторые классы ваших логических ошибок". DM>Я изначально написал "смещение этой границы, чтобы как можно больше логики кодировать в типах", т.е. не всю, а сколько получится.
Ну. Сколько логики ты перенесешь в типы, и как это будет проверяться и дебажиться?
ЗЫ. Это уже какое? пятнадцатое сообщение на тему? и до сих пор ни одного внятного ответа. Ни одного даже мало-мальски внятного примера.
Ну вот вам простейший пример простейшей логики:
- Есть заказ.
- Пока заказ не помечен, как отправленный, можно уменьшать и увеличивать сумму заказа
- Величина, на которую можно увеличить сумму заказа, зависит от:
- Страны, в которой сделан заказ по конфигурируемому умолчанию
- для Германии:
- уменьшить можно на max(10% от оригинальной суммы заказа, 10 евро)
- увеличить можно на max(10% от оригинальной суммы заказа, 10 евро)
- Магазина, в котором сделан заказ
- если конфигурации для магазина нет, берутся умолчания для страны магазина
- если заказ помечен, как pre-paid, увеличивать сумму нельзя, уменьшать можно
- уже есть тикет, который позволяет увеличивать сумму заказа для pre-paid
заказов в зависимости от конфигурации магазина
Просто же. Как можно больше логики можно на типах запрограммировать же.
Спасибо. Это все равно возвращает к изначальным:
— кто и как будет проверять, правильно ли реализована логика в этих типах
— не впихивать же 40 условий, половина из которых зависит от конфигураций, в эти инициализаторы
Здравствуйте, Mamut, Вы писали:
M>Спасибо. Это все равно возвращает к изначальным: M>- кто и как будет проверять, правильно ли реализована логика в этих типах M>- не впихивать же 40 условий, половина из которых зависит от конфигураций, в эти инициализаторы
1. так же как и раньше, просто некоторая часть ошибок найдется компилятором, а не тестером. те этот механизм ничего конечно не гарантирует, кроме того, что какой-то процент ошибок найдется раньше. так же см пункт 2.
2. ну вот поэтому я и не любитель таких методик, практика показывает, что гораздо быстрее найдется вылетевший NPE, чем ты озверев впихнешь всю бизнес-логику в систему типов. БОлее того, если уж ошибка проскочит компилятор, то найти ее будет сложнее, чем банальный NPE в примере с билдером.
Но принципиально такая возможность существует. Может быть можно даже извернуться и придумать дсл позволяющий реализовывать такие штуки гораздо менее многословно.
PS. немного подумав. и все-таки, для некоторых вещей такие техники вполне имеют смысл, например для каких-то базовых сущностей системы. Например, ордер в торговой системе инварианты которого проверяются компилятором это скорее добро, чем зло, учитывая, что модифицируется он крайне редко и можно потратить силы на систему типов один раз.
... << RSDN@Home 1.0.0 alpha 5 rev. 0>>
Re[19]: Haskell нужен! (в Standard Chartered Bank)
M>>Спасибо. Это все равно возвращает к изначальным: M>>- кто и как будет проверять, правильно ли реализована логика в этих типах M>>- не впихивать же 40 условий, половина из которых зависит от конфигураций, в эти инициализаторы
G>1. так же как и раньше,
Как? Ну то есть все те же юнит-тесты и отладочная печать? Тогда это совсем не отличается от обычной работы в любом языке программирования, даже насквозь динамическом
G>просто некоторая часть ошибок найдется компилятором, а не тестером.
Какая часть?
G>те этот механизм ничего конечно не гарантирует, кроме того, что какой-то процент ошибок найдется раньше. так же см пункт 2. G>2. ну вот поэтому я и не любитель таких методик, практика показывает, что гораздо быстрее найдется вылетевший NPE, чем ты озверев впихнешь всю бизнес-логику в систему типов. БОлее того, если уж ошибка проскочит компилятор, то найти ее будет сложнее, чем банальный NPE в примере с билдером.
:D Вот я как бы к этому веду и намекаю
G>PS. немного подумав. и все-таки, для некоторых вещей такие техники вполне имеют смысл, например для каких-то базовых сущностей системы. Например, ордер в торговой системе инварианты которого проверяются компилятором это скорее добро, чем зло, учитывая, что модифицируется он крайне редко и можно потратить силы на систему типов один раз.
У нас ордер проходит через машину состяний, достаточно сложную и разветвленную, сильно зависящую от конфигурация (по странам + по магазинам). Я сложно представляю, какой развесистый тип должен быть у заказа, чтобы «все было проверено»
M>У нас ордер проходит через машину состяний, достаточно сложную и разветвленную, сильно зависящую от конфигурация (по странам + по магазинам). Я сложно представляю, какой развесистый тип должен быть у заказа, чтобы «все было проверено»
