Ну как бы это очевидно должно быть

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

На этом уровне newtype Set, что выше не отличается от containers:Set

ну контракт, ассюм :) Ладно, Хаскель же не прувебл язык, что вы в самом деле

У них одинаковый уровень безопасности, это инварианты прописанные в документации к API и тесты

Можно сделать структуру, которая гарантирует определенные свойства, она более безопасна будет, но как правило более тормозная

Или сильно более сложная в реализации

у меня начальник после неуспешного пропихивания LiquidHaskell начинает подкаты с Идрисом. С coq-ом тоже не прошло, мда :) Вот я как прагматичный программер не понимаю зачем бы я хотел прувать код

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

список с какими-то функциями может давать гарантии, но мы не можем быть уверены в этом, потому что кто-то мог и другую функцию вызвать, не из этого списка функций

дерево с какими-то функциями может давать гарантии и еще и давать эффективность

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

можем быть уверены пока верим что либа реализована коррентно

точно так же как можем быть уверены в пруфе на идрисе, пока верим что тайпчек идриса реализован корректно

ну вот пишешь ты маленький стартапчик, а инвестор спрашивает: как проверить, что за все оказанные услуги взяты деньги?

тест-план. QA отдел. Идрис их не аннулирует никогда. А если они есть, зачем он нужен? :) И потом, инвестор понимает что такое начальник QA отдела - его прув весомее прува какого-то Идриса, о котором инвестор не слыхивал. А QA будет тестить, а не прувать. Двойная работа ИМХО.

QA теоретически может и прувать, а не тестить

а уж мне как программисту еще менее выгодно прувать, если у меня много багов - это хорошо, мне за их фиксинг будут платить. Я уже проходил такое, когда у тебя все перфектно и твой проект закрывают, а вас реорганизируют. Лучше уж пусть будут баги, а я буду нужен и получать ЗП по коммитам :)

на написание проекта с багами, а потом фикс всех багов может уйти меньше времени, чем на написание проекта с прувами, значит и денег будет меньше)

вообще говорят, есть такая должность - прув инженер или типа того.

определением типа не гарантирует, определением функций гарантирует или нет, зависит от того, можно ли считать что когерентность инстансов гарантирована

2008 vector* (ио так и не появилось)
2009 iteratee
2010 enumerator
2011 conduit
2012 pipes, machines
2013 io-streams, foldl* (ио в turtle в 2016)
2014
2015 streaming
2016 turtle Bytes
2017 streamly

есть еще potoki

Иронично, на https://hackage.haskell.org/package/haddock-api совсем нет доков

Доброго здоровья всем!