# [Agda] parametrised data structures

Nils Anders Danielsson nad at chalmers.se
Thu Jan 26 22:41:56 CET 2012

```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):

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 τ

--