Positivity annotations [Re: [Agda] parametrised data structures]

[Andreas Abel]

James' example is one more where one would want positivity annotations. 
  They are needed for compositional developments.
A compositional type system allows to replace implementations by 
abstractions.  Agda lacks a few ingredients still, one of them is 
positivity annotations.

For the example, here is the corresponding MiniAgda-snippet:

data D (A : Set)
        (P : ++(A -> Set 1) -> Set 1)
        (Q : List A -> Set) : Set 1
{ d : P (\ x -> D A P (\ xs -> Q (cons x xs))) -> D A P Q
}
-- passes, thanks to requiring P to be strictly positive

fun toBot : D Unit (\ F -> F tt -> Empty) (\ xs -> Unit) -> Empty
{ toBot (d f) = f (d f)
}
-- error: F may not occur

Cheers,
Andreas

On 26.01.12 10:41 PM, Nils Anders Danielsson wrote:
>
>    data D {A : Set}
>           (P : (A → Set₁) → Set₁)
>           (Q : List A → Set) : Set₁ where
>      d : P (λ x → D P (λ xs → Q (x ∷ xs))) → D P Q
>
> If this type were accepted by Agda, then we could easily prove that the
> empty type is inhabited (you can try by using --no-positivity-check):
>
>    bad : ⊥
>    bad = to-⊥ (d to-⊥)
>      where
>      to-⊥ : D (λ F → F tt → ⊥) (λ _ → ⊤) → ⊥
>      to-⊥ (d f) = f (d f)

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/