Что такое «Общее функциональное программирование»?

Question

Википедия имеет это сказать:

Общее функциональное программирование (также известный как сильный функционал программирование, чтобы быть в сравнении с обычный или слабый функционал программирование) это парадигма программирования который ограничивает спектр программ к тем, которые доказуемо терминатор.

и

Эти ограничения означают, что всего функциональное программирование не Тьюринг. Тем не менее, набор алгоритмы, которые могут быть использованы до сих пор огромно. Например, любой алгоритм, который имеет асимптотическую верхнюю границу рассчитать на это можно тривиально превращается в доказуемо завершающая функция с помощью верхняя граница в качестве дополнительного аргумента который уменьшается на каждом итерация или рекурсия.

Существует также лямбда The Ultimate Post о работе по Полному функциональному программированию .

Я не встречал этого до прошлой недели в списке рассылки.

Есть ли еще какие-либо ресурсы, ссылки или примеры реализации, о которых вы знаете?

Answer 1

Если я правильно понял, Полное функциональное программирование означает только это: Программирование с помощью полных функций. Если я правильно помню свои курсы по математике, функция Total - это функция, которая определена во всей области, а функция Partial - это функция, в определении которой есть «дыры».

Теперь, если у вас есть функция, которая для некоторого входного значения v входит в бесконечную рекурсию или бесконечный цикл или вообще не завершается каким-либо другим способом, то ваша функция не определена для v и, таким образом, частично, то есть не полностью.

Общее функциональное программирование не позволяет вам написать такую ​​функцию. Все функции всегда возвращают результат для всех возможных входов; и проверка типов гарантирует, что это так.

Я предполагаю, что это значительно упрощает обработку ошибок: их нет.

Недостаток уже упоминается в вашей цитате: он не является полным по Тьюрингу. Например. Операционная система по сути представляет собой гигантский бесконечный цикл. На самом деле, мы не хотим, чтобы завершала работу операционной системы, мы называем это поведение «крахом» и кричим на наши компьютеры об этом!

Answer 2

Хотя это старый вопрос, я думаю, что ни один из ответов пока не упоминает о реальной мотивации для полного функционального программирования, которая такова:

Если программы являются доказательствами, а доказательства являются программами, то программы, которые имеют «дыры», не имеют никакого смысла в качестве доказательств и вводят логическое несоответствие.

По сути, если доказательством является программа, бесконечный цикл может использоваться для доказательства чего угодно . Это действительно плохо, и дает большую часть мотивации для того, почему мы могли бы хотеть программировать полностью. Другие ответы, как правило, не учитывают обратную сторону статьи. В то время как языки технически не завершены, вы можете восстановить множество интересных программ, используя коиндуктивные определения и функции. Мы очень склонны думать о индуктивных данных, но codata служит важной цели в этих языках, где вы можете полностью определить определение, которое является бесконечным (и при выполнении реальных вычислений, которые завершается, вы потенциально можете использовать только конечную часть этого, или, возможно, нет, если вы пишете операционную систему!).

Также следует отметить, что большинство помощников по проверке работают на основе этого принципа, например, Coq.

Answer 3

Благотворительность является еще одним языком, который гарантирует прекращение:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Хьюм - это язык с 4 уровнями. Внешний уровень завершен по Тьюрингу, а самый внутренний слой гарантирует завершение:
http://www -fp.cs.st-andrews.ac.uk / hume / report /