[Agda] Problem with coinduction and positivity checker

[Simon Foster]

Hi,

I've been having problems with defining coinductive datatypes with
associated constraints and the positivity checker. I found the emails
below from 2009 which detail the same problem using an infinite Chains
example, but the discussion does not appear conclusive. I tried the
example and the positivity checker in the latest version of Agda still
rejects the example.

Is this a bug in Agda or a theoretical problem?

> Darin Morrison wrote:
> > Hi All,
> >
> > I'm working on a constructive domain theory module where I need a
> > formalization of chains and ωchains but I'm having some problems with
> > the positivity checker.
> >
> > Here is a snippet of the code I am using:
> >
> > -- Chains
> >
> > mutual
> >   data Chain : ℕ → Set where
> >     []    : Chain 0
> >     _∷_,_ : ∀ {n} (x : carrier) (xs : Chain n) (p : x ≼ xs) → Chain (suc n)
> >
> >   _≼_ : ∀ {n} → carrier → Chain n → Set
> >   _ ≼ []           = ⊤
> >   x ≼ (x′ ∷ _ , _) = x ≤ x′
> >
> > head : ∀ {n} → Chain (suc n) → carrier
> > head (x ∷ _ , _) = x
> >
> > -- ωChains
> >
> > mutual
> >   data ωChain : Set where
> >     _∷_,_ : ∀ (x : carrier) (xω : ∞ ωChain) (p : x ≼ xω) → ωChain
> >
> >   head : ωChain → carrier
> >   head (x ∷ _ , _) = x
> >
> >   _≼_ : carrier → ∞ ωChain → Set
> >   x ≼ xω = x ≤ head (♭ xω)
> >
> > The above encoding of Chains works great.  However, Agda complains
> > that ωChain is not strictly positive because of (xω : ∞ ωChain).  Note
> > that I am using the Coinduction module described by Nils in a previous
> > post.
> >
> > If I change the definition of ωChain to the following, the positivity
> > checker no longer complains:
> >
> > mutual
> >   codata ωChain : Set where
> >     _∷_,_ : ∀ (x : carrier) (xω : ωChain) (p : x ≼ xω) → ωChain
> >
> >   head : ωChain → carrier
> >   head (x ∷ _ , _) = x
> >
> >   _≼_ : carrier → ωChain → Set
> >   x ≼ xω = x ≤ head xω
> >
> > But this formulation is harder to work with for reasons discussed in
> > several recent posts on codata.
> >
> > I'd rather not have to turn off the positivity checker.  Is there any
> > way to get around this?  Perhaps the positivity checker should be
> > modified not to complain in cases like this?
> >

Andreas Abel wrote:
> Surely, the positivity checker should not complain in your case, since
> \infty is a monotone operation on Set.  Semantically,
>
>   \infty T = { t | \flat t \in T }
>
> thus, S \subseteq T implies \infty S \subseteq \infty T.
>
> So, your definition is perfectly positive.  Maybe you should file a bug
> report.
>
> Cheers,
> Andreas

Thanks,

--
Simon Foster <s.foster at dcs.shef.ac.uk>