Привет. На днях я искал, как сделать что-то в Idris, и наткнулся на неплохой пост, вольный перевод которого выглядит вполне уместным. Вольности и отсебятину, где необходимо, я буду обозначать ⟦вот такими закорючками в начале и в конце⟧.
Когда стоит использовать тесты, а когда — типы? Какую информацию и какие гарантии мы получаем в обмен на наши усилия по их написанию?
Мы рассмотрим простой и немного надуманный пример, выраженный на Python, C, Haskell и Idris. Мы также увидим, что можно сказать о реализации без каких-либо дополнительных знаний о ней, в каждом из случаев.
Мы не будем учитывать разнообразные чёрные ходы, позволяющие явно нарушать гарантии языка (например, расширения C, unsafePerformIO в Haskell, небезопасные приведения типов), иначе нельзя было бы сделать вообще никаких выводов, и этот пост получился бы довольно коротким. ⟦Кроме того, у того же хаскеля есть подмножество Safe Haskell, явно и транзитивно запрещающее использование этих и ряда других трюков, могущих нарушить целостность языка.⟧
