Celkové funkční programování - Total functional programming

Úplné funkční programování (známé také jako silné funkční programování , které je v kontrastu s běžným nebo slabým funkčním programováním ) je paradigma programování, které omezuje rozsah programů na ty, které prokazatelně končí .

Omezení

Ukončení zaručují následující omezení:

  1. Omezená forma rekurze , která funguje pouze na „redukovaných“ formách jejích argumentů, jako je Waltherova rekurze , substrukturní rekurze nebo „silná normalizace“, jak dokazuje abstraktní interpretace kódu.
  2. Každá funkce musí být totální (na rozdíl od částečné ) funkce. To znamená, že musí mít definici všeho ve své doméně.
    • Existuje několik možných způsobů, jak rozšířit běžně používané dílčí funkce, jako je dělení, na totální: výběr libovolného výsledku pro vstupy, u nichž je funkce normálně nedefinovaná (například pro dělení); přidání dalšího argumentu k určení výsledku pro tyto vstupy; nebo je vyloučit pomocí funkcí typu systému, jako jsou typy upřesnění .

Tato omezení znamenají, že celkové funkční programování není Turingovo úplné . Sada algoritmů, které lze použít, je však stále obrovská. Například jakýkoli algoritmus, pro který lze vypočítat asymptotickou horní hranici (programem, který sám používá pouze Waltherovu rekurzi), lze triviálně transformovat na prokazatelně ukončující funkci pomocí horní hranice jako extra argumentu sníženého při každé iteraci nebo rekurzi .

Například quicksort není triviálně zobrazen jako substrukturální rekurzivní, ale rekuruje se pouze do maximální hloubky délky vektoru (nejhorší časová složitost O ( n 2 )). Implementace quicksortu na seznamech (která by byla odmítnuta rekurzivní kontrolou substruktury) je pomocí Haskell : 

import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater

Aby to bylo substrukturální rekurzivní s použitím délky vektoru jako limitu, mohli bychom udělat: 

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

Některé třídy algoritmů nemají žádnou teoretickou horní mez, ale mají praktickou horní mez (například některé heuristické algoritmy lze naprogramovat tak, aby se „vzdaly“ po tolika rekurzích a zajistily také ukončení).

Dalším výsledkem celkového funkčního programování je, že jak přísné hodnocení, tak líné hodnocení mají za následek v zásadě stejné chování; jeden nebo druhý však může být z důvodů výkonu stále výhodnější (nebo dokonce požadovaný).

V úplném funkčním programování se rozlišuje mezi daty a kodaty - první je konečný , zatímco druhý je potenciálně nekonečný. Tyto potenciálně nekonečné datové struktury se používají pro aplikace, jako jsou I / O . Použití kódů znamená použití takových operací jako korekci . Je však možné provádět I / O v úplném funkčním programovacím jazyce (se závislými typy ) také bez kódů.

Oba Epigram a Charity mohl být považován za celkové funkční programovací jazyky, i když nepracují tak, jak Turner upřesňuje ve svém příspěvku. Mohlo tak být možné programovat přímo v prostém systému F , v teorii typů Martin-Löf nebo v Calculus of Constructions .

Reference