История изменений
Исправление AndreyKl, (текущая версия) :
По идее всё таки 
lovesan ты прав, идрис не должен быть тьюринг-полным, по крайней мере исходя из того что теория зависимых типов не полна если мне память не изменяет. Но я вот не поручусь ни за то что верно помню, ни за то что идрис это только лямбда-пи, может там какое расширение.
Но повторюсь, ограничение там такое по сути - нельзя написать бесконечный цикл. Обычно это воспринимается как «бох с ним». А учитывая что мы всё равно рекурсиями пишем, то выходит что ничего и не теряем на этом.
Исправление AndreyKl, :
По идее всё таки lovesan ты прав, идрис не должен быть тьюринг-полным, по крайней мере исходя из того что теория зависимых типов не полна если мне память не изменяет. Но я вот не поручусь ни за то что верно помню, ни за то что идрис это только лямбда-пи, может там какое расширение.
Но повторюсь, ограничение там такое по сути - нельзя написать бесконечный цикл. Обычно это воспринимается как «бох с ним», особенно когда всё равно рекурсиями пишем.
Исправление AndreyKl, :
По идее всё таки lovesan ты прав, идрис не должен быть тьюринг-полным, по крайней мере исходя из того что теория зависимых типов не полна если мне память не изменяет. Но я вот не поручусь ни за то что верно помню, ни за то что идрис это только лямбда-пи, может там какое расширение.
Но повторюсь, ограничение там такое по сути - нельзя написать бесконечный цикл. Обычно это воспринимается как «бох с ним», особенно когда, всё равно рекурсиями пишем.
Исправление AndreyKl, :
По идее всё таки lovesan ты прав, идрис не должен быть тьюринг-полным, по крайней мене исходя из того что теория зависимых типов не полна если мне память не изменяет. Но я вот не поручусь ни за то что верно помню, ни за то что идрис это только лямбда-пи, может там какое расширение.
Но повторюсь, ограничение там такое по сути - нельзя написать бесконечный цикл. Обычно это воспринимается как «бох с ним», особенно когда, всё равно рекурсиями пишем.
Исходная версия AndreyKl, :
По идее всё таки lovesan ты прав, идрис не должен быть тьюринг-полным. Но я вот не поручусь.
Но повторюсь, ограничение там такое по сути - нельзя написать бесконечный цикл. Обычно это воспринимается как «бох с ним», особенно когда, всё равно рекурсиями пишем.