12

Scala や OCaml などの最新の型付き関数型オブジェクト指向言語が、パラメトリック ポリモーフィズム、サブタイピング、およびその他の機能をどのように組み合わせているかを知りたいです。

それらはSystem F <:に基づいているのでしょうか、それともより強いものですか、それとも弱いものですか?

これらの言語の「コア」として機能する、Haskell のSystem F Cのような、十分に研究された正式な型システムはありますか?

4

1 に答える 1

15

OCaml

OCaml 型理論の「コア」はシステム F の拡張で構成されていますが、モジュール システムは F <: (モジュールはサブタイプ化によってより厳密な署名に強制することができます) と Fω の混合に対応します。

コア言語 (モジュール レベルでのサブタイプを考慮しない) では、サブタイプの関係を抽象化できないため、OCaml ではサブタイプが非常に制限されています (制限された量化はありません)。この言語は、代わりにポリモーフィック パラメトリズムを強調しています。特に、それがサポートする「拡張可能な」型でさえ、コアで行ポリモーフィズムを使用します (閉じた型の間のサブタイピングの便利なレイヤーを使用)。

OCaml の型理論プレゼンテーションの概要については、Didier Remy によるオンライン ブック、Using, Understanding, and Unraveling the OCaml Language (From Practice to Theory and vice versa) を参照してください。さらに読む章では、特にオブジェクト指向の扱いについて、より多くの参照が得られます。

モジュールシステム部分の形式化には多くの作業がありました。間違いなく、ML モジュール システムはFω または F <: ωをコア形式として自然に適合しません(一度、型パラメーターは、ラムダ計算のように位置で渡されるのではなく、モジュール システムで名前が付けられます)。通信の最良の説明の 1 つは、2010 年に Andreas Rossberg、Claudio Russo、および Derek Dreyer によって最初に公開されたF-ing モジュールです。

Jacques Garrigue は、この言語のより高度な機能 (「システム F に対する単なる構文糖衣」と要約することはできません)、つまりポリモーフィック バリアント (等再帰構造型)、ラベル付き引数、および GADT についても多くの作業を行いました)。 . これらの側面のさまざまな説明は、彼の Web ページで見つけることができます。これには、多相バリアントの機械化された証明 (Coq による) や緩和された値の制限が含まれます。

Web ページA few papers on Camlも参照してください。これは、OCaml 言語に関する研究記事の一部を示しています。

スカラ

Scala の同様のページは、これです。あなたの質問に特に関連するのは次のとおりです。

于 2013-05-24T11:41:20.353 に答える