От перемены мест слагаемых тип суммы удивляет вас

[deni_ok]

В Агде есть полезный зависимый тип данных - финитные натуральные.

Comments

[thedeemon]

Дык надо на определение функции сложения смотреть, так просто гадать нет смысла.

Оффтоп: я тут почитал про идрис, это оказывается детище автора Epic (бэкэнда для Эпиграма, Агды и Идриса). Выглядит как более хаскелизированная агда, когда пишесь себе в ascii текст, даешь компилятору и получаешь бинарник. Безо всяких емаксов и безумных юникодов. Есть и repl, есть и интерактивное доказательство теорем, есть тактики а-ля coq. Плюс спец.средства для создания DSL - простое описание новых синтаксических конструкций, возможность переопределить базовые операции (абстракцию и применение в первую очередь), idiom brackets (компрехеншоны для аппликативных функторов). В общем, попробую поставить, в винде это может быть чуточку сложнее.

[deni_ok]

А интерактивное доказательство - в repl'е?

[thedeemon]

ага, там специальный режим для него.

[deni_ok]

да, я надеюсь, что ты расскажешь нам об установке Идриса на винду.

[thedeemon]

Ну точно, Fin 9 и Fin 8 соответственно, видимо. Гипотеза такая у меня была, но уверенности не было.

[sassa_nf]

а какой в этом кроется смысл? (что мы можем умозаключить из разницы типов? чем не-эквивалентность аукнется?)

[dima_starosud]

Вообще то так не честно :)
Нужно же было тип функции показать (http://www.cse.chalmers.se/~nad/listings/lib-0.6/Data.Fin.html#3366).