3
$\begingroup$

Agda is ruling out definitions like

data Bad : Set where
 bad : (Bad → Bad) → Bad

Because "Non strictly-positive declarations are rejected because one can write a non-terminating function using them." (as one may read in Agda wiki). I know also that disabling strict positivity checking allows constructing inhabitant of empty type.

But Agda also complains about definition like this:

  data Bad? : ℕ → Set where
    badZ : Bad? zero
    badS : ∀ {n} → (Bad? n → Bad? n) → Bad? (suc n)

telling me that:

Bad? is not strictly positive, because it occurs
to the left of an arrow
in the type of the constructor badS
in the definition of Bad?.

What i know is that i can create valid definition without inductive datatypes:

  Bad?′ : ℕ → Set
  Bad?′ zero = Unit
  Bad?′ (suc n) = (Bad?′ n) → (Bad?′ n) 

  badZ′ : Bad?′ zero
  badZ′ = tt

  badS′ : ∀ {n} → (Bad?′ n → Bad?′ n) → Bad?′ (suc n)
  badS′ x = x

My question is:

Can "Bad?" datatype lead to similar inconsistencies, and this is the reason why it is rejected by Agda?

Or is it the case that positivity checking in Agda is too "cautious", and can't figure out that indexing is making it strict positive?

$\endgroup$
3
  • $\begingroup$ Sorry, I did not see your Bad?' at first. I don't think that type leads to inconsistencies, after all Bad?' is accepted. I guess it can not be accepted since Agda does not know how to generate a proper induction principle for it. In Bad?' no induction principle is being introduced, on the type definition. The induction principle for seem to suffice to prove properties on Bad?'. $\endgroup$
    – chi
    May 13, 2019 at 16:30
  • $\begingroup$ @chi Could you elaborate more on your comment? I would be happy to accept it as good answer if you can provide some explanation about impossibility of generating proper induction principle. $\endgroup$
    – MJG
    Aug 21, 2019 at 3:19
  • 1
    $\begingroup$ I don't know much more to write a proper answer. Agda, like similar languages, generates the induction principle following a given algorithm, which only handles strictly positive types. While your Bad? type could be accepted without leading to an inconsistency, the algorithm can not generate an induction principle (and I'm unsure about what an induction principle for Bad? would be). In your case, the type is "stratified" using a natural index, so probably induction on naturals is already enough to prove properties on Bad? -- without a new induction principle. $\endgroup$
    – chi
    Aug 21, 2019 at 7:33

0

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.