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

Question

我试图在Coq中建模一种不太天真的monadic编码的非确定性(比MonadPlus和常见列表更不天真),这在Haskell中经常使用; 例如,列表的编码看起来像

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.

但是,由于归纳数据类型的"严格正"条件,Coq中不允许这种定义.

我不确定我是否打算在Haskell中针对Coq特定的答案或替代实现,我可以在Coq中形式化,但我很高兴阅读有关如何克服此问题的任何建议.

Answer 1

请参阅Chlipala 的“依赖类型的认证编程”。如果你有Definition Id T := T -> T，那么List Id可以产生一个非终止项。我认为你也可以通过 导出矛盾Definition Not T := T -> False，特别是如果你放弃Nil构造函数并接受排中律。

如果有某种方法可以注释M为仅在肯定位置使用其参数，那就太好了。我认为安德烈亚斯·阿贝尔可能在这个方向上做了一些工作。

无论如何，如果您愿意稍微限制一下数据类型，您可以使用：

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 }.