[Agda] Relaxing the strict positivity requirement

[Daniel Peebles]

Hi all,

I was fooling around with the usual inductive-recursive dependent context
construction the other day:

module Env where
open import Data.Unitopen import Data.Natopen import Data.Fin hiding
(_+_)open import Data.Vec hiding (lookup)open import Data.Product
mutual
  data Context : Set₁ where
    ε   : Context
    _,_ : (Γ : Context) (S : Env Γ → Set) → Context

  Env : Context → Set
  Env ε = ⊤
  Env (Γ , S) = Σ (Env Γ) S
I then wondered if I could make it inductive-inductive, because we
love inductive families around here:


  data Context′ : Set₁ where
    ε   : Context′
    _,_ : (Γ : Context′) (S : Env′ Γ → Set) → Context′

  data Env′ : Context′ → Set₁ where
    ε   : Env′ ε
    _,_ : ∀ {Γ S} (xs : Env′ Γ) (x : S xs) → Env′ (Γ , S)


But unfortunately, Agda (correctly) rejects this definition as not being
strictly positive, because Env′ carries its Context′ index in an implicit
parameter and that appears in a negative position in Context′. This type
does, however, "feel" quite safe. I have a feeling my feeling of safety
comes from the fact that the index is structurally decreasing, but I can't
really put my finger on it. I spoke to Ulf on IRC about it and he said he
had a similar feeling, and other instances of the same kind of pattern
arose with a HOAS AST for the STLC.

Anyway, I was wondering if anyone knew of any work on relaxing the strict
positivity requirement and giving it a bit more of a "structural recursion"
flavor so the above definition could typecheck. I'd also be interested to
hear if the definition is actually unsafe (i.e., someone turns off
positivity checking and can prove false using that type).

Thanks,
Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111206/ba0f8c8b/attachment-0001.html