Total Function Programmingを読む
著者のDave TurnerはHaskellの前身のMirandaを設計した人。ちなみに、
- Church's Thesis and Functional Programming
の中でもTotal Function Programmingについて少し触れている。
プログラムの例外や無限ループをどう排除するか、ということに挑戦している。
基本的に普通の言語の関数は、partial function(全射でない関数)として記述する。もちろんプログラムの関数は全射でもかけるけれど、全射でない関数もかけるという意味。これは数学的に一般的にいう関数とは異なる性質になる。また、プログラミングでこういう関数をあつかうために、（あらゆる）型は暗黙的に⊥という最小値をもつものとして扱うdomain theoryがプログラミングの理論の基盤として使われたりする。関数の戻り値として⊥が出るとその関数は無限ループしてる、ということになる。domain theoryはコード中に無限ループがあっても成り立つようにした理論という感じ。
それを排除した、このTotal Function Programmingでは、有限の全射関数のみ記述できる形式に強制にしている。再帰データや再帰関数は書けるけど、強制的に有限になるよう表現が制限される。
以下はこの関数の規則
- Rule 1: 場合わけは完全
- パターンマッチングで場合わけは全パターン必須ということ(エラーの元になるため)
- Rule 2: 型の再帰はcovariant
- 再帰型中で使う型では -> の左手側に自身の型が使えない(無限ループの元になるため)
- Rule 3: 再帰呼び出しは、パラメータの構文的サブコンポーネントでのみ呼び出せる
一方で、無限をあらわす機能としてcodataを用意している。codataはつまりは無限のデータで、Haskellとかだと、普通に再帰定義でかけてしまうデータである。
ここでは、同様に書けるのではなく、codataはcodataだけ扱う関数として切り分けるという感じである。catada中の(codataでない)dataに対しては普通の(Totalな)関数が適用され、codataそのものを処理する場合はcodata用の関数として定義される。
例で
fibs = f 0 1
where
f a b = a <> f b (a+b)のようにあるので、codata関数ではサブコンポーネント制限のようなものはないようだ。
なんとなくHaskellのIOシーケンスと参照透過な関数をMonadで切り分けているのに似た思想な感じ。
codataとdataを分けるのはいいかも。elementary total functionも基本的にそうするのはいいと思う。だた通常の関数の制約としてはきついかもしれない。例だと、n/2で再帰呼び出しするために、整数とビットリストにして、(反転して)下位ビットで振り分けるコードがあったけど、これ普通に考え付くのだろうか。こういうトリッキーなアルゴリズムならしょうがないとは思う。
けど、普通の処理でパターン分解要素だけで再帰呼び出しってどうかな。たとえば言語のevaluatorだと、変数定義式での再帰呼び出しでのenvは、変数が追加されたenvが渡される。このenvはサブコンポーネントではない。複数引数の例としてアッカーマン関数もあったがその条件も満たさないと思う。となるとenvはcodataということになるのだろうか。
余談、データの再帰定義も最小不動点
再帰関数fact n = n * fact (n-1) がf fact n = n * fact (n - 1)の最小不動点だが、
同様に、ones = 1 : ones は f ones = 1 : onesの最小不動点。ghciで
Prelude> let y f = f (y f) Prelude> let ones = y (\o -> 1 : o) Prelude> take 5 ones [1,1,1,1,1]
fibs
Prelude> let fib a b = a : fib b (a+b) Prelude> let fibs = fib 0 1 Prelude> take 10 fibs [0,1,1,2,3,5,8,13,21,34] Prelude> let fib = y (\f a b -> a : f b (a+b)) Prelude> let fibs = fib 0 1 Prelude> take 10 fibs [0,1,1,2,3,5,8,13,21,34]
