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$ Commented Sep 27, 2016 at 15:43
  • 1
    $\begingroup$ Possible duplicate of Polymorphism and Inductive datatypes $\endgroup$
    – jbapple
    Commented Sep 24, 2017 at 22:21


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.