M>>А потом дебажить типы, когда логика закодирована неправильно K>Для типов есть легковесная верификация, в случае их отсутствия не все так радужно.
Какой-то набор слов.
M>>Действительно, ведь раз логика закодирована типами, она перестает быть логикой, ага, и никогда не может быть неверной. K>Она не перестает быть логикой, она представляется в форме, которая хорошо подходит для автоматической проверки.
Какой-такой автоматической проверки? У апологетов типов какое-то умопомрачение на типах, честное слово «Как только мы запиливаем логику в типах, она моментально становится правильной и логических ошибок там нет никогда».
Давай, я пример приведу.
Order flow:
1. Создали заказ
2. Опционально обновили заказ (добавили или убрали item'ы)
3. Если заказ expired, можно продлить expiry date
4. Пометили заказ, как отправленный [или]
пометили лишь некоторые из item'ов в заказе, как отправленные
В 1. заказ может быть создан с оплатой в рассрочку, оплаченный через pre-pay. Если через pre-pay, нужно создать запись, что ожидается оплата от банка (которая придет отдельным банковским файлом в течение недели, а то и больше).
В 2. уменьшать и увеличивать стоимость заказа можно на сумму, зависящую от страны и конфигурации конкретного магазина. Если заказ сделан в системе X, и предоплачен, то повышать сумму заказа нельзя
В 3. expiry date можно перемещать на дни, определенные конфигурацией магазина, и после энного перемещения впаивать магазину штрафы (для этого создается отдельная запись, которая потом выставляется магазину)
В 4. если заказ не предоплачен, то у пользователя начинатеся отсчет времени по рассрочке. При этом если отправлена только часть заказа, то рассрочка начинается только по части заказа, оставшиеся item'ы по сути остаются в состянии 1., и для них продолжают работать все остальные пункты, только в пункте 2. появляется дополнительнео условие: нельзя поднять сумму выше оригинальной суммы заказа (на сконфигурированные суммы) и т.п.
Как это ты все распилишь на типах? И когда распилишь, какого объема будут эти типы, и как их дебажить на предмет логических ошибок?
Ах, да. У нас сейчас задача.
Как сейчас:
1. Если оплата карточкой, мы сразу делаем authorize and capture (резервация денег и снятие со счета)
Как будет:
1. В зависимости от конфигурации магазина мы делаем или authorize and capture или только authorize
2. Если сделан только authorize, мы позволяем повышать сумму заказа даже для товаров, оплаченныз карточкой (зависит от конфигурации магазина)
3. Если заказ expired, мы должны отменить authorization в банке. Если продливается expiry date, мы должны заново сделать auth в банке
4. Если заказ помечен, как отправелнный, и в заказе сделан только auth, то мы должны в этот момент сделать capture
Как именно мне тут помогут типы, если я забуду сделать четвертый пункт?
M>>А потом дебажить типы, когда логика закодирована неправильно DM>Да, а что в этом плохого? Особенно, когда и до дебага-то не доходит, т.к. проблемы уже на стадии компиляции прояаляются.
Здравствуйте, jazzer, Вы писали:
K>>(при условии, что энергичный язык можно считать хаскелеподобным).
J>А почему нельзя? Я так понимаю, отсутствие ленивости только убивает разные бесконечные последовательности, да и то с оговорками, не?
Дело не в бесконечных структурах. Ленивость — это такая неявная "одноразовая" мутабельность. И если ее полноценной поддержки в языке нет, то нужно использовать гораздо больше явной мутабельности с понятными последствиями, особенно в чистом языке. Это означает что практически весь код будет написан на строгом языке иначе, не важно с бесконечными он структурами работает или конечными, поддержка бесконечных структур это только одно из следствий этого, как и более полезное раннее завершение и прочие вещи для которых в строгом языке придется континьюэйшенами пользоваться, что более чем сомнительное удовольствие.
См. например http://rsdn.ru/forum/decl/4519667.1
J>Остальное же все остается — правила вывода, паттерн-матчинг, частичное применение и т.п...
Хаскелеподобный язык от эмелеподобного отличается в первую очередь ленивостью и тайпклассами вместо модулей, а не паттерн-матчингом и частичным применением.
'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[10]: Haskell нужен! (в Standard Chartered Bank)
Здравствуйте, Mamut, Вы писали:
K>>Для типов есть легковесная верификация, в случае их отсутствия не все так радужно. M>Какой-то набор слов.
Что-то непонятно? Есть какие-то конкретные вопросы?
M>Какой-такой автоматической проверки?
Проверки типов.
M>У апологетов типов какое-то умопомрачение на типах, честное слово
Умопрояснение, скорее.
M> «Как только мы запиливаем логику в типах, она моментально становится правильной и логических ошибок там нет никогда».
Вы случайно запостили в ответ мне отрывок из вашего спора с соломенным человеком.
M>Как именно мне тут помогут типы, если я забуду сделать четвертый пункт?
Поможет тем, что вы можете делать описание чего-то корректным по построению, например. Т.е. сделать нежелательное состояние непредставимым в виде значения.
'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
Здравствуйте, D. Mon, Вы писали:
DM>>>Средний питонист/джаваскриптер/эрлангист может и не догадывается, что его "проблема в логике" может в другом языке быть проблемой с типами и быть поймана компилятором. Чем меньше твой язык позволяет выразить типами, тем меньше у тебя ошибок с типами и тем больше ошибок "в логике", это естественно. M>>Действительно, ведь раз логика закодирована типами, она перестает быть логикой, ага, и никогда не может быть неверной. DM>Зачем клоуна строишь? Ничего подобного я не говорил и не имел в виду.
Вы просто о разных вещах говорите.
"Проблемы в логике" могут быть разными. Могут быть эквивалентны ошибке в программе (тогда они ловятся типами), а могут быть отклонениями программы от спецификации (вместо "+" написали "-").
Re[11]: Haskell нужен! (в Standard Chartered Bank)
K>Что-то непонятно? Есть какие-то конкретные вопросы?
Да. Ты, правда, решил скипнуть мой пример с вопросом.
M>>Какой-такой автоматической проверки? K>Проверки типов.
Которая поможет мне с логическими ошибками... как?
M>>Как именно мне тут помогут типы, если я забуду сделать четвертый пункт? K>Поможет тем, что вы можете делать описание чего-то корректным по построению, например. Т.е. сделать нежелательное состояние непредставимым в виде значения.
Это какие-то общие фразы без конкретики.
Итак, повторю
Как сейчас:
1. Если оплата карточкой, мы сразу делаем authorize and capture (резервация денег и снятие со счета)
Как будет:
1. В зависимости от конфигурации магазина мы делаем или authorize and capture или только authorize
2. Если сделан только authorize, мы позволяем повышать сумму заказа даже для товаров, оплаченныз карточкой (зависит от конфигурации магазина)
3. Если заказ expired, мы должны отменить authorization в банке. Если продливается expiry date, мы должны заново сделать auth в банке
4. Если заказ помечен, как отправелнный, и в заказе сделан только auth, то мы должны в этот момент сделать capture
Как именно мне тут помогут типы, если я забуду сделать четвертый пункт?
То есть четвертый пункт — это
if is_activated(Order) and is_auth_only(Order):
do_capture(Order)
Здравствуйте, Mamut, Вы писали:
K>>Что-то непонятно? Есть какие-то конкретные вопросы? M>Да. Ты, правда, решил скипнуть мой пример с вопросом.
Т.е. этот пример был уточняющим вопросом, который поможет вам понять что я имел в виду под "легковесной верификацией"?
K>>Проверки типов. M>Которая поможет мне с логическими ошибками... как?
Так, что некоторые классы ваших логических ошибок будут приводить к ошибкам компиляции.
K>>Поможет тем, что вы можете делать описание чего-то корректным по построению, например. Т.е. сделать нежелательное состояние непредставимым в виде значения.
M>Это какие-то общие фразы без конкретики.
Ок, с конкретикой: нельзя будет сконструировать заказ с состоянием "Отправленный" и "Непроверенный как написано в 4-м пункте" одновременно, так что в случае забывания 4-го пункта будет ошибка компиляции. Ну, как нельзя забыть проверить значение типа Maybe Foo на пустоту и вызвать функцию bar заданную на Foo, потому что она на Maybe Foo не определена.
'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[13]: Haskell нужен! (в Standard Chartered Bank)
M>>Это какие-то общие фразы без конкретики.
K>Ок, с конкретикой: нельзя будет сконструировать заказ с состоянием "Отправленный" и "Непроверенный как написано в 4-м пункте" одновременно, так что в случае забывания 4-го пункта будет ошибка компиляции. Ну, как нельзя забыть проверить значение типа Maybe Foo на пустоту и вызвать функцию bar заданную на Foo, потому что она на Maybe Foo не определена.
Легко предание, да не верится вообще нифига.
Сколько условий «Непроверенный как написано в энном пункте» предлагаешь впихивать в тип?
Каким образом это поможет мне не забыть вписать в тип ошибку «Непроверенный как написано в энном пункте»? <- вот это и есть логическая ошибка, от которой все сказки про типы не спасут
Каким образом это мне поможет на этапе компиляции, если вся информация о заказе идет в рантайме (включая такие прекрасные вещи, как конфигурации десятка параметров из базы данных)?
Ты перенес все эти четыре десятка условий в типы, молодца. Как ты собираешься проверять, что ты эти условия описал в типах логически правильно?
[добавлено потом]
Это я еще умолчал о разных веселых сайд-эффектах:
— отсылать e-mail'ы разных типов при разных действиях
— в зависимости от конфигураций и того, что выбрал пользователь, отсылать бумажные письма
— дергать payments/dunning/bookkeeping за разные части в разные моменты
— вызывать risk check и производить разные действия в зависимости от результата. Не на всех этапах, естественно
— обрабатывать случаи нестандартной интеграции (в основном, для очень больших магазинов)
и еще вагон и маленькая тележка
Здравствуйте, AlexRK, Вы писали:
ARK>Вы просто о разных вещах говорите.
Мы просто разные вещи говорим. Он зачем-то додумывает за меня глупости и дописывает, будто я их написал.
ARK>"Проблемы в логике" могут быть разными. Могут быть эквивалентны ошибке в программе (тогда они ловятся типами), а могут быть отклонениями программы от спецификации (вместо "+" написали "-").
Да, могут. Я и не говорю, что проблемы исчезают и "никогда не может быть неверной". Это Мамут зачем-то говорит.
Re[14]: Haskell нужен! (в Standard Chartered Bank)
Здравствуйте, Mamut, Вы писали:
M>Сколько условий «Непроверенный как написано в энном пункте» предлагаешь впихивать в тип?
Для начала в конструктор значения этого типа.
M>Каким образом это поможет мне не забыть вписать в тип ошибку «Непроверенный как написано в энном пункте»? <- вот это и есть логическая ошибка, от которой все сказки про типы не спасут
Проектируя тип "Заказ", Вы просто описываете вашу спецификацию как конструкторы. Если в спецификации противоречия, вы даже можете их на этом этапе обнаружить. А потом тайпчекер уже заботится о том, что вы все проверяете по спецификации.
M>Каким образом это мне поможет на этапе компиляции, если вся информация о заказе идет в рантайме (включая такие прекрасные вещи, как конфигурации десятка параметров из базы данных)?
Это не является ограничением для статической проверки типов, но тут и этого не требуется.
M>Ты перенес все эти четыре десятка условий в типы, молодца. Как ты собираешься проверять, что ты эти условия описал в типах логически правильно?
Проще искать ошибки с трансляцией спецификации в тип в одном месте, чем с ее выполнением в 1024-х местах в коде.
'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[15]: Haskell нужен! (в Standard Chartered Bank)
[я там отредактировал сообщение, добавив еще немного текста]
M>>Сколько условий «Непроверенный как написано в энном пункте» предлагаешь впихивать в тип? K>Для начала в конструктор значения этого типа. K>Проектируя тип "Заказ", Вы просто описываете вашу спецификацию как конструкторы. Если в спецификации противоречия, вы даже можете их на этом этапе обнаружить. А потом тайпчекер уже заботится о том, что вы все проверяете по спецификации.
Можно больше конкретики? Я согласен на примеры кода.
M>>Ты перенес все эти четыре десятка условий в типы, молодца. Как ты собираешься проверять, что ты эти условия описал в типах логически правильно? K>Проще искать ошибки с трансляцией спецификации в тип в одном месте, чем с ее выполнением в 1024-х местах в коде.
Здравствуйте, Mamut, Вы писали:
M>>>А потом дебажить типы, когда логика закодирована неправильно DM>>Да, а что в этом плохого? Особенно, когда и до дебага-то не доходит, т.к. проблемы уже на стадии компиляции прояаляются.
M>С какого перепуга они вылезут на этапе компиляции?
C такого, что компилятор соответствие типов проверяет. Сделал SQL запрос и ввод от пользователя не строками, а разными типами, и вот уже не получается их так просто в одну строку соединить. В питонах с джаваскриптами это была бы "ошибка в логике", а тут стала ошибкой в типах.
Я не говорю, что абсолютно все проблемы выявляются любой системой статических типов. Лишь некоторые. И чем выразительней эта система и чем удачнее применяется, тем больше проблем выявляется при компиляции.
Re[11]: Haskell нужен! (в Standard Chartered Bank)
M>>С какого перепуга они вылезут на этапе компиляции? DM>C такого, что компилятор соответствие типов проверяет. Сделал SQL запрос и ввод от пользователя не строками, а разными типами, и вот уже не получается их так просто в одну строку соединить. В питонах с джаваскриптами это была бы "ошибка в логике", а тут стала ошибкой в типах.
В питонах с джаваскриптами это точно так же была бы проблема с типами, а не с логикой.
DM>Я не говорю, что абсолютно все проблемы выявляются любой системой статических типов. Лишь некоторые. И чем выразительней эта система и чем удачнее применяется, тем больше проблем выявляется при компиляции.
Пока что я про это слышу много сказок и рассказов, никто так конкретного ничего не показал. Более того, никто так и не ответил на банальный вопрос: ну перенесли логику в типы, молодцы. Кто и как будет проверять и дебажить реализацию логики в типах? Ну, весь этот real time pricing или risk management на типах.
150 контрибуторов это не означает что там столько haskell девелоперов. Хаскель девелоперов там около 10 — все перечисленны в презентации.
Все что они сделали — это просто Haskell DSL и назвали его Mu. Суть в том что в банке трейдеры или риск-аналисты пишут на Мю, это потом копилируется в C++ код и запускается. Я видел некоторые презентации когда этот haskell продвигали и в принципе на месте хаскеля тут мог стоять любой другой DSL язык — такое впечатление сложилось. Потом нужно же чем-то себя занять, они и continuous integration сервер на хаскеле написали и другие тулзы. Поинт в том что сам Хаскель это просто интсрумент, который можно заменить.
Re[12]: Haskell нужен! (в Standard Chartered Bank)
Здравствуйте, Mamut, Вы писали:
M> Более того, никто так и не ответил на банальный вопрос: ну перенесли логику в типы, молодцы. Кто и как будет проверять и дебажить реализацию логики в типах? Ну, весь этот real time pricing или risk management на типах.
Банальный вопрос имеет такой же банальный ответ. Программист будет. Как — имеющимися средствами.
Re[13]: Haskell нужен! (в Standard Chartered Bank)
M>> Более того, никто так и не ответил на банальный вопрос: ну перенесли логику в типы, молодцы. Кто и как будет проверять и дебажить реализацию логики в типах? Ну, весь этот real time pricing или risk management на типах.
DM>Банальный вопрос имеет такой же банальный ответ. Программист будет. Как — имеющимися средствами.
Можно на примере?
ЗЫ. Вот я не понимаю. Спрашиваешь вопрос про любой язык программирования — тебе и ответят, и примеры покажут, и ссылки подкинут — все, что угодно. Как только дело доходит до апологетов «типы везде, они рулят», все, тишина, одна демагогия на пять страниц ответов
МU, как я понял не хаскель, а понятный простым смертным хаскель-подобный DSL (без ленивости, монад и прочих категорий из теорий).
Попытка не нова, до этого есть/были SecDB, A+, kDB и много всего помельче. Подход имхо малоперспективен. Поддержка полностью своей экосистемы слишком дорога, лучше взять имеющиеся (питон, скалу, возможно .NET в скором будущем) и интегрироваться в нее. Естественно, если у вас есть один или несколько гуру, это может некоторое время летать, но потом они неизбежно уходят и наступает кошмар. Это сейчас понимают даже в SecDB, наиболее успешном и долгоиграющем проекте из подобных (ты же вроде в голдмане?).
Re[12]: Haskell нужен! (в Standard Chartered Bank)
Mamut,
M>>>С какого перепуга они вылезут на этапе компиляции? DM>>C такого, что компилятор соответствие типов проверяет. Сделал SQL запрос и ввод от пользователя не строками, а разными типами, и вот уже не получается их так просто в одну строку соединить. В питонах с джаваскриптами это была бы "ошибка в логике", а тут стала ошибкой в типах.
M>В питонах с джаваскриптами это точно так же была бы проблема с типами, а не с логикой.
Это если в питонах с джаваскриптами будут везде использовать разные типы для, скажем, изменяемых и неизменяемых мэпов. Тогда попытка поменять элемент у неизменяемого мэпа приведёт к рантайм-исключению. На деле же никто этого не делает, а уж строки и числа — все на одно лицо.
DM>>Я не говорю, что абсолютно все проблемы выявляются любой системой статических типов. Лишь некоторые. И чем выразительней эта система и чем удачнее применяется, тем больше проблем выявляется при компиляции.
M>Пока что я про это слышу много сказок и рассказов, никто так конкретного ничего не показал. Более того, никто так и не ответил на банальный вопрос: ну перенесли логику в типы, молодцы. Кто и как будет проверять и дебажить реализацию логики в типах? Ну, весь этот real time pricing или risk management на типах.
(Простите, не Хаскель, а пока Скала )
1. У меня есть функции, одна принимает количество миллисекунд с начала эпохи, вторая — количество миллисекунд с начала дня
Я хочу немного подкрутить гайку, и дать всем пользователям моих функций понять, что в первой я жду с начала эпохи, а во второй — с начала дня.
sealed trait Day
sealed trait Epoch
type EpochTime = Long @@ Epoch
type DayTime = Long @@ Day
def flush(moment: EpochTime) = ???
def analyze(moment: DayTime) = ???
Остаётся поработать над обёрткой вокруг "плоских" апи, и в своём приложении использовать только эти Tagged types (определение @@ искать в scalaz). Аналогично можно (и нужно) различать часы, минуты, килограммы, километры в час и так далее.
2. Известная штука — шаблон Builder — страдает одним недостатком: set-чего-то-там можно забыть сделать. Если мы хотим подкрутить гайку и здесь, то это можно сделать вполне — программа с неправильно инициализированным инстансом просто не скомпилируется:
// наш пользовательский классик, который мы хотим билдитьcase class Foo(x: Int, y: String, z: Char)
// HasBuilder[_] из библиотеки shapeless-builder
object Foo extends HasBuilder[Foo] {
// вспомогательные штука из библиотеки shapeless
val isoContainer = createIsoContainer(apply _, unapply _)
val fieldsContainer = createFieldsContainer(X :: Y :: Z :: HNil)
// параметр x обязательный
object X extends Param[Int]
// параметр Y опциональный с дефолтом "5"
object Y extends OptParam[String]("5")
// параметр Z опциональный с дефолтом '!'
object Z extends OptParam[Char]('!')
}
import Foo._
val test = Foo.builder.set(X, 42).set(Z, '+').build()
// здесь test == Foo(42,"5",'+')
// если не сделаем set(X, ...) получим ошибку компиляции
3. В базах данных часто все ключи всех таблиц — лонги, и FK-и тоже ессно лонги. Мы пишем свой Дао, и хотим раз и навсегда решить проблему сравнения несравнимых ключей. Например совершенно бессмыссленно делать сравнение между id в таблице комментов и id в таблице юзеров.
case class CommentRow(id: Option[CommentId], // Option в Slick показывает, что он автоинкрементный
text: String,
authorId: UserId,
date: DateTime)
case class UserRow(id: Option[UserId],
email: String,
firstName: String,
lastName: String)
// И потом в Дао очевидно будет ошибка компиляции, если это будет не UserId
usersDao.findById(userId)
А сколько возможностей открывается с тайпклассами — ммм... Тут как всегда — если появляются средства, появляется и необходимость. Уверен, что в Хаскеле можно то же, что выше и даже лучше. Первое так точно, там newtype из коробки. И да, я не говорю, что с момента, когда мы усилили типы, ошибки у нас исчезнут. Но типичные ошибки задавить типами — вполне можно.
M>>Пока что я про это слышу много сказок и рассказов, никто так конкретного ничего не показал. Более того, никто так и не ответил на банальный вопрос: ну перенесли логику в типы, молодцы. Кто и как будет проверять и дебажить реализацию логики в типах? Ну, весь этот real time pricing или risk management на типах.
LCR>(Простите, не Хаскель, а пока Скала )
И опять ни одного ответа на мои вопросы
Вау. Здесь есть типы, а там типы, а тут еще обертку сделали над базой данных.
ПРЕКРАСНО.
Но вопрос был не об этом.
Тут мне утверждают, что много логики можно уложить в типы, и все будет проверяться компилятором ну вот прямо-таки автоматически. Я даже примеры логики
Нет. В ответ «программист будет использовать тулзы», «пиши инициализаторы», «а вот тебе примеры, вообще с твоими вопросами несвязанные»
Хотя казалось бы: раз все настолько круто, как вы все это описываете, ведь можно внятно это объяснить и показать ну какой-нибудь простой пример, отвечающий на мой вопрос, не?
Могу повторить вопрос. Простейшие же.
— Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять и дебажить логику в типах?
— Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты?
LCR>А сколько возможностей открывается с тайпклассами — ммм... Тут как всегда — если появляются средства, появляется и необходимость. Уверен, что в Хаскеле можно то же, что выше и даже лучше. Первое так точно, там newtype из коробки. И да, я не говорю, что с момента, когда мы усилили типы, ошибки у нас исчезнут. Но типичные ошибки задавить типами — вполне можно.
«Сколько возможностей», «типичные ошибки», «задавить». Но при этом все равно нет ответов на мои простейшие вопросы
Здравствуйте, Mamut, Вы писали:
M>- Вы переносите логику из кода приложения в типы. Это не делает логику правильной, это делает логику в типах. Как вы собираетесь проверять и дебажить логику в типах?
Проверка типов эквивалентна доказательству правильности. Дебажить вообще не нужно, если можно формально доказать правильность. Другое дело, что система типов должна покрывать всю верифицируемую логику, что при существующих инструментах для большинства приложений слишком затратно.
M>- Как вы перенесете в типы логику, которая зависит от десятка разнообразных действий, включая интересные сайд-эффекты?
Сайд-эффекты легко типизируются, см монады. Проблема опять же в слабых средствах, но работы ведутся.
)
quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
