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

New issue

Closed

opened 2023-08-02 13:27:43 -04:00 by rhi · 0 comments

rhi commented

2023-08-02 13:27:43 -04:00

Owner

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.

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.