Positivity Checking

Note

This is a stub.

The NO_POSITIVITY_CHECK pragma

The pragma switches off the positivity checker for data/record definitions and mutual blocks. This pragma was added in Agda 2.5.1

The pragma must precede a data/record definition or a mutual block. The pragma cannot be used in --safe mode.

Examples:

  • Skipping a single data definition:

    1. {-# NO_POSITIVITY_CHECK #-}
    2. data D : Set where
    3.   lam : (D → D) → D

  • Skipping a single record definition:

    1. {-# NO_POSITIVITY_CHECK #-}
    2. record U : Set where
    3.   field ap : U → U

  • Skipping an old-style mutual block. Somewhere within a mutual block before a data/record definition:

    1. mutual
    2.   data D : Set where
    3.     lam : (D → D) → D
    5.   {-# NO_POSITIVITY_CHECK #-}
    6.   record U : Set where
    7.     field ap : U → U

  • Skipping an old-style mutual block. Before the mutual keyword:

    1. {-# NO_POSITIVITY_CHECK #-}
    2. mutual
    3.   data D : Set where
    4.     lam : (D → D) → D
    6.   record U : Set where
    7.     field ap : U → U

  • Skipping a new-style mutual block. Anywhere before the declaration or the definition of a data/record in the block:

    1. record U : Set
    2. data D   : Set
    4. record U where
    5.   field ap : U → U
    7. {-# NO_POSITIVITY_CHECK #-}
    8. data D where
    9.   lam : (D → D) → D

POLARITY pragmas

Polarity pragmas can be attached to postulates. The polarities express how the postulate’s arguments are used. The following polarities are available:

  • _: Unused.

  • ++: Strictly positive.

  • +: Positive.

  • -: Negative.

  • *: Unknown/mixed.

Polarity pragmas have the form {-# POLARITY name <zero or more polarities> #-}, and can be given wherever fixity declarations can be given. The listed polarities apply to the given postulate’s arguments (explicit/implicit/instance), from left to right. Polarities currently cannot be given for module parameters. If the postulate takes n arguments (excluding module parameters), then the number of polarities given must be between 0 and n (inclusive).

Polarity pragmas make it possible to use postulated type formers in recursive types in the following way:

  1. postulate
  2.   ∥_∥ : Set → Set
  4. {-# POLARITY ∥_∥ ++ #-}
  6. data D : Set where
  7.   c : ∥ D ∥ → D

Note that one can use postulates that may seem benign, together with polarity pragmas, to prove that the empty type is inhabited:

  1. postulate
  2.   _⇒_    : Set → Set → Set
  3.   lambda : {A B : Set} → (A → B) → A ⇒ B
  4.   apply  : {A B : Set} → A ⇒ B → A → B
  6. {-# POLARITY _⇒_ ++ #-}
  8. data ⊥ : Set where
  10. data D : Set where
  11.   c : D ⇒ ⊥ → D
  13. not-inhabited : D → ⊥
  14. not-inhabited (c f) = apply f (c f)
  16. d : D
  17. d = c (lambda not-inhabited)
  19. bad : ⊥
  20. bad = not-inhabited d

Polarity pragmas are not allowed in safe mode.