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
Replying to
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
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
Show replies