Typescript has a hole type too implemented in fp-ts and effect-ts.
Super useful for when you don't know what are you missing and get a type signature for it.
It's mostly useful for when you declare some `const foo: (bar: Bar) => Whatever` and in the midst of your implementation you don't know what you're missing.
Requires an advanced level in TS to be used to the max.
we (team hazel) recently used that device in our typescript version of a hazel setup for typed-hole-contextualized code completion as described in https://dl.acm.org/doi/10.1145/3689728
Brady has a presentation about Idris where he shows Type-Driven development (where you write code that could typecheck with some holes and you get the compiler to help you figure out the missing types for your "whatever/something" untyped variables)
It happens, but all syntax families eventually become familiar, even on LISP you eventually stop worrying about the parentheses as you learn how to grok the code.
and you start implementing it and get stuck with some callback or whatever you can put a `hole` and it will tell you the type signature of what you're missing.
Yes, and Idris actively encouraged iterative development that was based around its holes -- the book by Idris' creator Edwin Brady, Type-Driven Development[1], is an eye-opening introduction to this style of coding.
Agda has them too and they're more powerful there: https://agda.readthedocs.io/en/latest/language/lexical-struc...