Data structures with nondeterministic components in Coq

Question

I tried to model a less naive monadic encoding of non-determinism (less naive than MonadPlus and common lists) in Coq that is often used in Haskell; for example the encoding for lists looks like

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

whereas the corresponding definition in Coq would like as follows.

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

However, this kind of definition is not allowed in Coq because of the "strictly positive"-condition for inductive data types.

I'm not sure if I am aiming for a Coq-specific answer or an alternative implementation in Haskell that I can formalise in Coq, but I am happy to read any suggestions on how to overcome this problem.

Answer 1

See Chlipala's "Certified Programming with Dependent Types". If you had Definition Id T := T -> T, then List Id could produce a non-terminating term. I think you might also be able to derive a contradiction by Definition Not T := T -> False, especially if you drop the Nil constructor and accept the law of excluded middle.

It would be nice if there were some way to annotate M as only using its argument in positive locations. I think Andreas Abel may have done some work in this direction.

Anyway, if you're willing to restrict your datatypes just a little bit, you could use:

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