inductive types (W) #20

def0 Tag = {leaf, node}
def0 Field : Tag → ★ → ★ =
	λ t A ⇒ case t of {leaf ⇒ A; node ⇒ {o}}
def0 Body : Tag → ★ =
  	λcase {leaf ⇒ {}; node ⇒ {left, right}}
    
def0 Tree : ★ → ★ =
	λ A ⇒ (x : (t : Tag) × Field t) ⊲ 1.(Body (fst x))
    
def leaf : A → Tree A =
   	λ x ⇒ ('leaf, x) ⫽ λ()
def node: ω.(l r : Tree A) → Tree A =  -- >:(
  	λ l r ⇒ ('node, 'o) ⫽ λcase {'left ⇒ l; 'right ⇒ r}

but that's no good! we want node: 1.(l r : Tree A) → Tree A! the structure uses each subterm once, and the eliminator visits each once!!!

i have no idea what to do about this though.

inlining #24 ("the function part of a w value probably needs to be ω") here to reduce clutter --- a binary tree is something like (in hypothetical future quox with implicits and `λcase`) ``` def0 Tag = {leaf, node} def0 Field : Tag → ★ → ★ = λ t A ⇒ case t of {leaf ⇒ A; node ⇒ {o}} def0 Body : Tag → ★ = λcase {leaf ⇒ {}; node ⇒ {left, right}} def0 Tree : ★ → ★ = λ A ⇒ (x : (t : Tag) × Field t) ⊲ 1.(Body (fst x)) def leaf : A → Tree A = λ x ⇒ ('leaf, x) ⫽ λ() def node: ω.(l r : Tree A) → Tree A = -- >:( λ l r ⇒ ('node, 'o) ⫽ λcase {'left ⇒ l; 'right ⇒ r} ``` but that's no good! we want `node: 1.(l r : Tree A) → Tree A`! the structure uses each subterm once, and the eliminator visits each once!!! i have no idea what to do about this though.

rhi removed a dependency 2024-04-20 21:45:12 -04:00

#24 the function part of a w value probably needs to be ω

rhi changed title from 𝕎 to inductive types (W)

2024-04-30 20:52:53 -04:00

rhi commented

2024-04-30 21:29:45 -04:00

Author

Owner

it's like. the normal case rules are


\frac{
  \begin{gathered}
    Ψ \mid Γ ⊢ σ · e ⇒ A \rhd Θ' \qquad
    Ψ \mid Γ, x:A ⊢₀ C ⇐ ★ \\
    \overline{Ψ \mid Γ ⊢ σ · s_i ⇐ C[(a_i∷A)/x] \rhd Θ_i}^i \qquad
    \textcolor{red}{Θ := {\textstyle \bigsqcup_i Θ_i}}
  \end{gathered}
}{
  Ψ \mid Γ ⊢ σ ·
  \mathsf{case}π \; e \; \mathsf{return} \; x ⇒ C \;
  \mathsf{of} \; \{ \overline{a_i ⇒ s_i}^i \} ⇒ C[e/x] \rhd Θ'+Θ
}

but in the function in a W node it's


\frac{
  \begin{gathered}
    Ψ \mid Γ ⊢ σ · e ⇒ A \rhd Θ' \qquad
    Ψ \mid Γ, x:A ⊢₀ C ⇐ ★ \\
    \overline{Ψ \mid Γ ⊢ σ · s_i ⇐ C[(a_i∷A)/x] \rhd Θ_i}^i \qquad
    \textcolor{red}{Θ := {\textstyle \sum_i Θ_i}}
  \end{gathered}
}{
  Ψ \mid Γ ⊢ σ ·
  \mathsf{case}π \; e \; \mathsf{return} \; x ⇒ C \;
  \mathsf{of} \; \{ \overline{a_i ⇒ s_i}^i \} ⇒ C[e/x] \rhd Θ'+Θ
}

but also, presumably, only in certain top-level-ish positions???

it's like. the normal case rules are $$ \frac{ \begin{gathered} Ψ \mid Γ ⊢ σ · e ⇒ A \rhd Θ' \qquad Ψ \mid Γ, x:A ⊢₀ C ⇐ ★ \\ \overline{Ψ \mid Γ ⊢ σ · s_i ⇐ C[(a_i∷A)/x] \rhd Θ_i}^i \qquad \textcolor{red}{Θ := {\textstyle \bigsqcup_i Θ_i}} \end{gathered} }{ Ψ \mid Γ ⊢ σ · \mathsf{case}π \; e \; \mathsf{return} \; x ⇒ C \; \mathsf{of} \; \{ \overline{a_i ⇒ s_i}^i \} ⇒ C[e/x] \rhd Θ'+Θ } $$ but in the function in a W node it's $$ \frac{ \begin{gathered} Ψ \mid Γ ⊢ σ · e ⇒ A \rhd Θ' \qquad Ψ \mid Γ, x:A ⊢₀ C ⇐ ★ \\ \overline{Ψ \mid Γ ⊢ σ · s_i ⇐ C[(a_i∷A)/x] \rhd Θ_i}^i \qquad \textcolor{red}{Θ := {\textstyle \sum_i Θ_i}} \end{gathered} }{ Ψ \mid Γ ⊢ σ · \mathsf{case}π \; e \; \mathsf{return} \; x ⇒ C \; \mathsf{of} \; \{ \overline{a_i ⇒ s_i}^i \} ⇒ C[e/x] \rhd Θ'+Θ } $$ but also, presumably, only in certain top-level-ish positions???

rhi commented

2024-04-30 22:28:48 -04:00

Author

Owner

maybe this can be a quantity that is treated specially on the head of a case expression

maybe this can be a quantity that is treated specially on the head of a `case` expression