Проимущества такого языка очевидны - мы можем доказать, что программа всегда завершится (ибо любая программа на таком языка терминальна), а функции которые нельзя выразить в таком языке всё равно находятся в области кукаретики (не имеют отношения к real world программированию). Все так или иначе используют map, fold, filter и другие примитивно-рекурсивные комбинаторы.
И так анон, как бы он выглядел? Какой бы у него был синтаксис?
Лямбда-исчисление позволяет выражать и общерекурсивные функции в том числе (Y-комбинатор). Речь идёт о языке, который допускает примитивную рекурсию, но не допускает общую.
То есть функция вида `f(x) = f(x+1)` не возможна в таком языке, но можно описать функции map, (+), factorial и другие примитивно-рекурсивные функции.
Я не настоящий сварщик, но miniagda с sized types не попадает попадает в класс primitive recursion? https://www.cse.chalmers.se/~abela/miniagda/
https://www21.in.tum.de/~traytel/papers/fscd16-coind_lang/paper.pdf пишут, что примитивная рекурсия является синонимом структурной. Хз, правда или нет, если да, то в тогда практически любой proof assistant является таким языком. Coq и его клоны построены на структурной рекурсии. Капча намекает, лол.