Off-topic, but related to undefined in Haskell, I love holes in Idris as a way to represent incomplete programs. I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?". You type it in, the program keeps going and a unit test is generated and put away somewhere for you to make sure that later when you implement it, you can help verify that you're doing it right.
> I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?"
For some cases, this is pretty simple to implement with unsafePerformIO - I've done that once or twice. Not a sin at all in development.
Heh, nice idea. Seems a long way off though. GHC semi-recently took a baby step in this direction by adding PartialTypeSignatures, although it emits a warning if you actually use them!
This makes sense on its own, but seems a bit silly when we consider that completely removing the signature will fix the warning ;)
Off-topic, but related to undefined in Haskell, I love holes in Idris as a way to represent incomplete programs. I'd love if it somebody could take them one step further and have it so that if a hole is evaluated at runtime, a prompt came up and said "Well this is the input, what do you think the output should be?". You type it in, the program keeps going and a unit test is generated and put away somewhere for you to make sure that later when you implement it, you can help verify that you're doing it right.