Coq 中具有不确定组件的数据结构

Question

我尝试在 Haskell 中经常使用的 Coq 中对非确定性的不那么天真的单子编码（比 MonadPlus 和普通列表更不天真）建模；例如列表的编码看起来像

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

而 Coq 中的相应定义如下。

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

但是，由于归纳数据类型的 "strictly positive" 条件，这种定义在 Coq 中是不允许的。

我不确定我的目标是针对 Coq 特定的答案还是 Haskell 中的替代实现，我可以在 Coq 中形式化，但我很高兴阅读有关如何克服这个问题的任何建议问题。

Answer 1

参见Chlipala's "Certified Programming with Dependent Types"。如果你有 Definition Id T := T -> T，那么 List Id 可以产生一个非终止词。我认为您也可以通过 Definition Not T := T -> False 推导出矛盾，尤其是如果您放弃 Nil 构造函数并接受排中律。

如果有某种方法可以将 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 }.

Coq 中具有不确定组件的数据结构

Data structures with nondeterministic components in Coq

haskell

coq

non-deterministic