Totale functionele programmering - Total functional programming

Totaal functioneel programmeren (ook bekend als sterk functioneel programmeren , in tegenstelling tot gewoon of zwak functioneel programmeren ) is een programmeerparadigma dat het bereik van programma's beperkt tot programma's die aantoonbaar eindigen .

Beperkingen

Beëindiging wordt gegarandeerd door de volgende beperkingen:

1. Een beperkte vorm van recursie , die alleen werkt op 'gereduceerde' vormen van zijn argumenten, zoals Walther-recursie , substructurele recursie of 'sterk normaliseren', zoals bewezen door abstracte interpretatie van code.
2. Elke functie moet een totale (in tegenstelling tot een gedeeltelijke ) functie zijn. Dat wil zeggen, het moet een definitie hebben voor alles binnen zijn domein.
   • Er zijn verschillende manieren om veelgebruikte deelfuncties, zoals deling, uit te breiden tot totaal: een willekeurig resultaat kiezen voor invoer waarvoor de functie normaal niet gedefinieerd is (zoals voor deling); een ander argument toevoegen om het resultaat voor die invoer te specificeren; of ze uitsluiten door gebruik te maken van type systeemkenmerken zoals verfijningstypes .${\ displaystyle \ forall x \ in \ mathbb {N} .x \ div 0 = 0}$

Deze beperkingen betekenen dat de totale functionele programmering niet Turing-compleet is . De set aan algoritmen die kan worden gebruikt, is echter nog steeds enorm. Elk algoritme waarvoor bijvoorbeeld een asymptotische bovengrens kan worden berekend (door een programma dat zelf alleen Walther-recursie gebruikt), kan triviaal worden omgezet in een aantoonbaar afsluitende functie door de bovengrens te gebruiken als een extra argument dat bij elke iteratie of recursie wordt verlaagd. .

Bijvoorbeeld quicksort is niet triviaal aangetoond substructural recursief, maar het terugkeert slechts tot een maximale diepte van de lengte van de vector (worst-case tijdcomplexiteit O ( n ² )). Een quicksort-implementatie op lijsten (die zou worden afgewezen door een substructurele recursieve checker) is, met behulp van Haskell :

import Data.List (partition)

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

Om het substructureel recursief te maken met de lengte van de vector als limiet, zouden we kunnen doen:

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

Sommige algoritmenklassen hebben geen theoretische bovengrens, maar wel een praktische bovengrens (sommige op heuristiek gebaseerde algoritmen kunnen bijvoorbeeld worden geprogrammeerd om na zoveel recursies "op te geven", waardoor ook beëindiging wordt gegarandeerd).

Een ander resultaat van totaal functioneel programmeren is dat zowel strikte evaluatie als luie evaluatie in principe tot hetzelfde gedrag leiden; het een of het ander kan echter nog steeds de voorkeur hebben (of zelfs vereist) vanwege prestatieredenen.

Bij totale functionele programmering wordt een onderscheid gemaakt tussen data en codata - de eerste is eindig , terwijl de laatste potentieel oneindig is. Dergelijke potentieel oneindige datastructuren worden gebruikt voor toepassingen zoals I / O . Het gebruik van codata houdt het gebruik van bewerkingen zoals corecursie in . Het is echter mogelijk om I / O te doen in een volledig functionele programmeertaal (met afhankelijke typen ), ook zonder codata.

Zowel Epigram als Charity kunnen worden beschouwd als volledig functionele programmeertalen, ook al werken ze niet zoals Turner in zijn paper aangeeft. Dat zou ook rechtstreeks kunnen programmeren in gewoon Systeem F , in Martin-Löf-typetheorie of de Calculus of Constructions .

Referenties