4 背景：1990年代における強く型付けされた関数型プログラミング -- Calculi、Miranda、OCaml、Haskell、Pizza

2021-09-25 00:00:21

Microsoftが1990年代初頭に独占的な立場を確立し、オブジェクト指向が世界を席巻していた一方で、 強く型付けされた関数型プログラミングの世界は小さく、取り残されながらも活発で活気に満ちていました。 この世界は、私たちが今「プログラミング言語研究（PL Research）」と呼ぶ他の活動分野と重なっていましたが、 当時は形式的検証、型理論、プログラミング論理、そして適用が広がる圏論が含まれていました。 この世界は基本的な計算、つまり一番わかりやすいのはラムダ計算とシステムFのような派生ですが、 他にもCCSやπ計算[Sangiorgi and Walker 2001]のような並行計算によっても大きな影響を受けました。 統一オブジェクト計算を見出すための努力は順調に行われており[Abadi and Cardelli 1996]、 FOOL（Foundations of Object-Oriented Languages、オブジェクト指向言語の基盤）のような研究会は、 既存の言語に追加されている新しい構成体について基礎となる定式化を探していました[Leavens 1995]。

「形式手法」は、形式化されたハードウェアとソフトウェアに関して政府が大規模に主導する、1980年代の当時の重複分野でした。 産業界における形式的方法の論争[Restivo 2004]および比較的謙虚な成功によって、 1990年代の研究者はモデル検査や静的分析ツールを含む、実用的なバグ発見手法に注目しました。 SMV, Z, ACL, HOL88, PVS, HOL90, Isabelleおよび商業製品などのシステムを使用して、ソフトウェアおよびハードウェア設計の側面がモデル化され、形式化され、検証されました。 これらのシステムの実装とスクリプト作成には、関数型言語、たとえばEdinburgh ML（HOL88）、Standard ML（HOL90、Isabelle）、OCaml（Coq、NuPRL）、 Caml Light（HOL-Lite）、LISP（ACL2、PVS）がよく使用されました。 このように、これらのシステムは、強く型付けされた関数型言語の採用の中核的要素を形成し、関数型プログラミングを理論寄りのコミュニティ界隈にとどめました。 Standard MLの形式的定義[Milner et al. 1990]とその解説は、標準化、協力、形式主義、理論の素晴らしさを信奉する、ほとんど聖なるテキストとして見られていました。 同時に、いくつかの関数型プログラミングシステム、例えばParallel ML[Rabhi and Gorlatch 2003]やHaskellの並列版などは、並列プログラミングの研究と密接に連携していました。 これらが一緒になって、私が学部時代の研究で最初に遭遇したのは強く型付けされた関数型プログラミングとMLだったという文脈を形成しました[Syme 1993]。

1994年に発見されたIntelのFDIVバグ[Athow 2014]により、形式検証に対するハードウェア製造業者の投資が大幅に増加しました。 Intelは学術界に助けを求めましたが、その中から、Carl Seger氏が率いるForteが選ばれました。 Forteは二分決定図と定理証明によってIEEEモデルに対する浮動小数点回路のデータパスを検証するツールチェーンで、 Forte FLと呼ばれる強く型付けされた関数型言語を中心に構築されています。 プログラミング言語の設計にはそれ以外の影響はありませんが、このことが言及されているのは、1996-97年に私がこのプロジェクトのインターンとして雇われ、 その文脈で応用形式検証における記号操作のための「グルー言語」として強く型付けされたFPが非常に有効だったことを経験したからです。 なお、それはF# の初期の応用分野でもあります[Seger et al. 2005]。 Forte FLは、外部データと相互運用する場合や、クォートを含める場合など、強く型付けされた言語の設計に関する実用的な選択も多く行いました。 この経験は後のF# 設計に大きな影響を与えました。

強く型付けされたFPは、1985年に最初にリリースされたMiranda¹でも重要な用途を見せました。 1990年代には、強く型付けされた関数型プログラミングの小さな世界も、活発な研究コミュニティによくある経緯で分裂しました。 Haskell 98は、遅延評価で純粋な関数型プログラミングの流れを統合しました。前身はHOPEとMirandaでした。 1989年からのStandard MLは、関数型と命令型が混在する言語の統一的な取り組みとして残っています。 しかし、INRIA Project Cristalグループは標準化を時期尚早と見なし、その代わりにCaml Lightを作成し、次にOCamlを作成しました[Leroy 2014]。 Standard ML自体は、その革新的なモジュールシステムと密接に関連しており、Poly ML、New JerseyのStandard ML、およびMLtonで実用的な実装が行われていました。

強く型付けされたFP言語とコンパイラーは、関心、採用、そして利用に関して、細流化を続けています。 C、C++、およびJavaの大規模な採用に挑むまでには至っていないので、産業界ではほとんど知られていませんが、 言語を維持し、研究を推進し、OCamlやStandard MLやHaskellの熱心な支持者たちによる小さな群²を形成するのには十分です。 幸運にもこれらの言語を実際に使用した人々（私を含む）は、生産性の劇的な向上といくつかのフラストレーションを経験しました。 オリジナルのMLの実装と同様に、使用されるドメインは通常ある種のシンボリックプログラミングでした。 高い生産性を経験できるのは、提供されている機能が組み合わさったときに生まれる独特な有効性によるものです： それは、安全な合成プログラミングをサポートするHindley-Milner型推論(図1)の「魔法」、ドメインデータを記述および操作する際のパラメトリック多相（ジェネリクス）と判別共用体の有効性、 null値が蔓延しないプログラミングの正当性が持つ利点、コードと形式モデルの密接な対応などです。 これらに加えて、表現指向プログラミングの優雅さと表現力がありました。それはLISPの頃からよく知られていたものですが、喜びと感動をもって新たに再発見するユーザーが相次ぎました。 これらの言語はもっと広く使用される可能性を秘めているけれども、価値のあるプログラミング技術がJavaの広範な採用によって失われつつあるという強い思いがありました。

図1. ML系言語の核となる発想である、Hindley-Milner型推論の形式記述([Wikipedia 2020a]より)

1990年代初頭に起こったオブジェクト指向への関心の波は産業界と同様に学術界にも大きな影響を与えました。 1990年代半ばまでに、FPおよびプログラミング言語の世界の多くは、C++ 、Java、およびOO全般の出現によって、本当にショックを受け、当惑し、混乱を招き、一部のケースでは幻滅を感じました。 反応は様々でしたが、ここでは、2000年代のF# 、Scala、その他の言語の起源を理解するための鍵となる、OOの大波への反応を検討します。

オブジェクト指向に対する反応のひとつは、「降参」してJava実装に取り組むことでした。 Java関連の形式化に取り組んだ人たちもいました。 実際、私が博士論文で最初にやったことはまさにそれでした[Syme 1999a]し、他には基礎的なオブジェクト計算を定式化して論文を発表した人たちもいました。 オブジェクト指向の機能をFP言語に統合するという反応を見せた人もいます： LISPはすでにCLOS（Common LISPオブジェクトシステム）を追加していましたし、 OCamlは魅力的なオブジェクトシステムの基礎として使用される新しい形式の総称性（「列変数多相」と「多相バリアント」）を導入しました[Garrigue 2001]。 同じ頃、Standard MLの設計者と実装者は、ML2000という取り組みを始めました。 その目的は、形式的で、理論的根拠のあるアプローチを用いて、オブジェクト指向に匹敵する言語を構築することでした。 この取り組みは、1990年代後半に頓挫してしまいました。

別の反応には、強く型付けされた関数型言語に関連づいた特定の技術的特徴を「主流の」オブジェクト指向言語に統合することを提案するというものもがありました。 WadlerとOderskyは、パラメトリック多相（ジェネリクス）、判別共用体、およびファーストクラスの関数値を組み込んだJavaの変形であるPizzaの開発を担当しました[Bracha et al. 1998]。 これはその後、Generic Java（GJ）の提案に切り詰められ、その後C# 、Scala、およびF# に大きな影響を与えました。 最終的にGJはJavaジェネリクスの基礎となりましたが、「型消去」の使用と正確な実行時型情報の欠如は重大な妥協点でした。

また別の角度からのアプローチには、関数型プログラミング自体を「分解」して、根本的な問題（例えば、HaskellまたはStandard MLの実装にみられるような）を調べるというものもありました。 その一例が、 なぜ誰も関数型言語を使わないのか という論文でした[Wadler 1998]。 この文書は、私が1998年にMicrosoft Researchで仕事を始めたときの、プログラミング言語の分野に対する理解の中心となっていました。 Wadlerの論文は、下賤な大衆の無知を非難するのではなく、当時の強く型付けされたFP実装の7つの問題を概説しています： それは、ライブラリー、移植性、可用性、パッケージ性、ツール、トレーニング、人気度 です。 また、関数型言語が使われない理由ではないものとして 性能 および 無知 を列挙しています。 F# の初期の開発は、本質的にこれらの問題に対処するための努力でした。

さらに、Poly MLやHarlequin MLWorksなど、強く型付けされたFP言語の新しい商用実装でオブジェクト指向言語と競争しようとした人たちもいました。 しかし、これらはほとんど採用されず、産業界の「大手」の支援が必要だったと感じながらコミュニティを去りました。

最後の反応は、洗練された関数型プログラミング言語を実装するための基盤としてJVMを使用し、 それによってFPをブラウザーおよびWebに配信する手段とすることでした（当時はそれがJavaの背後にある初期の原動力でした）。 これらの取り組みの中で最も重要なのは、PersimmonでのBentonやKennedyらによるStandard MLの研究的/商業的実装であるMLjでした[Benton and Kennedy 1999]。 MLjはプログラム全体のコンパイラーで、オブジェクトプログラミング拡張機能を介してJavaエコシステムと相互運用できました。 Persimmonの研究部門が1998年に畳まれたとき、BentonはMSR Cambridgeに移籍し、その後Kennedyも後を追いました。 これは.NETおよびそれ以降のF# と強く関連した体験をもたらしました。 こういったさまざまな反応にもかかわらず、理論系コミュニティではオブジェクト指向への強い嫌悪もありました。 OOの支持者はあっという間に異端の汚名を着せられました：「節操のないナンセンス」、「理論的根拠の欠如」などです。

私が1998年にMicrosoft Researchに参加し、F# に至る前身の作業を開始したことで、全体的な周囲状況の概要が完成しました。 完全を期すために、これらの背景が私自身に与えた影響は次のとおりです。

• 私は、主に定理証明システム（HOL88のEdinburgh ML、HOL 90のNew Jersey Standard ML、HOL-LiteのCaml-Light、IntelのForteFL）のコンテキストで、 強く型付けされた関数型プログラミングを使用しました。 弱点を認めながらも、私はそれらを愛するようになりました。 私の学部時代の仕事は、MLの創始者の一人であるMalcolm Neweyによって監督されていました。 博士課程の仕事、OCamlコミュニティ、そしてMSR Cambridgeを通じて、私は、強く型付けされた関数型プログラミングを規範とする、重複したコミュニティに関わっていました。
• 私は、JavaとJVMの形式化の研究を含む論文の仕事の一部として、オブジェクト指向言語（C++ 、Java）を使用していました。 1992年の大学でのC++ に関する私の印象は否定的でした。特に学生プロジェクトでは階層的な分類が濫用されていたからです – モデリング技法としても、クラス階層へのエンコーディングとしても。
• 子供時代、1980-87年に、私はBASICとLogo（Apple II）とTurbo Pascal（Windows）を使いました。 学生時代に、私はProlog、C、Scheme、Modula 2を使いました。 比較プログラミング言語コースは、幅広い言語に興味を起こさせました。 就職して早い時期に、私はオーストラリアのソフトウェア会社でWindows上のPrologを使っていました（SoftLaw、1990-1993）。
• 私は、博士論文の一部として、SMLNJ、MoscowML、Caml-light、OCamlなどさまざまなMLの方言やツールチェーンを使い、 強く型付けされた言語や、証明とコンパイルのシステムをいくつか実装しました。 さらに私は、当時はやや変わっていましたが、これらのシステムのためのビジュアルツール、 特にHOL90用のグラフィカルな証明編集IDE[Syme 1995]と定理証明器DECLARE用の証明編集ワークベンチ[Syme 1999b]も実装しました。 私はIDEツールに肯定的な印象を持ち、IDEツールと言語設計の間の相互作用を理解しました。
• 1996-98年に、私は、OOと関数型プログラミングを融合するという、Drossopoulou、Leroy、Wadler、Oderskyなどの学術的リーダーの仕事に触れていました[Alves-Foss 1999]。
• 私は、強く型付けされた関数型プログラミングを「大衆」に提供する方法を考え直そうとする議論に参加していました。

インデックスへ戻る