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
Conversation
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
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
Where as in logic programming you declare the rules and it can make an attempt at running your program just from those (although sometimes it tries too hard and loops forever).