История изменений
Исправление AndreyKl, (текущая версия) :
ха, классный вопрос :)
Так сложилось, что я ушёл в формальные доказательства. Поэтому на идрисе кроме крестиков ноликов я так ничего и не написал.
Но в целом, кроме того что привёл как пример monk, есть Scala - промышленно применяемый язык с зависимыми типами. Там можно поглядеть как это должно выглядеть ориентировочно. + Идрис может быть облегчит написание за счёт того Бреди называет type driven development. (Вообще на сколько я помню, мне показалось что очень удобно было видеть цели в ide, по сравнению со скала).
Для чего-то ещё годится эта dependent typed system?
Для формальных доказательств ещё.
Исходная версия AndreyKl, :
ха, классный вопрос :)
Так сложилось, что я ушёл в формальные доказательства. Поэтому на идрисе кроме крестиков ноликов я так ничего и не написал.
Но в целом, кроме того что привёл как пример monk, есть Scala - промышленно применяемый язык с зависимыми типами. Там можно поглядеть как это должно выглядеть ориентировочно. + Идрис может быть облегчит написание за счёт того Бреди называет type driven development.
Для чего-то ещё годится эта dependent typed system?
Для формальных доказательств ещё.