Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a constructor. This is because if no such condition were made the fixed point combinator could be written and the systems would become inconsistent. Ok great but perhaps this is overly zealous in eliminating these kinds of paths to inconsistency. It reminds me of the the difference between Coq and Agda recursion. Agda allows for recursion in multiple arguments where as Coq requires that one of the arguments always decrease. Is there something similar that we can do with inductive definitions?

Is there a better rule that could be used to allow for more definitions?

  • $\begingroup$ Just a comment: here is related question, and here is a quote from this answer by @Gilles: "Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity". $\endgroup$ – Anton Trunov Sep 27 '16 at 15:43
  • 1
    $\begingroup$ Possible duplicate of Polymorphism and Inductive datatypes $\endgroup$ – jbapple Sep 24 '17 at 22:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.