[Agda] parametrised data structures

[Nils Anders Danielsson]

On 2012-01-26 18:26, James Cranch wrote:
> However, I have been having problems getting this to work. The
> attached code violates positivity.
  
> Does anyone have any ideas for circumventing this?

A variant of your problematic definition:

   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)

In your case there is no reason to believe that N.Map uses its argument
in a strictly positive way. One possible workaround is to replace the
outer function space in "(V : K → Set ν) → Set ℓ" by something more
concrete, which ensures that the "map" is well-behaved.

> It is possible that a coinductive approach would solve that

I don't know what you have in mind, but coinductive types are also
required to be strictly positive.

Sometimes one can work around positivity problems by using recursion. An
example:

   data Ty : Set where
     _⟶_ : Ty → Ty → Ty

   -- Not accepted:

   data D : Ty → Set where
     fun : ∀ {σ τ} → (D σ → D τ) → D (σ ⟶ τ)

   -- Accepted:

   D : Ty → Set
   D (σ ⟶ τ) = D σ → D τ

-- 
/NAD