Арифметика с контролем диапазонов в Haskell с помощью Type-Level Literals

[Terranz]

а если нам надо написать что-то сложнее чем вычисление факториала?
например чем это поможет если мы будем писать электронный документооборот?
сайт?
игру?
web браузер?
rss агрегатор?

[danslapman]

Про факториал — слишком толсто)
Я, честно говоря, не представляю, как можно не видеть полезности проверки диапазонов значений.

[KolodeznyDiver]

Никаких сложностей в написании больших приложений на функциональных языках, и, в частности на Haskell, нет. И приложения большие есть.
Я думаю, Вы догадываетесь, что подобные вопросы не новы.
Относительно малая распространённость Haskell объясняется так называемым «большим порогом вхождения в язык». Т.е. нужно достаточно много из Haskell выучить прежде чем писать программы сложнее вычисления факториала. Зато потом пишется и отлаживается быстрее.

[Terranz]

вы воду то не лейте, на вопросы ответьте, пожалуйста

[danslapman]

Это не вопросы, а скорее вброс

[VoidEx]

Компилятор Си — достаточно сложная штука?

The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness — the fact that the generated assembly code is semantically equivalent to its source program — was entirely proved within the Coq proof assistant

[Terranz]

нет, не сложная, что там сложного то?
судя по википедии, компилятор Си не написал только ленивый en.wikipedia.org/wiki/List_of_compilers#C_compilers

[VoidEx]

Ну сложнее вычисления факториала хотя бы?

[shock_one]

Надеюсь, автор меня простит за то, что я отвечу за него. Bounded arithmetic — идея достаточно общего назначения. К сожалению, в этом решении все константы должны быть известны на этапе компиляции, что сужает область применения. Но все же количество месяцев никогда не должно быть больше, чем 12, HTTP статус должен быть между 100 и 799, а количество пользователей в бесплатной версии вашего чата должно быть до десяти.

[KolodeznyDiver]

К сожалению, в этом решении все константы должны быть известны на этапе компиляции, что сужает область применения.

Именно так и задумано.
Бывает, что границы известны заранее и это уменьшает затраты на хранение переменных границ.
Когда границы меняются динамически — см. вариант 1 в статье. Плюс контроль границ массивов и других контейнерных типов уже реализованный библиотечно.

[Bodigrim]

Про остальные сферы — не специалист, но с сайтами никаких проблем нет. Есть, например, Yesod — фреймворк на Haskell, сравнимый по уровню с Ruby on Rails. Для сайтов попроще есть тоже масса решений. Я сейчас перевожу backend нескольких проектов, написанных на PHP, на Haskell (Happstack) — сплошное удовольствие от надежности и скорости.

[chemistmail]

сайт: www.fpcomplete.com
игра: steamcommunity.com/sharedfiles/filedetails/?id=107105028
браузер: github.com/k0ral/hbro
и еще тут можно посмотреть реализацию простого браузера: hrothen.github.io/2014/09/05/lets-build-a-browser-engine-in-haskell/
rss агрегатор: bazqux.com
он же сайт

[chemistmail]

еще игры под андроид: keera.co.uk/blog/

Еще вопросы?

[Terranz]

мой вопрос перечитайте, пожалуйста
потом вслух, потом ответьте на него, если не сложно

[shock_one]

Я вам поставил минус в карму потому, что вы неуважительно относитесь к людям.

[Terranz]

ну что-ж поделать, если человек не умеет читать, надо ему помочь в этом

[vshabanov]

Как разработчик rss агрегатора на хаскеле скажу, что type level числа не использовал. Но использовал type classes и type families. Хотя и то другое всего в паре мест.

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

Но в более специфических задачах это может быть очень полезно. Например, при разработке компилятора GADT-ы использовались в полный рост. Когда я возился со всякими физическими вычислениями даже делал type level физические величины и было очень удобно.

В целом, type level вычисления действительно нужны не во всех задачах (а узнав, насколько они более удобно делаются в Agda/Coq делать их в хаскелле уже не хочется). Но иногда они действительно удобны и помогают сократить число ошибок, объем кода и работы по тестированию. И лучше иметь такую возможность, чем не иметь.

[Vitter]

www.youtube.com/watch?v=rhWMhTjQzsU
Тут хорошо описано чем полезны зависимые типы

[shock_one]

Не уверен зачем нам Num'. У меня работает и ab 14 + 7, ведь у нас есть fromInteger для RgVld.
И еще, вы пишете, что для newtype runtime overhead меньше. Разве он не отсутствует совсем?

[KolodeznyDiver]

ну, что считать совсем. Столько же, как и для типа a.
Насчёт Num' — согласен, перемудрил.

[shock_one]

Ну да, overhead N a по сравнению c а отсутствует. Понятно, что быстрее, чем a не станет.

[KolodeznyDiver]

Насчёт, того что с Num' перемудрил — это я зря.

*RangeValidation> ab 4 + 0
*** Exception: out of range [1 .. 20], value 0 in fromInteger
*RangeValidation> ab 4 +. (0::Int)
4
*RangeValidation> 

[shock_one]

Да, действительно. Но если не пользоваться функциями из Num, зачем нам этот instance? Только для того, чтобы создавать значения без конструктора?

[KolodeznyDiver]

Допустим, диапазон задан 10… 20, а нужно добавить 1 к текущему номеру. 1 не в диапазоне, так что получится только через (+.). При этом контроль выхода результата за диапазон сохраняется. А сам Num нужен, см. пример с топливом.

[shock_one]

Вы ведь слышали о dependent types, правда? Они предоставляют большую гарантию: программа с неправильный диапазоном не скомпилируется.

Классический пример — функция head. В Haskell она неполная — если передать пустой список, получим runtime exception. В Idris же (который как Haskell, но с dependent types), тип этой функции можно прочитать как «список, у которого по крайней мере один элемент».

[KolodeznyDiver]

В Haskell не обязательно использовать head. можно take 1 или Safe.headMay или Safe.headDef.
Да, даже Type-Level Literals предназначены, на самом деле, в первую очередь для compile-time контроля, этого самого dependent types dev.stephendiehl.com/hask/#typelevel-numbers. Это я их (и не только я) «нетрадиционно» использую.

с Idris не знаком.

[Vitter]

Такой переход от синглтонов к зависимым типам в языке, который не поддерживает зависимые типы

[shock_one]

Вы уверены, что это можно назвать зависимыми типами? Ведь тип не зависит от значения, а просто содержит некие константы. Вот если бы можно было, скажем, изменить верхний лимит в процессе выполнения меняя значение, тогда да.