Проимущества такого языка очевидны - мы можем доказать, что программа всегда завершится (ибо любая программа на таком языка терминальна), а функции которые нельзя выразить в таком языке всё равно находятся в области кукаретики (не имеют отношения к 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 и его клоны построены на структурной рекурсии. Капча намекает, лол.
Примерно как Рефал.
Французы как обычно сдались и переименовали Coq в Rocq. Такой мем загубили, ироды. А изучить советую, лютая годнота.
Единственная в индустрии невсратая система типов, которая ещё и эффективно реализована (привет Lean). Тотальные функции. Встроенный искуственный идиот и нативная поддержка vibe coding'а тактиками, до того, как это стало мейнстримом. Наиболее полная реализация коиндукции. Либы типа https://github.com/math-comp/math-comp
P.S. Туториал: https://softwarefoundations.cis.upenn.edu/lf-current/index.html
Ну, пока еще только в планах. Но радует, что в Coq есть нихуевое метапрограммирование, в котором можно даже синтаксис собственных литералов объявлять (такое только в Racket/Scheme видел, но там это очень многословно и непонятно реализовано).
Правда пока не совсем понятно, как это в реалворлд будет работать. Как только у нас появляется I/O система типов идёт нахуй, и эксепшены должны оборачиваться в Maybe или `try{} catch(){}`, и обработку исключительных случаев берет на себя программист. А так в теории можно написать такой код, который еще на этапе компиляции не допустит, к примеру, деление на ноль.
> Как только у нас появляется I/O
А нету там никакого IO лол.
Вернее, как: люди моделируют состояние реального мира на чистых функциях и каких-нибудь алгебраических эффектах, доказывают всякие инварианты про эту модель, а потом делают extraction из Coq в Ocaml. К примеру: https://github.com/uwplse/verdi-raft Но это уровень кандидатской примерно.
Я со своими тремя классами церковно-приходской на практике только некоторые чистые алгоритмы про lock-free структуры данных верифицировал, что в целом было не так трудно и поприятнее TLA+.
>только примитивно-рекурсивные функции
>мы можем доказать, что программа всегда завершится
не такая тривиальная задача. императивные и функциональные языки используются потому что там это можно доказать, и это сделано математиками. а вот для рекурсии этого нет
>>3506493
ваше лямбда = говно
>функция вида `f(x) = f(x+1)` не возможна в таком языке
чем сразу делает бесполезным такой язык. во первых это уже не рекурсия по определению, а во вторых без этой конструкции невозможно написать ни одну прикладную программу
например как ты сможешь >описать функции map, (+), factorial и другие примитивно-рекурсивные функции
без этой основной конструкции
получается у тебя базовые примитивные функции не рекурсивные, а потом ты из них пытаешься строить рекурсивные прграммы. это так не работает
>первых это уже не рекурсия по определению
Примитивная рекурсию это тоже рекурсия, а если быть точнее, частный случай рекурсии.
>а во вторых без этой конструкции невозможно написать ни одну прикладную программу
>например как ты сможешь >описать функции map, (+), factorial и другие примитивно-рекурсивные функции
С помощью конструкции primrec, что-то типа:
let map fn lst = primrec fn lst
Где, lst - любой моноид, то есть то что имеет нулевой элемент.
Для чисел - это 0, для списков - [], для строк "".
primrec имеет аккумулятор, который вернётся, когда функция достигнет нулевого элемента.
Сам primrec функцией не является, а является синтаксический конструкций, типа "let x=y in exp" или "import Module".