https://www.youtube.com/watch?v=DRq2NgeFcO0
The book also walks you through lots of examples. The key part is the type needs to constrain the possible implementations down quite a bit.
you can sort of do this with ghci and :hoogle.
the simplest example is
foo : A -> A
since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
All of the environments are pretty interactive, and you pick and choose. but from time to time there is exactly one possible implementation that meets all the constraints, so the compiler can fill that in.
When the solution is ambiguous, Idris (and I believe wingman) will supply suggestions that you can pick from.
In your `bar` case, `bar xs = 42` is also a solution. Idris suggests 0 1 2 3 ... I think, it's going off of the constructors for the return type. I expect this technology to improve over time (try to use arguments, etc.)
Idris and Agda will also do stuff short of "fill in the answer" like "case split an argument for me" or "insert the appropriate constructor or lambda and leave a hole inside". This is quite helpful in cases where it's not gonna find the answer, but can type out the next step or two for you. (Wingman might have this, I haven't used it much. I don't know Coq at all.)
On the Agda side, the first couple of sections of "Programming Language Foundations in Agda" will walk you through using that functionality. Idris has a couple of videos that others have pointed out. It's fun stuff.
and yes programming with holes is almost magical. I really like "run as much as you can" then complain when you get stuck. kind of a mind blowing change for me.
Not if you add the condition that the type must be as general as possible.
> since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
> another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.
For some type signatures there is (are) only one (or only a few) meaningful implementation(s).
I'm curious about this. Can you provide some examples, please? Which languages can do this?