OCamlの依存型

Question

HaskellとScalaの依存型に関する多くの情報があります。 OCamlのために、それほど多くはありません。誰でもOCamlでこれを達成するためのコーディング例を提供するのに十分な熟練者ですか（それが可能ならば）？もちろん（放棄された）Dependent MLがありますが、このようなものを「通常の」OCamlコードに組み込むことはできないようです。

基本的には、assert(n > 0)のようなコードを削除し、コンパイル時にチェックします。サイドノートとして

EDIT

、それが依存型システムのニーズの一部を埋めることができることを、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 *) 

Answer 1

参照リンクはML言語で使用される依存のような技術の例（OCamlの中か、OCamlのに変換することができる）で、オレグのlightweight dependent typingページです。 2007年にChung-chieh ShanとのLighweight static capabilities (PDF)の彼の論文は特に関連性が高い。

編集：バージョン4.00以降（上記の文書の後にリリースされています）、OCamlにはGADTがあり、洗練された静的情報（以前はファントムタイプのテクニックに依存しています）パターンはOmegaで示されます。強力な型付きプログラミングをするために必須ではないことが示されていますが、野生のさまざまな例でも使用される可能性があります。