Edit
It has since come to my attention that this was a formatting issue, and that the figure appears in a confusing place. Formatting is important!
type theory is impenetrable
So I’m trying to learn more about type theory because I’m trying to implement type inference for my dialog scripting language, rumor. I’m reading this paper A tutorial implementation of a dependently typed lambda calculus and it’s pretty comprehensible when:
The type language of λ→ consists of just two constructs:
![An evaluation in λ→ written in mathematical syntax, which reads: e ⇓ v / e :: τ ⇓ v, / x ⇓ x, e ⇓ λx → v v[x 7 → e′ ] ⇓ v′ / e e′ ⇓ v′, e ⇓ n e′ ⇓ v′ / e e′ ⇓ n v′, e ⇓ v / λx → e ⇓ λx → v](./20231027035311-image.png)
fam, that looks like five things.
also, wtf are these symbols, you going to explain them?
uh, these are just more symbols i don’t recognize?
well, okay then.
