Структуры данных с недетерминированными компонентами в Coq

Question

Я попытался смоделировать менее наивное монадическое кодирование недетерминизма (менее наивное, чем MonadPlus и общие списки) в Coq, которое часто используется в 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 из-за "строго положительного" условия для индуктивных типов данных.

Я не уверен, что я стремлюсь к специфическому для Coq ответу или альтернативной реализации в Haskell, которую я могу формализовать в 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 }.