3 ms·

Thanks for clarifying. 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

Thanks for clarifying. 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.

chriswarbo 10y ago
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 ;)
dllthomas 10y ago
> 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.
- clusmore 10y ago
  I hadn't through of doing that, good idea.