Полное функциональное программирование - Total functional programming
Полное функциональное программирование (также известное как сильное функциональное программирование , в отличие от обычного или слабого функционального программирования ) - это парадигма программирования, которая ограничивает диапазон программ теми, которые завершаются с доказуемым завершением .
Ограничения
Прекращение действия гарантируется следующими ограничениями:
- Ограниченная форма рекурсии , которая работает только с «сокращенными» формами своих аргументов, такими как рекурсия Вальтера , субструктурная рекурсия или «строго нормализующая», что подтверждается абстрактной интерпретацией кода.
- Каждая функция должна быть общей (а не частичной ) функцией. То есть у него должно быть определение для всего, что находится в его области.
- Есть несколько возможных способов расширить часто используемые частичные функции, такие как деление, до итогового: выбор произвольного результата для входов, на которых функция обычно не определена (например, для деления); добавление еще одного аргумента, чтобы указать результат для этих входов; или исключая их с помощью функций системы типов, таких как типы уточнения .
Эти ограничения означают, что полное функциональное программирование не является полным по Тьюрингу . Однако набор алгоритмов, которые можно использовать, по-прежнему огромен. Например, любой алгоритм, для которого может быть вычислена асимптотическая верхняя граница (программой, которая сама использует только рекурсию Вальтера), можно тривиально преобразовать в доказуемо завершающую функцию, используя верхнюю границу в качестве дополнительного аргумента, уменьшающегося на каждой итерации или рекурсии. .
Например, нетривиально показано , что быстрая сортировка является субструктурно-рекурсивной, но она повторяется только до максимальной глубины длины вектора (временная сложность наихудшего случая O ( n 2 )). Реализация быстрой сортировки списков (которая будет отклонена субструктурной рекурсивной проверкой) с использованием Haskell :
import Data.List (partition)
qsort [] = []
qsort [a] = [a]
qsort (a:as) = let (lesser, greater) = partition (<a) as
in qsort lesser ++ [a] ++ qsort greater
Чтобы сделать его субструктурно рекурсивным, используя длину вектора в качестве ограничения, мы могли бы сделать:
import Data.List (partition)
qsort x = qsortSub x x
-- minimum case
qsortSub [] as = as -- shows termination
-- standard qsort cases
qsortSub (l:ls) [] = [] -- nonrecursive, so accepted
qsortSub (l:ls) [a] = [a] -- nonrecursive, so accepted
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
-- recursive, but recurs on ls, which is a substructure of
-- its first input.
in qsortSub ls lesser ++ [a] ++ qsortSub ls greater
Некоторые классы алгоритмов не имеют теоретической верхней границы, но имеют практическую верхнюю границу (например, некоторые алгоритмы на основе эвристики могут быть запрограммированы так, чтобы «сдаваться» после стольких рекурсий, что также обеспечивает завершение).
Другой результат тотального функционального программирования состоит в том, что и строгая оценка, и ленивая оценка в принципе приводят к одинаковому поведению; однако тот или иной вариант может быть предпочтительным (или даже необходимым) по соображениям производительности.
В общем функциональном программировании, проводится различие между данными и КОДАТОМ -The бывшим является финитарным , в то время как последний является потенциально бесконечным. Такие потенциально бесконечные структуры данных используются для таких приложений, как ввод-вывод . Использование codata влечет за собой использование таких операций, как corecursion . Однако можно выполнять ввод-вывод на полном языке функционального программирования (с зависимыми типами ) и без кодовых данных.
И Epigram, и Charity можно считать полностью функциональными языками программирования, хотя они не работают так, как указывает Тернер в своей статье. То же можно сказать и о программировании непосредственно в простой Системе F , в теории типов Мартина-Лёфа или в исчислении конструкций .