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.

You're probably looking for Freer monads and the NDet effect there. Everything is strictly positive and this representation even gives you non-determinism with committed choice. I implemented that in Agda, but the code is horrible due to the Agda's way of handling universe polymorphism. — user3237465
Committed choice (or call-time choice as the FLP community likes to call it) is exactly what I want to formalise with Coq! My current source is another paper that is explicitly modelling a FLP-like semantics of non-determinism with monads. Since I'm still trying to figure out which model would be best suited to be used in Coq, I'm definitely going to look at the representation with Oleg's Freer monads -- as far as I remember, I have already read the paper (for a different context). So thanks for the reminder! — ichistmeinname

jbapple jbapple · Accepted Answer · 2016-04-05T10:50:41

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

Data structures with nondeterministic components in Coq

1 Answers