Coqの非決定性コンポーネントを持つデータ構造

Question

私は、Haskellでよく使われるCoqの非決定性（MonadPlusや一般的なリストよりもあまり知られていない）のあまり知られていないモナド符号化をモデル化しようとしました。例えば、リストのエンコーディングは、Coqの対応する定義が以下のようになるのに対して、リストのエンコーディングは、

data List m a = Nil | Cons (m a) (m (List m a)) 

のようになります。

Inductive List (M: Type -> Type) (A: Type) := 
    Nil: List M A 
| Cons : M A -> M (List M A) -> List M A. 

ただし、インダクティブデータタイプの「厳密にポジティブな」条件のため、この種の定義はCoqでは許可されていません。

私がCoq特有の答えや、Coqで正式化できるHaskellの代替実装を目指しているかどうかはわかりませんが、この問題を解決する方法については何かお勧めします。

Answer 1

Chlipala's "Certified Programming with Dependent Types"を参照してください。 Definition Id T := T -> Tがある場合は、List Idは非終端の用語を生成する可能性があります。 Nilコンストラクタを削除し、除外された中間の法則を受け入れる場合は、Definition Not T := T -> Falseによって矛盾を引き出すこともできると思います。

Mにアノテーションを付ける方法がある場合は、正の位置で引数を使用するだけでいいはずです。私はAndreas Abelがこの方向でいくつかの仕事をしていると思います。とにかく

、あなたのデータ型少しだけを制限するために喜んでいる場合は、使用できます。

Fixpoint SizedList M A (n : nat) : Type := 
    match n with 
    | 0 => unit 
    | S m => option (M A * M (SizedList M A m)) 
    end. 

Definition List M A := { n : nat & SizedList M A n }.