Was ist "Total Functional Programming"?

Question

Wikipedia hat folgende zu sagen:

Gesamt funktionale Programmierung (auch als starke funktionale Programmierung bekannt, mit gewöhnlicher oder schwacher funktioneller Programmierung gegenübergestellt wird) ist ein Programmierparadigma , die den Bereich beschränkt Programme zu denen, die beweisbar Terminierung sind.

und

Diese Einschränkungen bedeuten, dass insgesamt funktionale Programmierung nicht Turing-vollständig ist. Jedoch ist der Satz von Algorithmen, die verwendet werden können, immer noch riesig. Zum Beispiel kann jeder Algorithmus, der hat berechnet, eine asymptotische obere Schranke hatten dafür in eine transformierten trivially sein kann beweisbar abbrechenden Funktion durch die obere Grenze als ein zusätzliches Argument die bei jedem Iteration oder Rekursion dekrementiert wird.

Es gibt auch einen Lambda The Ultimate Post über ein Papier auf Total Functional Programming.

Ich war bis letzte Woche nicht auf einer Mailing-Liste.

Gibt es weitere Ressourcen, Referenzen oder Implementierungen, die Sie kennen?

Answer 1

Wenn ich das richtig verstanden habe, bedeutet Total Functional Programming genau das: Programmieren mit Total Functions. Wenn ich mich an meine Mathe-Kurse richtig erinnere, ist eine Total Function eine Funktion, die über ihre gesamte Domäne definiert ist, eine Partial Function ist eine Funktion, die in ihrer Definition "Löcher" aufweist.

Nun, wenn Sie eine Funktion haben, die für einige Eingabewerte v in eine unendliche Rekursion oder eine Endlosschleife geht oder im Allgemeinen nicht auf eine andere Weise endet, dann ist Ihre Funktion nicht für v definiert und somit auch nicht teilweise, dh nicht total.

Total Functional Programming erlaubt Ihnen nicht, eine solche Funktion zu schreiben. Alle Funktionen geben immer ein Ergebnis für alle möglichen Eingaben zurück; und der Type Checker stellt sicher, dass dies der Fall ist.

Meine Vermutung ist, dass dies die Fehlerbehandlung erheblich vereinfacht: Es gibt keine.

Der Nachteil ist bereits in Ihrem Zitat erwähnt: Es ist nicht Turing-vollständig. Z.B. Ein Betriebssystem ist im Wesentlichen eine riesige Endlosschleife. In der Tat, wir nicht wollen ein Betriebssystem zu beenden, nennen wir dieses Verhalten einen "Absturz" und schreien an unseren Computern darüber!

Answer 2

Charity ist eine andere Sprache, die Beendigung garantiert:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Hume ist eine Sprache, mit 4 Ebenen.Die äußere Ebene ist Turing vollständig und die innerste Schicht garantiert Kündigung:
http://www-fp.cs.st-andrews.ac.uk/hume/report/

Answer 3

Während dies eine alte Frage ist, glaube ich, dass keine der Antworten weit so die reale Motivation für die gesamte funktionale Programmierung, erwähnen, die dies :

Wenn Programme Proofs und Proofs Programme sind, dann haben Programme, die "Löcher" haben, keinen Sinn als Beweise und führen zu logischer Inkonsistenz.

Grundsätzlich, wenn ein Beweis ein Programm ist, kann eine Endlosschleife verwendet werden, um alles zu beweisen. Das ist wirklich schlecht und liefert einen Großteil der Motivation dafür, warum wir total programmieren wollen. Andere Antworten neigen dazu, die Kehrseite des Papiers nicht zu berücksichtigen. Während die Sprachen technisch nicht vollständig sind, können Sie viele interessante Programme wiederherstellen, indem Sie co-induktive Definitionen und Funktionen verwenden. Wir sind sehr anfällig für induktive Daten, aber codata dient ein wichtiger Zweck in diesen Sprachen, wo Sie eine Definition, die unendlich ist vollständig definieren können (und wenn Sie echte Berechnung, die beendet, verwenden Sie möglicherweise nur eine Endliches Stück davon, oder vielleicht nicht, wenn Sie ein Betriebssystem schreiben!).

Es ist auch erwähnenswert, dass die meisten Proofassistenten basierend auf diesem Prinzip arbeiten, zum Beispiel Coq.