I've had a silly idea and now i seem to be taking it seriously - dependently-typed prolog. If you consider DT to be algebraic balancing across the colon, and then squinting quite hard can just about consider prolog to be balancing across the equals sign, then superpowers ensue?
Conversation
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
1
2
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?
1
I've definitely though it felt kind of 'logic programmy' in a way. You can do interesting stuff with inductive types that feel like a logic program (like declaring typing rules), but then you then you have to go and reimplement those rules as again as a program.
1
1
Show replies
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!
1
1
Show replies