Non-deterministic component data structures in Coq

Question

I tried to simulate a less naive monadic non-determinant coding (less naive than MonadPlus and general lists) in Coq, which is often used in Haskell; for example, the encoding for lists looks like

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

whereas the corresponding definition in Coq would be as follows:

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

However, such a definition is not allowed in Coq because of the “strictly positive” condition for inductive data types.

I'm not sure if I intend to get an answer to Coq or an alternative implementation in Haskell that I can formalize in Coq, but I am happy to read any suggestions on how to overcome this problem.

Answer 1

See Chlipala Certified Dependent Type Programming . If you have Definition Id T := T -> T , then List Id can call a non-limiting term. I think you can also get a Definition Not T := T -> False contradiction, especially if you drop the Nil constructor and accept the excluded middle law.

It would be nice if there was some way to annotate M as soon as you use its argument in positive places. I think that Andreas Abel may have done some work in this direction.

In any case, if you want to limit your data types a bit, you can use:

 Fixpoint SizedList MA (n : nat) : Type := match n with | 0 => unit | S m => option (MA * M (SizedList MA m)) end. Definition List MA := { n : nat & SizedList MA n }.