Re: Holes in GHC

On 1/26/12 1:30 PM, Dan Doel wrote:

On Thu, Jan 26, 2012 at 12:45 PM, Thijs Alkemade wrote:

...

Let me try to describe the goal better. The intended users are people new to Haskell or people working with existing code they are not familiar with.

Also me. I want this feature. It pretty much single handedly makes prototyping things in Agda and then porting them to Haskell a better experience than writing them straight in Haskell to begin with. I can partially implement functions and get feedback on what I need to provide and what is available, add candidate terms, have them type checked and filled in if they work. Etc.

It's significantly better than any Haskell editor I'm aware of, and adding undefined or ?foo and poking at things in ghci isn't comparable.

Ditto. I've long wished for holes and sheds in Haskell. I do a lot of my programming in an interactive bric-a-brac manner. And ever since I've started hacking with Coq and Agda ---even more than the dependent types--- this sort of interactivity has become a must-have feature. Just think about how having a REPL makes life so much nicer than going through the build cycle every time you change something. Having holes and sheds is like making the same leap in utility and productivity, except that we're making the leap from where REPLs leave off. -- Live well, ~wren