[Agda] Re: Strict positivity and indices
Nils Anders Danielsson
nad at chalmers.se
Mon May 14 13:17:48 CEST 2012
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
More information about the Agda
mailing list