Бананы на розовых кустах

Когда я только разбирался с бананами, линзами и т.д. задача описания катаморфизма для розы:

data Rose a = Rose a [Rose a]

вызывала у меня большое затруднение.

( Read more... )

Бананы, сорок лет одни бананы...

К чему я так подробно расписывал получение свёртки для розы? Очевидно, что интуитивно получить её можно сразу. Так я обычно и делаю, воспользовавшись методом размерностей, пардон, программированием "от типов". Возможно, так делаете и вы. Я хочу показать главный недостаток этого подхода - он неформален.

( Read more... )

В данном конкретном случае нам очень сильно помогает Curry-Howard, но он не гарантирует уникальности доказательства (реализации), т.е. этот метод не формализуем. А вот на основе ТК, думаю, можно построить CataEval.