関数型言語の技術マップ

要求開発アライアンスの定例会で『Object-Functional Analysis and Design: 次世代モデリングパラダイムへの道標』というタイトルでセッションを行うことになりました。

セッション時間が50分なので、かなり俯瞰した形での全体像の説明になりそうですが、関連する要素技術の数が多いのと、内容が込み入っているので、ブログで補足説明をすることにしました。

今回はその第一弾です。

「関数型言語の関連技術」として用意した以下の図を説明します。関数型プログラミング言語レベルの説明はScalaを対象にします。

Disclaimer

2008年にScalaをはじめて足掛け4年、関数型プログラミングとは、どうも数学を使ってプログラミングしていくことらしい、ということが分かってきました。

ScalaをBetter Javaとして使うのであれば、そこまで頑張らなくてもよいのですが、関数型言語のパワーを引き出すにはやはり関数型プログラミング、さらにいうと関数合成をベースとしたMonadicプログラミングをしていく必要があります。

ボク自身はにわか関数型プログラマですし、数学や計算機科学は門外漢なので関数型言語の背景技術を調べるのはなかなか辛いのですが、関数型プログラミングをする以上は避けて通れないので、牛歩のようなスピードですが、少しづつ調べています。

現時点で分かったことをまとめたのが上の図です。

計算機科学、数学の観点からは緩い点もあると思いますが、逆にオブジェクト指向プログラマの目から見た関数型言語という観点で見て頂けると、これから関数型言語にアプローチする人にはよいスタートポイントになるかもしれません。

Curry-Howard対応

プログラミング言語の中での関数型言語の位置付けを考える上で重要なのがCurry-Howard対応(Curry-Howard correspondence)です。

Curry-Howard対応の詳細は上記Wikiページやk.inabaさんのCurry-Howard Isomorphism も参考になります。

ざっくりいうと、「単純型付ラムダ計算」と「直感主義命題論理&自然演繹」がIsomorphism(同型)ですから文字通り相互変換が可能ということです。この枠組みの中では「型＝命題」、「計算＝証明」となり、コンパイルが成功すれば証明完了となります。まさにプログラミングが数学の証明と同じということです。凄いですね。

残念ながら「直感主義命題論理&自然演繹」で記述できる範囲は狭いので、汎用的に一般の問題を記述できるわけではありません。

しかし、同型という形で数学と直結している点が重要です。「直感主義命題論理&自然演繹」を軸に、数理論理学の膨大な理論体系をプログラミングに取り込む可能性がみえてきます。

純粋関数型言語

関数型言語は大きく純粋関数型言語と(純粋でない普通の)関数型言語に分類することができます。

純粋関数型言語は、副作用がないといった性質が有名?ですが、重要なのは「単純型付ラムダ計算」をプログラミング言語として実現した物ということであろうと思います。

「純粋関数型言語」＝「単純型付ラムダ計算」であればさらに、「純粋関数型言語」＝「直感主義命題論理&自然演繹」であるわけで、プログラミング言語と数理論理学が直結することになります。

ハードウェアの壁

純粋関数型言語は、「マッカーシーの5つの基本関数」 の時代から関数型言語の理想の姿でした。関数型言語における関数の評価は、ラムダ計算を基盤にしていて、数学的に記述して証明できることがそもそもの存在理由だったわけです。

しかし、ハードウェア性能の壁を乗り越えることは難しく、現在に至っています。関数型言語は実用性能を得るために、手続き型言語機能やオブジェクト指向言語機能を取り込んで、事実上関数型言語的な手続き型言語、関数型言語的なオブジェクト指向言語として使用されてきました。

いうまでもありませんが、ハードウェア性能の向上はこういった制約を取り払いつつあります。

Webアプリケーションなどのアプリケーションプログラムでは、RubyやPythonといったインタープリタ型のスクリプト言語が実用言語として十分機能することが明らかになってきました。コンパイル型の純粋関数型言語ではこの壁はすでに超えていることは容易に推測できます。

Scalaの立場

ハードウェア性能が純粋関数型言語を動作させるのに十分なレベルに向上してきたのではないかということを説明しました。しかし、それでは一足飛びに純粋関数型言語に切り替えてしまえばよいのかというと、そう簡単でもありません。

ハードウェア性能が向上したといっても、やはりぎりぎりの局面では副作用のあるプログラムにしたいケースは残りそうです。仮にそういう事は事実上は滅多にないにしても、いざという時のために保険の意味で機能は残しておきたいのが人情です。

もう一つは、純粋関数型言語で状態を扱う技術であるモナドの難易度が高いことです。習得コストがかなり高いので、すでにオブジェクト指向言語で普通にプログラミングできるエンジニアが、コストをかけて学ぶメリットがあるのかという問題が出てきます。モナドを習得してはじめてスタートラインに立てるというだけなので、習得のインセンティブはかなり小さくなります。

これらのニーズを満たす解として考えらられるのがScalaが採用しているハイブリッド方式です。

Scalaでは、キーワードval、mutable/immutableの2種類がパラレルに用意されているコレクションライブラリ、代数的データ型を実装するのに適したcase classとキーワードsealed、といった形で副作用のない純粋関数型的なプログラミングを行うための仕掛けが多数用意されています。

この範囲でプログラミングしておけば、純粋関数型言語に近しい効果を得ることができます。

Scalaでは不変オブジェクトであるListは何も設定しなくても使えるのに対して、オブジェクト指向プログラミングに必須のArrayBufferは、importしなければ使えないようになっています。これは、純粋関数型的な利用方法を推奨するのがScalaのスタンスということの現れだと思われます。もちろん「純粋」では対処できない問題に対して(Javaと同等以上の)通常のオブジェクト指向プログラミングも可能になっています。

また、アルゴリズムのコアの部分は純粋関数型的に記述するとしても、それを取り囲む周辺機能は普通のオブジェクト指向プログラミングで記述するのも可能です。このため、関数型プログラマとオブジェクト指向プログラマが同一言語で協業するような運用も可能になります。

もちろん、不慮のバグで副作用が発生する可能性もあるので、純粋関数型言語のように安全というわけではありませんが、プログラマが気をつければ、純粋関数型プログラミングのメリットを享受できるようになっているわけです。

新しい要素技術

純粋関数型言語と相性のよい色々な要素技術が追加されています。

• 代数的データ型
• 永続データ構造
• 型クラス

代数的データ構造は、代数的な計算に適したデータ型です。Scalaでの実装は不変オブジェクトであることに加えてキーワードsealedを用いることで、開いた形での継承によるポリモーフィズムを使わないようにします。

永続データ構造は、副作用を持たないデータ構造です。純粋関数型データ構造(pure functional data structure)という用語もあり、同じ意味を持つと思われます。一度作ったデータ構造は、二度と変更されることがなくメモリ上に残り続けるので「永続」と呼ばれています。(不揮発性のストレージに格納するという意味の「永続」ではありません。)不変オブジェクトのみで木構造やグラフ構造といったものを実現します。関数型プログラミングでは永続データ構造を使うスキルが重要になってきます。

型クラスは、「アドホック・ポリモーフィズムを提供する型システム」と定義されています。

オブジェクト指向的にいうと、アルゴリズムを実現したフレームワークと処理対象のデータオブジェクトを、それぞれ相互に依存しない形で実装したものを、どちらも変更することなく後付で接続するためのメカニズムです。

Scalaでは暗黙パラメタを使ったConceptパターンという手法で実現します。暗黙パラメタに対する文脈として型クラス・インスタンスをバインドすることで、フレームワークとデータオブジェクトをプログラム上は疎結合のままコンパイル時に接続できるのがミソです。

群論と圏論

型クラス導入前から、Scalaでもモナドを使うことはできましたが、コンベンションを使用した決め打ちの実装で、拡張性に乏しいものでした。

モナド以外にも、関数型プログラミングに有用な抽象代数学の概念はたくさんあるので、これらを必要に応じて取り入れていきたいニーズがあります。この目的に適したメカニズムが型クラスです。

型クラスは純粋関数型言語であるHaskellが導入した言語機能で、Haskellのクラスライブラリで代数的なメカニズムを構築するのに使用されています。

Scalaでは、型クラスを実現するクラスライブラリScalazを用いると、群論(モノイドなど)や圏論(モナドなど)が定義しているさまざまな代数的な処理をプログラミングテクニックとして利用することが可能になります。

代数的な計算メカニズムのサポートは、当然ながら型付ラムダ計算とも相性がよく、さらに他の数学分野との連携でも有効に機能すると思われます。

発展の方向

数理論理学では、命題論理は基本中の基本ですが、述語論理や様相論理といった形で、よる複雑で応用範囲の広い理論が存在しています。

現段階では、ボクの調べた範囲では、述語論理や様相論理を関数型プログラミングの基本テクニックとして活用できるようにはなっていないようです。

とはいえ、最近話題の証明駆動という形になるのか、論理型言語に昇華していくのか、着地点は分かりませんが長い目で見ればいずれそういう方向に進むのではないかと思います。

圏論の上に論理学の圏を載せたものとしてトポスという理論体系があるようです。また、論理学と代数の裏側には常に集合論が見え隠れしています。このあたりの相互に関連を持つ数学の理論群がいろいろな形で関数型プログラミングにも取り入れられていくことが期待できます。

プログラミング言語が数学と直結することで、数学の理論体系がある意味、プログラムから利用できる具体的な機能となるわけです。実際にモナドやモノイドといった数学上の概念が型クラスという形で利用可能になりました。このポテンシャルはかなり大きく、今後プログラミング技術が大発展するホットスポットになるのではないかと思います。