13

Haskell と Scala には依存型に関する多くの情報があります。OCaml の場合、それほど多くはありません。OCamlでこれを達成する方法についてのコーディング例を提供するのに十分なスキルを持っている人はいますか? (可能であれば) もちろん (放棄された) Dependent MLはありますが、そのようなものを「通常の」OCaml コードに組み込むことはできないようです。

基本的に、私がやりたいことは、コードのようなものを削除しassert(n > 0)て、コンパイル時にチェックすることです。

編集

補足として、OCaml Hybrid Contract Checkingブランチに言及する価値があります。これは、依存型システムのニーズの一部を満たすことができます。あなたの代わりにassert(n > 0)契約書を書きます:

contract f = {x : x > 0} -> int
let f x = x + 1
let dummy_variable = f (-1) (* Won't compile *)

編集 2 : これを読んでいる人にとって、F* は依存型を持つ興味深い ML のような言語だと思います。

4

1 に答える 1

12

参照リンクは、Oleg の軽量な静的保証ページであり、ML 言語で使用される依存型の手法の例 (OCaml または OCaml に変換できます) が含まれています。2007 年の Chung-chieh Shan とのLighweight static capabilities (PDF)に関する彼の論文は、特に関連性があります。

編集: バージョン 4.00 (上記の文書が書かれた後にリリースされた) 以降、OCaml には GADT があり、洗練された静的情報 (以前はファントム型の手法に依存していた) のためのいくつかの手法、特にOmegaで示されている「シングルトン型」パターンを合理化できます。 . それらは強力なタイプフル プログラミングを実現するために必須ではないことが示されていますが、実際に見られるさまざまな例でまだ使用されている可能性があります。

于 2013-03-29T05:50:45.323 に答える