[Agda] Relaxing the strict positivity requirement

[Andrea Lo Pumo]

The following might be of interest:
 
  A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definitions, Lawrence C. Paulson
  http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.9846



On Tue, Dec 06, 2011 at 01:58:22PM -0500, Daniel Peebles wrote:
> 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

> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


--