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
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
the revelation for me was that I can have variables shared across the :, and simplify expressions like with algebra
1
1
Yeah I think that's more to do with having a single namespace for types and terms - which often languages keep separated. Like:
(\x :: A -> x) :: A -> A
…probably isn't too surprising? Even though bindings are used on the left and right?
And you can write 'type functions' using type aliases:
type Id (a :: Type) = a
(\x :: Id A -> x) :: A -> Id A
2
right. and when you're for example using sized vectors, the ability to borrow variables in the type just becomes this immensely powerful thing.