関数型プログラミング技術マップ2015

『圏論の歩き方』を読んで少し理解が進んだので、関数型プログラミング技術マップを更新しました。「関数型プログラミング技術マップ2014」の2015年版です。

以下の点を改良しています。

• Curry-Howard対応をCurry-Howard-Lambek対応に拡張
• 直観主義述語論理を追加して直観主義命題論理を包含
• カルテジア閉圏とトポス(圏)を追加
• 直観主義命題論理⇔カルテジアン閉圏、単純型付ラムダ計算⇔カルテジアン閉圏間の関係を追加

この図は関数型プログラミング(FP: Functional Programming)を取り巻く理論を整理することを目的としています。

誤解があるといけないので補足しておきますがFPを行うために必須の理論という意図ではありません。

業務アプリケーションをFPで開発するという目的には、圏論も論理学も抽象代数も必須知識ではなく、MonoidやMonadのプログラム上での使い方をパターンとして覚えておけば十分だと思います。代数的データ型もcase classの筋の良い使い方を覚えてしまえば大丈夫です。(もちろんFPとして筋の良いプログラミングをするためには、こういった理論を知っておいた方がよいのは言うまでもありません。)

一方、ビジネス・モデリングや要件定義といった上流のモデリングとFPとの連携を考えていく際には、こういった理論も取り込んでいく必要がありそうです。

OOAD(Object-Oriented Analysis and Design)はUML/MOF(Meta Object Facility)によるようなメタモデルの議論はあるものの、現実的には数学や情報科学とは一定の距離がある現場ベースのベストプラクティスの集大成といえます。OOADによるモデルをOOPで実装するという目的には、数学や情報科学の知識は(あった方がよいのは確かですが)必須スキルという形ではなかったと思います。

しかし、実装技術としてFPが導入されると上流モデルとFPとの連携が論点となってきます。

こういった「FP成分」を取り込んだOOADをOFAD(Object-Functional Analysis and Design)と呼ぶとすると、このOFADでは数学や情報科学をベースとした数理モデルを部分的にでも取り込んでいくことになるかと思います。

一つの切り口としては、OOADのモデルが静的構造モデル、動的モデル、協調モデルから構成されるとすると、(記述力が弱い)協調モデルを数理モデルベースのデータフローで記述し、静的構造モデル、動的モデルを数理モデルとの連続性を担保できるように強化する、といった戦略が考えられます。

このためのモデルとしてどのようなものを採用するのがよいのか分かりませんが、Curry-Howard対応あるいはCurry-Howard-Lambek対応による直観主義命題論理、単純型付ラムダ計算、カルテジアン閉圏によるトライアングルが中心になることが予想されます。

もちろん、一階述語論理/論理プログラミング(Prologなど)や直観主義高階述語論理/証明プログラミング(Coqなど)といった方向性も有力ですが、Scala＆ScalazによるFPでは述語論理は(言語機能的には)スコープ外なので、仮に上流モデルで取り入れたとしてもプログラミングとは不連続になってしまいます。

また、一階述語論理/論理プログラミングや直観主義高階述語論理/証明プログラミングが最終的な解であるにしてもその前提として「Curry-Howard-Lambek対応」の理解は必要です。

そういった意味で、まずは「Curry-Howard-Lambek対応」のスコープで色々と考えていくのがよさそうと考えています。