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, "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.</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 "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).</div>
<div><br></div><div>Thanks,</div><div>Dan</div>