「「関数型プログラミングはオブジェクト指向の正当な後継」なの？」を書いていて次のようなことを思いました： テクノロジーに関する思索を語るのは推奨されるべき事だと思いますが、ベーシックな知識に裏打ちされてないと、解釈困難で意味不明になりがちです。せっかくの経験や思いがうまく伝わらないことになります。
知識は大切だな、とは思っているので、ちょっと気になりそうなトピックに関して、ベーシックな知識の入り口を解説する記事を書いてきました。
- モナド 入門 → 世界で一番か二番くらいにやさしい「モナド入門」 （2006年）
- 圏論 入門 → はじめての圏論 その第1歩：しりとりの圏 （2006年）
- 継続 入門 → CPS（継続渡し方式）変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ （2008年）
- メタクラス・レイフィケーション 入門 → いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ （2008年）
- ラムダ計算 入門 → JavaScriptで学ぶ・プログラマのためのラムダ計算 （2007年）
- ゲーデルの不完全性定理 入門 → プログラマのための「ゲーデルの不完全性定理」(1) （2006年）
公開年を見るとわかるように、いずれも10年近く前です。一度書いてしまうと、同じことを繰り返し書く気にはなれないので、このテの入門記事を書くことはなくなってしまいました。
表題の「関数型プログラミングとオブジェクト指向」とかは、今でも興味を持つ人は多いのでしょうが、（僕自身にとっての）新しい切り口がなかなか見つからない。「なんかないかな？」と見渡してみると、型クラスあたりかな、と。
型クラスは重要で面白い話題だと思います。ただね、例によって概念も用語法も混乱していて、それを整理するのがすごく負担。そもそも型クラスって何？ の定義を確定するのが容易じゃない。
元祖・型クラスみたいなHaskellの型クラスは、およそ指標（signature）のことです。Standard MLでは素直にsignatureと呼んでます。しかし、Standard MLのsignatureは（structure, functorと共に）モジュール機構を意図しているので、多相な型システムとは微妙に違う気がします。
CoqやIsabelleの型クラスとなると、指標だけではなくて公理を書けます。よって、型クラスは形式セオリー（または形式仕様）のことになります。公理（条件、制約、表明）を書けない型クラスというのは、人間だけが知っている暗黙の思いに支えられている点で不十分で脆弱なものです。
例えば、Haskell型クラスの定番の例であるEqクラス：
class Eq a where (==) :: a -> a -> Bool
こんなもんで等号の性質を規定したことには全然なりません。Coq型クラスなら、
Class Setoid A := { equiv : relation A ; setoid_equiv :> Equivalence equiv }.
Equivalenceは、反射律（Reflexive）、対称律（Symmetric）、推移律（Transitive）をまとめた記述で、等号（同値関係を表す記号）として満たすべき制約まで記述してます。これなら、二項関係equivが等号にふさわしい関係であることが保証されます。
CoqやIsabelleの型クラスのインスタンス化では、公理（要求される制約）を満たすことの証明を要求されます。通常のプログラミングで、型定義の際に証明を要求されるのは現実的ではありません。しかし、指標だけでは上っ面の構文を規定しただけで、型の内実は何も制約してません。「x == y を x < y と具体化してはいけない」は人間側のモラルに過ぎません。
「指標＋公理」という意味の型クラスには、CoqやIsabelleの型クラスがいいのですが、ややこし過ぎる、しかしHaskell型クラスやML指標では構文だけで貧弱過ぎる、という現状。
「指標＋公理」の記述には、CafeOBJのような形式仕様記述言語が一番いいような気がするんですが、CafeOBJを知っている人／使っている人が少な過ぎて、実効性がありません。実は、Categorical InformaticsのFQL／OPLも「指標＋公理」の説明には好適な素材・道具なんですが、ユーザーの少なさはCafeOBJと同様の問題です。
関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた（愚痴った）ような事情で（あと、C++のコンセプトは宙ぶらりんだし）、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。
