コンビネータ

ラムダ計算の親戚みたいな理論として、コンビネータ理論がありますが このページの趣旨は、理論的なことはさておき コンビネータを使って遊んでみようというものです。 例えばコンビネータを使うと 「引数の順序を入れ替えたり、入れ替えて適用する」 といったことができます。 なお、ここではλ式について少し知識があることを仮定しています。 最初にコンビネータとは何かというと 「自由変数を含まないλ式」、と定義されています。 自由変数とはλ式において束縛されていない変数のことで letによる関数定義をλ式の定義とみなすと  引数が束縛変数、  既に定義されてる識別子が自由変数 になります。
自由変数と束縛変数
let x = 10;;
//λx.yxのつもり
let f y = y x;;	//x:自由変数、y:束縛変数
コンビネータに関する本として スマリヤンの本「To mock a mocking bird」 (邦題:数学パズル ものまね鳥をまねる―愉快なパズルと結合子論理の夢の鳥物語) は有名です。 この本の楽しいところは、様々なコンビネータに鳥の名前を付けていて 特定のコンビネータの組み合わせで表現出来るもの全体を 森(forest)と呼んだりしてるところです。 (ex.KestrelとStarlingがいる森には、ものまね鳥(Mockingbird)がいる  M=S(SKK)(SKK)といった風に計算できるため) ちなみに、Starlingはムクドリで Kestrelはチョウゲンボウだそうです。 いくつか見てみましょう。
コンビネータの例
let i x = x;;            //Identity bird
let istar x y = x y;;    //Identity bird once removed
let b x y z = x (y z);;  //Blue bird:瑠璃鶇(ルリツグミ)
let t x y = y x;;        //Thrush:鶫(ツグミ)
let c x y z = x z y;;    //Cardinal:コウカンチョウ
最初のIコンビネータは、引数をそのまま返すコンビネータです。 istarはI*というコンビネータで、これもIコンビネータの仲間です。 (starは短く発音するために私が勝手につけた名前です) 以下の2つの結果は同じになります。
I*コンビネータ
      (fun x -> x+1) 2 |> printfn "%d";;
istar (fun x -> x+1) 2 |> printfn "%d";;
こんなのが何の役に立つんだ!と思うかもしれないですが 高階関数と組み合わせたりすると便利なことがあります。 (Iコンビネータはidだとか identityだとかいう名前で見かけることが多い) 以下はIコンビネータを利用した例です。
木構造へのfold関数を作る
type Tree = L of int | B of Tree * Tree;;
let rec tfold_fg f g tree =
    match tree with
        | L(i) -> f i
        | B(l,r) -> g (tfold_fg f g l) (tfold_fg f g r);;
tfold_fg i (fun x y -> x+ y) (B(B(L(1),L(2)),L(3))) |> print_any;;
Treeは木構造を表すデータ型(Lが葉、Bが枝)で tfold_fgは  ・木構造の葉に作用する関数f  ・左右のノードの結果に作用する関数g を使って値を折りたたむ関数です。 この例では、単に和を求めたいだけだったので 葉に対する処理は何もしないという意味でIコンビネータを渡しています。 I*に関しては F#で演算子を定義すれば演算子の優先順位と結合性を 変更出来ることを利用して 関数呼び出しの括弧を減らすのにもつかえます。
I*コンビネータの利用
let ( ** ) = istar;; //let ( ** ) x y = istar x y;;
let ( ||>) = istar;;

let f x = x + 1;;
let g x = x * 2;;
printfn "%d" (f (g 10));;
printfn "%d" ** f ** g 10;;
//printfn "%d" ||> f ||> g 10;;	//エラー
ライブラリを作る際はI,I*,I**,...コンビネータは シンタックスシュガー作りにも使えそうです
シンタックスシュガー
let pen = "pen";;
let a x = x;;		//Iコンビネータ
let is x = a x;;		//I*コンビネータ
let this x = is x;;	//I**コンビネータ
> this is a pen;;
val it : string = "pen"</a>
Bコンビネータは関数合成に相当するコンビネータです。 TやCは引数の順序を入れ替えるのに使えるコンビネータです。 Tは1番目と2番目、Cは2番目と3番目を入れ替えます。 ちなみに、これ以後は 3番目と4番目を入れ替えるC*, 4番目と5番目を入れ替えるC**, C***,...と続きます。
Cコンビネータの利用
c List.map [1..10] ((+)1) |> print_any;;
引数を入れ替えたい時ってのはわりとあるもので 結構便利に使えます。 ただし、あまり順番を入れ替えすぎてしまうと コードがわかりにくくなってしまう恐れもあり 使いすぎには注意したほうが良いと思います。 Bコンビネータを次のように使えばC*,C**,...を定義するのにも使えます。 C*=B C C**= B C* ... (ただ、B T≠Cです) Wコンビネータ(Warbler:うぐいす)なんかも同様にしてW*,W**が定義できます。 他のコンビネータにも興味がある方は この素晴らしいページへ。 鳥の名前一覧もあって、しかもコンビネータ計算機付きです

F#での制限事項

次の例を動かそうとすると
Bコンビネータで
let cstar a b c d = a b d c;;	//OK
//(('a -> 'b -> 'c -> 'd) -> 'a -> 'c -> 'b -> 'd)
let cstar2 = b c;;	//NG
//(('_a -> '_b -> '_c -> '_d) -> '_a -> '_c -> '_b -> '_d)と推論
cstar2は型エラーのため定義できません。 これは、結論から言えば「書き換え可能な変数」があるために 型推論の規則に制限(value restriction)があるからだそうです。 こうした制約はML系の言語は何らかの形で持っているそうで F#の場合は 「メンバ、コンストラクタ、関数、type functionではない任意の要素の  結果のシグニチャはfree inference type variablesを含んではならない」   The resulting signature of any item that is not a member,   constructor, function, or type function   must not contain any free inference type variables;   if so, a value restriction. error is reported. となっています(12.1) 他のML系言語関連の説明も役に立つと思いますので プログラミングin OCamlの78-79,162-163ページや ここやここなども参考に挙げてみます。 StackOverflowのスレッドには 上のエラーに対して次の2つの解決策が載っています。  1.型注釈を付ける(これはそのままの意味)  2.η変換(の逆の操作)を利用する η(イータ)変換というのは、 関数fについて、fun x -> f xをfに変換することです。 (fun x -> f x)とfは、 どちらも同じ引数に対して同じ結果を返すので、 これらを同じものと見なしてしまうというのが 基本的なアイデアです。 先ほどのコンビネータでの型エラーは、部分適用によって 未解決のfree inference type variableが残ってしまったのが原因なので 具体的には次のようにします(η変換の逆の操作) エラーメッセージから、 推論された型は4つの引数をとることがわかるので 引数を4つほど追加して
Bコンビネータで
let cstar3 x y z w = b c x y z w;;
このようにするとfree inference type variableが無くなるため エラーが出なくなります。 F#ではこういう制限があったりするので コンビネータ自体について興味があるなら 先ほど紹介したcombinator birdsの計算機や petit lambdaなどのソフトウェアを使ったほうが 面倒がなくて良いかもしれません。 次のサイトにはλ項のみで様々な計算を行う方法が紹介してあるので 興味を引かれた人はコンビネータ版への書き換えに挑戦してみては いかがでしょうか (参考:Church Numerals と Lambda Calculus ところでλ計算には型のあり/なしという観点での分類があって オリジナルのコンビネータの理論は 型無しλ計算(untyped lambda calculus)と対応していますが、 F#は型付きλ計算(typed lambda calculus)を背景としています。 (※2、※3型付きのコンビネータの理論はCartesian Closed Categoryというものに対応してるそうです) Churchが型のないλ計算に変わって、型付きのλ計算を導入したのは ラッセルのパラドックスが起こらないようにするためだったという経緯があるため(※1) 型付きのλ計算の中でも 単純型付きλ計算(simply typed lambda calculus)と呼ばれているものは 型なしλ計算よりも計算出来る範囲が狭くなります。 おそらくそのあたりのことが原因で λ計算の世界で再帰を実現するためのコンビネータとして 有名なYコンビネータは、 単純型付きλ計算の世界では定義できません。 F#でも、普通にやると型エラーが起きてしまいます。 しかし、型ありのλ計算に再帰型を加えれば 型なしのλ計算と同じ計算能力になることがわかっているそうで F#でも再帰的な型を使って、Yコンビネータが定義できます。 いげ太さんのブログに、実際に F#でYコンビネータを実装した例が載っています。 ※1 Proofs are Programs: 19th Century Logic and 21st Century Computingの3 Typed lambda calculus ※2 P.-L. Curien (1986) Combinators Categoriques. Algorithmes Sequentiels et Programmation Applicative. These de Doctorat detat. Univ. Paris VII. または P.-L. Curien (1993) Categorical Combinators, Sequential Algorithms and Functional Programming. Progress in Theor. Comp. Sci., Birkhauser. ※3 J. Lambek (1980) From types to sets. Adv. in Math. 36. 113-164