ウィキペディアには次のように書かれています。
完全な関数型プログラミング (通常の関数型プログラミングまたは弱い関数型プログラミングとは対照的に、強力な関数型プログラミングとも呼ばれます) は、プログラムの範囲を、終了することが証明されているプログラムに制限するプログラミング パラダイムです。
と
これらの制限は、関数型プログラミング全体がチューリング完全ではないことを意味します。ただし、使用できるアルゴリズムのセットは依然として膨大です。たとえば、漸近的な上限が計算されたアルゴリズムは、反復または再帰ごとに減分される追加の引数として上限を使用することにより、証明可能な終了関数に自明に変換できます。
Total Functional Programmingに関する論文についての Lambda The Ultimate Post もあります。
私はメーリングリストで先週までそれを知りませんでした。
あなたが知っているリソース、参照、または実装例は他にありますか?
私がそれを正しく理解していれば、TotalFunctionalProgrammingはまさにそれを意味します：TotalFunctionsを使ったプログラミング。私の数学のコースを正しく覚えていれば、全体関数はその定義域全体で定義されている関数であり、部分関数はその定義に「穴」がある関数です。
ここで、ある入力値に対してv無限再帰または無限ループに入る関数がある場合、または一般に他の方法で終了しない関数がある場合、関数はに対して定義されていないためv、部分的、つまり合計ではありません。
トータル関数型プログラミングでは、そのような関数を書くことはできません。すべての関数は、可能なすべての入力に対して常に結果を返します。タイプチェッカーは、これが事実であることを確認します。
私の推測では、これによりエラー処理が大幅に簡素化されます。エラー処理はありません。
欠点はあなたの引用ですでに述べられています：それはチューリング完全ではありません。たとえば、オペレーティングシステムは本質的に巨大な無限ループです。実際、オペレーティングシステムを終了させたくありません。この動作を「クラッシュ」と呼び、コンピュータに怒鳴りつけます。
これは古い質問ですが、これまでのところ、完全な関数型プログラミングの本当の動機について言及している回答はないと思います。これは次のとおりです。
プログラムが証明であり、証明がプログラムである場合、「穴」のあるプログラムは証明として意味がなく、論理的な矛盾が生じます。
基本的に、証明がプログラムであれば、無限ループを使って何でも証明できます。これは本当に良くないことであり、なぜ完全にプログラミングしたいのかという動機の多くを提供します。他の回答は、紙の裏側を説明しない傾向があります。言語は技術的に完全にはチューリングされていませんが、共帰納的な定義と関数を使用することで、多くの興味深いプログラムを復元できます。私たちは帰納的なデータを考える傾向がありますが、codataはこれらの言語で重要な目的を果たします。無限の定義を完全に定義できます (そして、終了する実際の計算を行うときは、この有限部分のみを使用する可能性があります)。 、またはオペレーティングシステムを作成している場合はそうではないかもしれません!)。
また、Coq など、ほとんどの証明アシスタントがこの原則に基づいて機能することにも注意してください。
チャリティーは終了を保証する別の言語です：http：
//pll.cpsc.ucalgary.ca/charity1/www/home.html
ヒュームは4つのレベルを持つ言語です。外側のレベルはチューリング完全であり、最も内側のレイヤーは終了を保証します：
http ://www-fp.cs.st-andrews.ac.uk/hume/report/