programmer friends!
whats your favorite but not common language tooling thing?
Conversation
Special syntax for asking the compiler what it thinks the type of an expression should be, and what locals exist to write it, without running/compiling the code. I've heard that Idris has this and that it's amazing. Only works with very strictly typed languages though.
1
7
Yeah, typed holes are great, especially when you can run code with holes still present. See Agda, and Haskell as some other examples. I think Agda is one of the best as the programmer can insert extra info into the hole to guide the editing interaction.
I also like how in Coq and Lean you can use commands in the source file to query the type of something, etc. As noted here, combined with intellisense it feels a bit like a more tightly integrated REPL:
Quote Tweet
Replying to @defnotbeka
Typed holes like in Agda, Where you get syntax that you can use to manipulate half-finished code (inferring programs and case splitting etc).
Commands to #check and #eval stuff in Lean, which combined with intellisense lets you have a REPL-like experience within a source file.
2
Typed holes! That's the phrase I was looking for. My brain gave up on remembering their name.