Oooh, pinged me on another thread. You might be interested in:
- delphin.poswolsky.com
- twelf.org
By 'algebraic balancing', do you mean something like the typed equality jugements in MLTT? Ie.
Γ ⊢ T₁ = T₂
Γ ⊢ t₁ = t₂ : T
Conversation
In general I mean we're allowed to calculate on both sides of the colon and each side feed back into the other. like how in algebra we could condense e.g. 2a = 4b into a = 2b
1
1
What do you mean by "each side feed back into the other"?
Interestingly most typed languages already do some level of computation in types - eg. simplifying type aliases so that `Id Int` is the same type as `Int`.
1
1
variables are matched on both sides of the colon. more than that, you can embed function calls on the right hand side like you could the left. and both sides must equate when the process is done.
1
1
By "variables are matched on both sides of the colon" do you mean that you can use variable bindings in types and terms? I'm also not sure what you mean by 'both sides must equate'. 🤔
1
1
Yes, precisely. By equate, i mean simply the thing to the left must have the type on the right, by the time the process of normalisation has completed. But the type is way more powerful than in most langs!
1
1
Hmm, you don't need to normalize the term on the left of the colon in order to type check it. In fact you usually don't afaik 😅
1
1
maybe this isn't universal. i've certainly seen examples that play with this.
1
1
I might be misunderstanding - just confused about how you are talking about the colon and your mental model of how it works. Like, maybe looking at identity types (the ones that you can construct with `refl` might be what you are thinking of?
2
1
it's entirely possible i got the wrong end of the stick somehow. i really should finish "the little typer". i'm not an expert :/
2
1
Yeah no worries! You might get a better idea of what's going on once your reach the appendix with the typing rules. I'd also _highly_ recommend having a go at implementing your own toy dependent type checker. It illuminates a bunch of stuff, I've found!
strongly keep meaning to, but have been doing productive stuff rather than satisfying my curiosity :/
1