Hi all,<div><br></div><div>I was fooling around with the usual inductive-recursive dependent context construction the other day:</div><div><br></div><div><pre style="margin-top: 0px; margin-bottom: 0px; font-size: 13px; text-align: left; background-color: rgb(255, 255, 255); ">
<code class="language-agda haskell"><span class="module"><span class="keyword" style="color: rgb(57, 116, 96); ">module</span> Env <span class="keyword" style="color: rgb(57, 116, 96); ">where</span></span>

<span class="title" style="color: rgb(51, 51, 51); ">open</span> <span class="import"><span class="keyword" style="color: rgb(57, 116, 96); ">import</span> Data.Unit</span>
<span class="title" style="color: rgb(51, 51, 51); ">open</span> <span class="import"><span class="keyword" style="color: rgb(57, 116, 96); ">import</span> Data.Nat</span>
<span class="title" style="color: rgb(51, 51, 51); ">open</span> <span class="import"><span class="keyword" style="color: rgb(57, 116, 96); ">import</span> Data.Fin <span class="keyword" style="color: rgb(57, 116, 96); ">hiding</span> <span class="container">(<span class="title" style="color: rgb(51, 51, 51); ">_</span>+<span class="title" style="color: rgb(51, 51, 51); ">_</span>)</span></span>
<span class="title" style="color: rgb(51, 51, 51); ">open</span> <span class="import"><span class="keyword" style="color: rgb(57, 116, 96); ">import</span> Data.Vec <span class="keyword" style="color: rgb(57, 116, 96); ">hiding</span> <span class="container">(<span class="title" style="color: rgb(51, 51, 51); ">lookup</span>)</span></span>
<span class="title" style="color: rgb(51, 51, 51); ">open</span> <span class="import"><span class="keyword" style="color: rgb(57, 116, 96); ">import</span> Data.Product</span>

<span class="title" style="color: rgb(51, 51, 51); ">mutual</span>
  <span class="class"><span class="keyword" style="color: rgb(57, 116, 96); ">data</span> <span class="label">Context</span> : <span class="label">Set</span>₁ <span class="keyword" style="color: rgb(57, 116, 96); ">where</span></span>
    ε   : <span class="label">Context</span>
    _,_ : (Γ : <span class="label">Context</span>) (<span class="label">S</span> : <span class="label">Env</span> Γ → <span class="label">Set</span>) → <span class="label">Context</span>

  <span class="label">Env</span> : <span class="label">Context</span> → <span class="label">Set</span>
  <span class="label">Env</span> ε = ⊤
  <span class="label">Env</span> (Γ , <span class="label">S</span>) = Σ (<span class="label">Env</span> Γ) <span class="label">S</span>

<span class="Apple-style-span" style="font-family: arial; white-space: normal; font-size: small; ">I then wondered if I could make it inductive-inductive, because we love inductive families around here:</span></code></pre>
<pre style="margin-top: 0px; margin-bottom: 0px; font-size: 13px; text-align: left; background-color: rgb(255, 255, 255); "><code class="language-agda haskell"><br></code></pre><pre style="margin-top: 0px; margin-bottom: 0px; font-size: 13px; text-align: left; background-color: rgb(255, 255, 255); ">
<code class="language-agda haskell">  <span class="class"><span class="keyword" style="color: rgb(57, 116, 96); ">data</span> <span class="label">Context</span>′ : <span class="label">Set</span>₁ <span class="keyword" style="color: rgb(57, 116, 96); ">where</span></span>
    ε   : <span class="label">Context</span>′
    _,_ : (Γ : <span class="label">Context</span>′) (<span class="label">S</span> : <span class="label">Env</span>′ Γ → <span class="label">Set</span>) → <span class="label">Context</span>′

  <span class="class"><span class="keyword" style="color: rgb(57, 116, 96); ">data</span> <span class="label">Env</span>′ : <span class="label">Context</span>′ → <span class="label">Set</span>₁ <span class="keyword" style="color: rgb(57, 116, 96); ">where</span></span>
    ε   : <span class="label">Env</span>′ ε
    _,_ : ∀ {Γ <span class="label">S</span>} (xs : <span class="label">Env</span>′ Γ) (x : <span class="label">S</span> xs) → <span class="label">Env</span>′ (Γ , <span class="label">S</span>)
</code></pre></div><div><code class="language-agda haskell"><br></code></div><div><code class="language-agda haskell"><span class="Apple-style-span" style="font-family: arial; ">But unfortunately, Agda (correctly) rejects this definition as not being strictly positive, because </span></code><span class="label" style="font-family: monospace; font-size: 13px; text-align: left; white-space: pre; background-color: rgb(255, 255, 255); ">Env</span><span class="Apple-style-span" style="font-family: monospace; font-size: 13px; white-space: pre; background-color: rgb(255, 255, 255); ">′</span> carries its <span class="label" style="font-family: monospace; font-size: 13px; text-align: left; white-space: pre; background-color: rgb(255, 255, 255); ">Context</span><span class="Apple-style-span" style="font-family: monospace; font-size: 13px; white-space: pre; background-color: rgb(255, 255, 255); ">′ </span>index in an implicit parameter and that appears in a negative position in <span class="label" style="font-family: monospace; font-size: 13px; text-align: left; white-space: pre; background-color: rgb(255, 255, 255); ">Context</span><span class="Apple-style-span" style="font-family: monospace; font-size: 13px; white-space: pre; background-color: rgb(255, 255, 255); ">′</span>. This type does, however, &quot;feel&quot; quite safe. I have a feeling my feeling of safety comes from the fact that the index is structurally decreasing, but I can&#39;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.</div>
<div><br></div><div>Anyway, I was wondering if anyone knew of any work on relaxing the strict positivity requirement and giving it a bit more of a &quot;structural recursion&quot; flavor so the above definition could typecheck. I&#39;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).</div>
<div><br></div><div>Thanks,</div><div>Dan</div>