Proving strict positivity in Agda

Question

In Agda we can prove termination of functions by using well-founded relations, is there a guideline for proving datatype declarations strictly positive, possibly via use of some container techniques together with well-founded relations?

I have been trying to port Danielsson's A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family to modern Agda and there I have encountered the following argument.

Rendered in more modern Agda:

-- Values

  -- This data type is a little problematic, since Val occurs
  -- negatively in ΠVal and ΠValCong. However, notice that the spines
  -- of the types of the recursive components are decreasing in
  -- ΠVal/ΠValCong, and non-increasing in all other constructors. This
  -- should ensure that the type is well-founded. I'm not aware of any
  -- meta-theory explaining a type such as Val, though.
mutual
    {-# NO_POSITIVITY_CHECK #-}
    data Val : {Γ : Ctxt} {τ : Ty Γ} -> (Γ ⊢ τ) -> Set where
        ✶Val : {Γ : _} {x : Γ ⊢ ✶ Γ } -> Atom x -> Val x
        ElVal : {Γ : _} {n : _} {t' : Γ ⊢ U n} {t : Γ ⊢ El t'} -> Atom t -> Val t
        _∷ˢ_ : {Γ¹ : Ctxt} {τ¹ : Ty Γ¹} {t¹ : Γ¹ ⊢ τ¹}
            {Γ² : Ctxt} {τ² : Ty Γ²} {t² : Γ² ⊢ τ²} -> Val t¹
            -> (t¹ ≈⊢ t²) -> Val t²
        ΠVal : {Γ : Ctxt} {τ₁ : Ty Γ} {τ₂ : Ty (Γ ▻ τ₁)} {t₁ : Γ ⊢ Π τ₁ τ₂}
          -> ΠFun t₁ -> Val t₁
    ΠFun : {Γ : Ctxt} {τ₁ : Ty Γ} {τ₂ : Ty (Γ ▻ τ₁)}
      -> (t₁ : Γ ⊢ Π τ₁ τ₂) -> Set
    ΠFun {Γ = Γ} {τ₁ = τ₁} t₁ = (Γ' : RCtxt Γ)
      -> (t₂ : (Γ ++ Γ') ⊢ (τ₁ / wk⋆ Γ'))
      -> (v₂ : Val t₂)
      -> Val (app (t₁ /⊢ wk⋆ _) t₂)

Are there any techniques that could allow formalizing this argument? Note that it is possible to unroll $\Pi$Fun, the induction-recursion here is not essential.

Answer 1

Are there any techniques that could allow formalizing this argument?

Beluga has a notion of 'stratified types' that corresponds to this type of construction. From the user manual:

We distinguish between inductive types and stratified types. Inductive types correspond to fix-point definitions in logic and must be strictly positive, i.e. the type family we are defining cannot occur in a negative occurrence. Stratified types define a recursive type by induction on an index argument. As a consequence, the type family we are defining may occur in a negative position, but the index is decreasing.

I don't know however if the current system would be able to detect that the type of values ought to be accepted.

Answer 2

Here's a solution, that I have been making progress with, that fits normal Agda.

The aim of defining a type via induction, yet allowing non-obviously decreasing argument in a negative position can be approached via levitation from The Gentle Art of Levitation. The trick there is to introduce a syntax and interpretation of indexed datatypes.

The syntax is

data IDesc (I : Set) : Set₁ where
  var : (i : I) -> _
  k : (A : Set) -> _
  _×D_ : (D1 : IDesc I) -> (D2 : IDesc I) -> _
  ΣD ΠD : (S : Set) -> (T : S -> IDesc I) -> _

We also need an interpretation function [|_|] : {I : Set} -> IDesc I -> (P : I -> Set) -> Set, that interprets variables by P and other constructors by the obvious recursion, i.e. k by its argument, ΣD - by
Σ S (λ s → [| T s |] P), etc.

and then we have a least fixpoint on IDesc

data IMu {I : Set} (R : I -> IDesc I) (i : I) : Set where
  con : [| (R i) |] (λ j → IMu R j) -> IMu R i

Note that the troubling call becomes the first argument to ΠD after inlining and translating into the syntax of IDesc.

we thus define the type as

Vallev : (Σ _ λ Γ → Σ _ λ τ → Γ ⊢ τ) -> Set
Vallev x = IMu (λ (a , b , c) → ValDesc c) x

and ValDesc as

 ΣD ValCon ...

where ValCon is

data ValCon : Set where
  valstar : _
  valel : _
  valcons : _
  valpi : _

Here we will focus only on the problematic valpi case. The trouble here is that ΠD takes first argument a Set not a description. We thus need to apply ΠD to the result of applying IMu to the whole description. This is where the failure of strict positivity comes from.

We can now define a single function

data MutualLevDesc : Set where
  Lev : MutualLevDesc
  Desc : MutualLevDesc

DescType =  {Γ : Ctxt} -> {τ : Ty Γ} -> (t : Γ ⊢ τ) -> IDesc (Σ Ctxt (λ Γ → Σ (Ty Γ) λ τ → Γ ⊢ τ))
LevType = (Σ _ λ Γ → Σ _ λ τ → Γ ⊢ τ) -> Set
ValLevDesc : (m : MutualLevDesc) -> case m of λ{Lev → LevType
                                            ; Desc → DescType}
ValLevDesc = ...

and voila strict positivity becomes a termination proof for this function, ValLevDesc, we now have hope that we can use standard techniques of well-founded recursion to prove this function terminating.

Our original datatype would then be

Val = ValLevDesc Lev