| While I can imagine worlds which improve upon this (working in Agda and Coq is a great way to see a glimpse of it) I honestly feel like my dominant way of working is conversational with the compiler. I tend to write code for a bit, and then ask it one of two questions (1) what is the type of this thing or (2) is there any part of this that looks wrong? In particular (2) is obviously type checking (which is great to run in a fast background loop like `cargo watch -x check`) and (1) is some system for "please insert an annotation on this variable with your current inferred type". This happens near constantly, and a very common "move" I make typing is to isolate some section and give it a temporary variable name just so I can receive that annotation. The flow there could be better, to be sure. The proposal here is kind of fascinating with regard to question (1), making it less interactive and more reactive. It reminds me of, say, working with Observable, where you make edits throughout your document and watch the dependents react. To that end, being able to draw circles around fragments of code and have a persistent monitor that reactively outputs either "error: [reason]" or the type of that variable as I edit the code seems great. Though I do feel a little uncomfortable with that being literally embedded in the code. Code being reactively edited by a program makes me itch with fear of file corruption. |
Agda programmer here. Not sure what you mean here. Although Agda does save a binary cache file to minimize type-checking latency (.agdai, "agda interface") with compressed type information, it does not have any kind of hidden state. This is very different than what the OP suggests.
Other than this, I agree with you. When I write code in a typed language I have a conversation with the compiler. I keep asking, is this ok, what do you think about this, what type is this... Which is why I find OP misguided. You can have a conversation with the compiler without hidden state.