[Agda] Re: Strict positivity and indices

[Nils Anders Danielsson]

On 2012-05-10 21:29, Stefan Monnier wrote:
>> Agda remembers how the arguments to _<_ and length are used, and deduces
>> that the definition is strictly positive.
>
> Can you expand on how Agda does it?

Take the following example:

   infixr 9 _·_
   infixr 2 _⊗_
   infixr 1 _⊕_

   -- Polynomial functors.

   data Functor : Set1 where
     Id      : Functor
     K       : (A : Set) → Functor
     _⊕_ _⊗_ : (F₁ F₂ : Functor) → Functor

   -- Functor application.

   _·_ : Functor → Set → Set
   Id        · B = B
   K A       · B = A
   (F₁ ⊕ F₂) · B = F₁ · B ⊎ F₂ · B
   (F₁ ⊗ F₂) · B = F₁ · B × F₂ · B

   -- Inductive types.

   data μ (F : Functor) : Set where
     inn : (x : F · μ F) → μ F

Why is μ accepted? Take _·_, to start with. Agda computes and records
the following information:

* The first  argument of _·_ occurs strictly positively in _·_.
* The second argument of _·_ occurs strictly positively in _·_.

When Agda later checks μ this information is used to deduce that μ F
occurs strictly positively in μ.

How is the information about _·_ computed? Agda builds a positivity
graph, containing local information about where _·_ and its arguments
are used (making use of previously computed information about _⊎_ and
_×_). Global information is obtained by taking the transitive closure of
this graph. See Agda.TypeChecking.Positivity for details.

-- 
/NAD